Global State Checker & SD Consistency Checker

Last Updated on Thursday, 19 March 2015 13:08 Written by Petra Brosch

 

The Global State Checker and the Sequence Diagram Consistency Checker (SD Checker) implement a novel propositional encoding for the reachability problem of communicating state machines and sequence diagrams as provided by UML. The problem deals with the question whether there is a path to some combination of states in a state machine and, respectively, to check if a set of communicating state machines and a sequence diagram are consistent. Reachability analysis finds its application in many verification scenarios, ensuring consistency between sequence diagrams and state machines is a valuable tool for testing. By using an encoding inspired by approaches to encode planning problems in artificial intelligence, we obtain a compact representation of the both problems in propositional logic.

Prototype

The implementation of the Global State Checker and the SD Checker is based on the Multiview Modeling Language (MVML), which is inspired by UML and consists of a simplified, yet concise variant of class diagrams, sequence diagrams, and state machine diagrams. MVML is defined as Ecore metamodel and is supported by a graphical modeling editor. Further, MVML sequence diagrams may be automatically merged with our SDMerge tool. Both, the Global State Checker and the SD Checker are integrated in one tool.

The Global State Checker may be used either as API, or directly in the graphical modeling editor by selecting a set of states and right clicking on MVML Model Checking -> Check global state. Then, a bound and an expected outcome is specified. The result is shown as red or green highlighting of the selected states, depending on the effective outcome. Additionally, the Global State Checker Console (Window -> Show View -> Other -> MVML Model Checking -> Global State Checker Console) lists the specified test cases and gives the path to reachable states.

The SD Checker may also be used either as API, or directly in the graphical modeling editor. The MVML model has to contain a set of communicating state machines as well as a sequence diagram. Then the SD Checker is called by right-clicking on MVML Model Checking -> Check sequence. The SD Checker Console (Window -> Show View -> Other -> MVML Model Checking -> Sequence Checker Console) lists the trace containing the sequence diagram in case consistency is given or points to the error location otherwise.

A set of examples for global state checking is shipped with the plug-in. Import -> Plug-ins and Fragments -> org.modelevolution.multiview.mc.examples and open a *.mvml or *.mvmld file.

Experiments and Benchmarks

To give a first impression on the runtimes of the Global State Checker, consider the following table.

The following table shows the average runtimes in milliseconds for all possible combinations of states for the examples.

Bound315100500
Timeencodingsolvingtotalencodingsolvingtotalencodingsolvingtotalencodingsolvingtotal
mail 8 1 9 5 15 20 34 1,173 1,207 201 63,043 63,244
coffee 13 3 16 12 24 36 28 2,165 2,193 143 39,291 39,434
philosophers 18 3 21 21 44 65 43 21,192 21,235 - - -

 Benchmark sets:

Download

Our prototype implementation is available as Eclipse plug-in on our update site:
http://modelevolution.org/updatesite

Select category Model Evolution and install the plug-ins Multiview Modeling Language and  MVML Model Checking.
Due to some dependencies of the graphical editor, currently only Eclipse Juno is supported.