Model Checking of Embedded Systems

by Stefania Gnesi

The integration of different dependability techniques is an open research question. We address problems that arise when attempting to combine fault tolerance mechanisms with formal methods and formal verification tools in the development of an embedded system.

In recent years, the wide spread deployment of embedded systems on which human activities depend has raised many concerns about safety issues. A combination of fault prevention, fault tolerance, fault removal and fault forecasting techniques are commonly used in order to achieve a high degree of dependability. However, there is no common agreement on a standard method to combine and integrate individual techniques. For example, industries with different backgrounds and application fields tend to adopt their own particular development trajectories when applying techniques aimed at enhancing dependability.

The application of formal methods in the rigorous definition and analysis of the functionality and the behaviour of a system means that the system is designed according to a set of predefined abstract properties that guarantee its 'correct' behaviour. It is thus astonishing to see how seldom formal methods are actually used by the safety-critical system industry, despite the fact that their adoption is increasingly required by the international standards and guidelines for the development of such systems. The truth is that industrial acceptance of formal methods is strictly related to the investment needed to introduce them, to the maturity of the tool support available, and to the ease of use. For these reasons, the current industrial trend is to adopt formal verification techniques to validate system design and integration within the existing development process. Industries prefer to use formal verification techniques assessing the quality attributes of their products, obtained by a traditional life cycle, rather than adopting a fully formal life cycle development, simply because it is cheaper to do so.

Several approaches to the application of formal methods in the development process have been proposed; they mainly differ with respect to the degree of involvement of the method. Starting from rigorous specifications, formal methods can be used for the derivation of test cases, as a validation technique aimed at proving that the specification satisfies the requirements, or just as an auxiliary technique in the automated generation of code.

Formal verification methods based on model checking are applied on a finite state representation of system behaviour. Verification is usually carried out by using model checking algorithms to demonstrate the satisfiability of certain properties formalized as logical formulae over the model of the system. For example, safety and liveness requirements can be expressed as temporal logic formulae and can be checked on the model of the system. Unfortunately, this approach suffers from the so-called 'State Space Explosion' problem that can arise when a system is composed of several subsystems. In this case, a finite state model with a number of states, which is exponential to the number of the component subsystems, can be generated. Systems that are highly dependent on data values share the same problem, producing a number of states exponential to the number of data variables. Hence, traditional model checking techniques have proved to be insufficiently powerful for many 'real' systems, when their models are larger than 100000 states.

Recent advances in model checking techniques, however, have managed to deal with very large state spaces by using symbolic manipulation algorithms inside model checkers. Such tools have been successfully applied to very large state spaces in the realm of hardware verification.

Embedded computer-controlled systems often include fault tolerance techniques. Fault tolerance is the property of a system to provide, through redundancy, a service that complies with the specification despite the occurrence of faults. The rigorous definition and verification of this class of systems is extremely important since it makes it possible to demonstrate that a system is correct even in the presence of faults and failures.

Embedded computer-controlled systems often include fault tolerance techniques. These are, for example, applied to a Railway Interlocking System.

We have applied model checking verification techniques to embedded systems illustrating how certain characteristics of embedded systems, such as the use of redundancy, can help to reduce the state space explosion problem. In this work, we have considered several case studies. Two interesting examples were the verification of the safety requirements of a Railway Interlocking System developed by Ansaldo Trasporti and the verification of some fault tolerant mechanisms defined inside the EU project GUARDS (Generic Upgradable Architecture for real-time Dependable Systems).

Both studies have shown that:

• the application of model checking formal verification methodology is feasible and well accepted in the industrial context of embedded fault tolerant systems
• the formalization process strictly depends on the application domain. Some standard rules for the passage from the semi-formal description of the system to its formal specification can be successfully applied to the field of embedded fault tolerant systems. This passage is generally recognized as one of the critical points in the introduction of formal methods in the software development cycle
• the reduction in the state space due to the phased structure of redundant systems makes the model checking approach viable in this application domain
• the use of finite state machines as the specification language has the advantage of ensuring the adherence of the formal specification to the original semi-formal one.

Link:
http://matrix.iei.pi.cnr.it/FMT/

Please contact:
Stefania Gnesi, ISTI-CNR
ERCIM Formal Methods for Industrial Critical Systems (FMICS) Working Group Chair
Tel: +39 050 3152918
E-mail: gnesi@iei.pi.cnr.it