How to create robust system models with YAKINDU Statechart Tools and verification tools

Information: YAKINDU Statechart Tools Is Now itemis CREATE

With statecharts, we can model behavioral systems like machines, robots, mobile apps and more. For safety critical applications it is necessary that they are failure safe. We need to ensure this with absolute certainty. YAKINDU Statechart Tools (now itemis CREATE)’ configurability can help to achieve this, for example by combining it with a model checking tool or otherwise integrating it into existing toolchains.

Model checking with YAKINDU Statechart Tools (now itemis CREATE)

Subsequently, we present a model-checking approach for statecharts with YAKINDU Statechart Tools (now itemis CREATE) and the Gamma verification framework. Currently, Gamma uses the UPPAAL verification engine, however, a new verification engine named Theta is already in development.

UPPAAL is an integrated tool environment for modeling, validation and verification of real-time systems modeled as timed automata, extended with data types (bounded integers, arrays etc.). It has been developed in collaboration between the Design and Analysis of Real-Time Systems group at Uppsala University, Sweden, and Basic Research in Computer Science at Aalborg University, Denmark.

Theta is a framework for abstraction refinement-based model checking. It supports various kinds of formal models and uses different algorithms and strategies. It consists of reusable and combinable modules. Theta is developed at Budapest University of Technology and Economics. This framework will be easier to integrate into existing toolchains than the UPPAAL integration explained in the following.

To present these model checking features we create a traffic light example. We extend this example to a crossroads example. Every traffic light has the states Green, Yellow and Red. We have two crossing roads. We call the first road 51st Street and the second 2nd Avenue. The one important safety requirement is the following:

The traffic lights of 51st St and 2nd Ave shall never be green at the same time!

Otherwise this would lead to serious accidents. The following image illustrates the trafficlight statechart.

This statechart shows one traffic light. But we need two and later even more instances of this state machine. This feature is in development for YAKINDU Statechart Tools (now itemis CREATE). With the Gamma project, we are now already able to create a statechart of statecharts for verification purposes. Therefore we create a new statechart Controller with two interfaces I51stStControl and I2ndAveControl.

These interfaces are the connectors to the first TrafficLight statechart. The connection points are the events. The TrafficLight statechart offers in events called toggle and toggleToGreen, and the Controller statechart’s interfaces have corresponding out events. To make these statecharts run together, some additional Gamma models need to be created and generated. For each statechart we need a Gamma state machine, interface and generation models. We define the  composite statechart with this Gamma component definition. This is a textual model in a .gcd file. If we right-click on the .gcd file, we see additional context menu entries. One of them is “Open UPPAAL Query Generator”. This UPPAAL query generator is a simple dialog with forms to build a condition for model checking. The tool supports the severities “might eventually”, “must eventually”, “might always”, “must always” and “leads to”. For our condition we need the “must always” severity in negation. This is very strict because it always needs to be true. With a logical expression this condition looks like the following:

!((51stSt_Green)&&(2ndAve_Green))

We can build this condition with the forms editor in the UPPAAL Query Generator. The condition is translated to a more complex condition to be executed with the UPPAAL model checker. What’s especially great is that the query generator offers direct verification within the editor. If the condition does not hold, a log file is generated. It provides a detailed view of the statecharts’  different states and thus makes debugging easier. The following image shows the verification of our condition on the model. The condition holds:

If we check the opposite condition “sometimes both traffic lights get green” we get an error:

The integration of UPPAAL is a bit complicated. That’s the reason why a new verification engine Theta is under development.

With the integration Gamma you can do model checking on your YAKINDU Statechart Tools (now itemis CREATE) and thus create robust system models. You can integrate all tools within one Eclipse application and do not have to switch between different applications.

Information: YAKINDU Statechart Tools Is Now itemis CREATE