The Gamma Statechart Composition Framework
Articles Blog

The Gamma Statechart Composition Framework

October 18, 2019


Welcome to the demonstration of the Gamma Statechart Composition Framework. In this video, we will present how you can use Gamma to design, analyse and generate code from hierarchical networks of communicating state-charts. Gamma has been conceived in the context of reactive controllers, where systems generate reactions to external stimuli depending on their current state. Such systems can be conveniently modelled with state-charts. For more complex systems, however, a single state-chart model may soon become way too complicated to understand and maintain. The Gamma Framework enables the decomposition of the problem by modelling reactive systems as a hierarchical network of communicating statechart components. The Framework defines a modelling language for state-charts and composite components. Statecharts, however, may also come from Yakindu Statechart Tools. The modelling language for composite components comes with a rigorously defined formal semantics, precisely describing the means of communication and the behaviour of composite systems. Based on this semantics, the Gamma Framework supports the automatic generation of source code for composite models. The formal semantics also enables the precise generation of formal system models, which can be used to check the behaviour of the system against user-specified requirements. If the satisfaction of a requirement can be proven by a witness, which is a single behaviour of the system, the Gamma Framework will present this behaviour to facilitate debugging. Let us take a look at a simple example to demonstrate how the tool works in practice. In this example, we have modelled the controller of the traffic lights of a single crossroad. We have used two statecharts, one that controls the state of a single traffic light, and another that takes care of synchronising the lights of the two crossing roads. The light-control statechart describes the usual states of a three-phase traffic light, including the blinking yellow light, that, in this example, may be triggered by the police. The communication between the crossroad-controller and the light-controllers will happen through separately defined interfaces. An interface describes the different signals that can be sent or received through a port that implements it. The crossroad-controller statechart will also use these interfaces to toggle the light-controllers in a specific order. Furthermore, it will forward any police interrupts to trigger the blinking yellow state of the lights. The whole system, composed of two light-controllers and a crossroad-controller, is defined in a composite component definition. You can see an illustration of what the textual model describes. Notice the definition of composite component ports, the instantiation of constituent components, port bindings that describe which constituent component should handle a composite component port, and finally the definition of communication channels. At this point, our model should be ready. Generating the implementation is now only a matter of a few clicks. Currently, the framework supports the generation of Java code. We can also use the formal verification capabilities of the Gamma Framework to check if our controller is safe. First, we have to generate a formal model for the underlying UPPAAL model checker. Requirements may be specified through the query generator UI. Users can choose from a number of requirement templates describing different kinds of behaviour, then fill them with logical expressions describing state configurations. Let’s specify that we should never see a state in which both light-controllers are in the green state. The verification process can be invoked by the click of a button. Unfortunately, the result is negative, we have a counterexample. The great thing is, however, that we can use it to debug and fix the problem. The execution sequence driving our system in the dangerous state is saved as a text file, as well as a jUnit test replaying the sequence on the generated implementation. This way, we can make sure that the violating behaviour is indeed present in the code. We may use the simulation capabilities of Yakindu to visualise the problem. This reveals that if a police interrupt arrives right after initializing the primary road to green, the lights enter the blinking yellow state, but the controller will still assume that it can change the state of the lights. If the interrupt is revoked two steps later, the inconsistent view of the controller will lead to toggling the wrong light, leading to a state that should never occur. Knowing this, the model would be easy to fix now. Thank you for watching this video about the Gamma Statechart Composition Framework, a tool for designing, analysing and generating code from hierarchical networks of communicating state-charts. Make sure to check out the tool and our detailed tutorial at gamma.inf.mit.bme.hu.

Leave a Reply

Your email address will not be published. Required fields are marked *