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
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