Formal Verification of Statechart Networks

Information: YAKINDU Statechart Tools Is Now itemis CREATE

Imagine you have developed a spacecraft that is super-safe, because following the trends, you have applied model-based design and testing. All components modeled by statecharts, tested, implemented by automatically generated code, what can go wrong? Then on the day of launch, the whole thing explodes in a spectacular fireball. The cause? Interactions. The cure? Formal verification.

Reality is usually much more complex, of course. Nevertheless, the analysis of component interactions is often neglected, even though much of the design mistakes we make are related to wrong assumptions about the other components. How can formal verification help? What is formal verification in the first place?

This post will introduce the basic concepts, demonstrating them through an experimental tool, called the Gamma Statechart Composition Framework, which is developed by researchers of the Budapest University of Technology and Economics, in Hungary. To keep things simple, the example system will be a crossroad with a standard three-phase traffic light in each direction (see Figure 1 for an illustration).

Figure 1: Illustration of crossroad states

A Plain Old Crossroad Controller

To reduce the complexity of the model, we divide the controller into submodules. For each road, the lights will be controlled by an instance of the traffic light controller statechart (Figure 2), while a separate crossroad controller (Figure 3) will be responsible for the coordination of the flow of traffic.

The model of the controllers should be easy to read. The traffic light controllers start from the Red state and will advance to the next state upon receiving a toggle signal. In this example, we assume that timing comes from outside of the system – in the form of such toggle signals. The external toggles will be sent to the crossroad controller first, so that it can decide which traffic light(s) to toggle in the given step. This strategy separates the responsibility of handling the lights (through the LightCommands interface) and coordinating the flow of traffic.

As an extra feature, assume that the police could interrupt the behavior of the crossroad at any time, switching all the lights to a blinking yellow state. This signal is also sent through the crossroad controller, which will forward it to the traffic light controllers (as the blinking yellow behavior is implemented there).

Figure 2: Statechart model of the traffic light controller

Figure 3. Statechart model of the crossroad controller

Notice our interfaces in the two statecharts. Upon closer look, there are only three types of interfaces in the system, but there are multiple “instances” and sometimes they are “inside out”. This is due to the concept of ports. A port is an endpoint of communication that can implement interfaces in provided or required mode. Interpreting the different interfaces as ports, Figure 4 shows the layout of the whole crossroad system.

Figure 4. Composite system model for the whole crossroad

At this point, after some simulations, we should be pretty confident that the model is correct. After all, it is quite simple, and we have even managed to separate responsibilities by using submodules. We could fire up our code generator, implement the glue-code, and deploy the controller.

After the catchy introduction, I do not expect anyone to believe that the model is correct. Some readers might have a clue about the source of the problem – the only non-trivial part is the police interrupt signal, right? However, the exact nature of the problem and the way to trigger it is not straightforward to see.

Catching Bugs with Formal Verification

Formal methods are mathematically founded techniques mainly used in software and hardware design, with the aim of raising reliability and robustness. Formal verification is a family of such techniques, where the goal is to prove that the system design meets the previously formalized specifications.

Formal verification is significantly different from testing. Testing inherently samples the behavior of a system, while formal verification techniques – such as model checking, which is deployed in the prototype tool demonstrated here – exhaustively analyze every possible behavior. Truth to be told, this can get very expensive. There are more and more domains, however, where the benefits tend to exceed the cost.

Getting back to our crossroad, the single most important requirement in the specification of any crossroad is to not give a green light to both roads. As this is a state invariant, one of the simplest requirements, it can be formalized in a number of ways. Model checkers typically support assertions or temporal logics. For the purpose of this blogpost, it is enough to precisely state that in any state of the whole system, the Green state must not be active in both instances of the traffic light controller.

Proper tool support should let users define these requirements by using textual templates. The tool would then automatically translate the formalized requirement into logic formulas, something that can be fed into a model checker. This would also happen automatically, as most model checkers are fully automated tools. The last – and probably most important – step is the processing of the results.

A model checker always looks for the possibility of some (bad or desired) behavior in the system. Whenever it can actually find some of the specified behavior, it will also produce an example trace – something that can be replayed on our model or code. Such a trace can be of great help when the trace is actually a counterexample to our specification, because they often invoke the functions of our system in an unusual, but almost certainly unexpected way.

Therefore, model checkers can be regarded as the “ethical hackers” of system design, automated adversaries that will try to break our system before it gets deployed.

How to Cause a Crash

The described features are currently being realized in the labs of the Budapest University of Technology and Economics based on statecharts, and with the prototype version, it is already possible to analyze our crossroad model. With that prototype, it takes only a few clicks to see how a policeman can cause a mass accident by sending his interrupt at the wrong time (see Figure 5).

Figure 5. Verification with Gamma

Without further ado, let us see the sequence of inputs that can break our crossroad controller.

1. The crossroad initializes and the crossroad controller toggles the priority road to enter the Green
2. A police interrupt arrives, gets relayed to the traffic light controllers and switches every light to a blinking yellow state.
3. The external timer sends a toggle The crossroad controller now thinks that the priority road has switched to the Yellow state, but it is still blinking due to the previous police interrupt.
4. Another toggle signal arrives. The crossroad controller thinks that the priority road has red, while the secondary road got green
5. The policeman changes his mind and sends another interrupt. The signal is relayed to the traffic light controllers, returning them into normal operation (priority road green, secondary road red).
6. Another toggle signal makes the crossroad controller send a toggle signal to the secondary road believing that it is now turning yellow, but in reality, the traffic light controllers are not synchronized anymore, so it gives green light to the secondary road.

There we are, with the green light blazing in every direction, confused drivers drifting and crashing.

What caused the problem? The wrong handling of the police interrupts in the crossroad controller, obviously. The tricky part is, however, that it would have been very hard to notice this mistake without considering the environment of the crossroad controller. Indeed, our specification considered the traffic light controllers only, while the problem originates in the crossroad controller. In larger systems, these fault chains may become much longer through component interactions. Even a small, seemingly insignificant violation of the (often undocumented) assumptions about the component can cause a somewhat larger violation in another, propagating until finally a system-level failure is caused in a seemingly unrelated part of the system. Formal analysis of composite systems is therefore an important aspect of safety-critical system design, often required by industry standards.

That’s Great, Can I Have It?

In a matter of time, yes. You can already use model checkers (we suggest one of the most user-friendly model checkers, UPPAAL, which is free for non-commercial use), but they usually require a deep mathematical knowledge and have specific formal modelling languages. More and more tools try to offer verification support for engineer-friendly modelling formalisms, and larger companies also have internal solutions tailored to solve their specific problem.

We at the Budapest University of Technology and Economics are building a flexible framework based on model transformations to bridge the gap between modelling tools designed for engineers and verification tools that require great expertise to work with. With the core of the Gamma Framework, we are bundling this expertise into an Eclipse-based tool to complement your modelling framework. If you are using Yakindu Statechart Tools (now itemis CREATE) to model your components, stay tuned, as the workflow described above is about to get real. In the meantime, check out our preview and the traffic light tutorial here. If you are new to statecharts and modelling, download Yakindu Statechart Tools (now itemis CREATE) and get started with the great tutorials offered by itemis.

Information: YAKINDU Statechart Tools Is Now itemis CREATE