[home] [info] [docu] [examples] [download] [contact] [applications] [bugs]

AGG Application: Translating Statecharts to CSP

As there is currently no formally defined semantics for UML, consistency checking of UML models on a semantic basis cannot be done within the UML itself. In principle, there are at least two different ways of tackling the problem of achieving semantic consistency: One is to define a complete formal semantics for the UML. The other is to establish semantic consistency using an approach not relying on such a complete semantics.

Our approach for consistency checking relies on the observation that semantic consistency checking can also be performed by choosing an appropriate semantic domain for a particular consistency problem. A semantic domain has to be appropriate in the
sense that it must allow the formal specification and (automatic) verification of consistency constraints of the UML models. For different consistency problems also different semantic domains can be chosen. As a consequence, the specification of mappings of UML models into various semantic domains is of major interest because such a mapping is essential for checking consistency of UML models following our approach.

For analyzing consistency of statecharts, we have proposed a mapping to Communicating Sequential Processes (CSP)  which provide a mathematical  model for concurrency based on a simple programming notation and supported by tools.
 

A semantic mapping can be described by attributed graph transformation. Using AGG as an engine for attributed graph transformation it becomes possible to automatically translate UML models into some semantic domain and to do semantic consistency  checking by further tools. For the whole procedure we assume that the UML model  is already checked to be syntactically correct.

The graph part of the following mapping rules represent meta model patterns showing the abstract syntax of the source language UML. The metamodel representation is extended by attributes containing semantic expressions. Each model element which shall be equipped with corresponding semantic expressions is extended by further attributes containing some semantic information. Mapping statecharts to CSP, a new equation is created for the state machine and for each state not being a pseudo state. Thus, nodes of type StateMachine and State get a semantic attribute exp each containing the corresponding CSP equation after translation. Moreover, we need a semantic attribute extBeh, since the external behaviour is inherited from the superstate.

The proper attribute computation is encapsulated in a separate Java class. Each translation rule refers to a method of this class which computes the new CSP expression. Since the target language is rather simple we implemented its context-free replacement rules directly in Java.  Consider  class CSP to understand how the computation can look like.

In rules  top,  comp and simple, the attribute computation is rather easy. After testing that the semantic expression is not yet computed the rules just create CSP equations for the state machine and its states.

Figure 1. Rule "top"  to translate the top state




Figure 2.  Rule "comp" to proceed composite states


 


Figure 3. Rule "simple" to translate a simple state

In the following rules, we have to test the occurrence of non-terminals in semantic expressions and to replace them by equivalent expressions. To do so, we use the additional attribute extBeh which clearly has to be determined first. This is done by rules extBeh_top2 and extBeh_comp2.
 
 

Figure 4. Rule "extBeh_top2" to compute the external behaviour of the top state


 


For mapping rule extBeh_comp2 attribute conditions: !k.equals("pseudo") and !b.equals("")  are added.

Figure 5. Rule "extBeh_comp2" to compute the external behaviour of a composite state


  Rule extBeh_top has the following attribute condition:  e.indexOf("extBeh(top)") != -1

Figure 6. Rule "extBeh_top" to translate the external behaviour of the top state


 

For mapping rule extBeh_comp attribute conditions: e.indexOf(``extBeh(``+s+'')'') != -1, !k.equals(``pseudo'') and !b.equals("") 
are added.

Figure 7. Rule "extBeh_comp" to translate the external behaviour of a composite state


The following three rules are needed to translate state transitions. They implement an iteration through the set of event objects of transitions going out of state s. Rule directBeh_s has attribute condition: e.indexOf("directBeh("+s+")") != -1

Figure 8.  Rule "directBeh_s" to start the translation of the direct behaviour of a simple state

Both rules directBeh_m and directBeh_e have attribute condition: e.indexOf("dB") != -1

Figure 9. Rule "directBeh_m" to continue the translation of the direct behaviour of a simple state

Figure 10. Rule "directBeh_e" to end the translation of the direct behaviour of a simple state


 

Mapping the following abstract syntax graph according to the above mapping rules, i.e. applying the above rules to the following graph as long as possible, yields a set of CSP equations collected in TP.csp describing the CSP semantics of the given statechart.
 

Figure 11.  Start graph showing  the abstract syntax of a sample statechart