Transforming Specifications to verify Embedded Systems

by María del Mar Gallardo, Jesús Martínez, Pedro Merino and Ernesto Pimentel

A team from the GISUM research group at the University of Málaga is working on extending current tools to analyse the functional correctness of software for embedded systems.

Interest in these tools, which are based on formal languages, is now moving from academia to industry. In this new context, the systems to be analysed are more realistic and the problems of complexity appear more frequently, especially for automatic verification. One promising method for maintaining the interest in verification is the use of reduction techniques to obtain smaller specifications. We are using a robust syntactic transformation method that reduces the specification and is compatible with existing tools.

The use of formal specifications to analyse the correctness of software for embedded systems has been a hot research topic in the last 25 to 30 years. Many design errors have been detected by using the specification as a way of manually revising the design, or more interestingly, as a way of performing an exhaustive inspection of the potential executions of the system. This last automatic method, usually called model checking, has been mainly implemented for academic use. More interest now exists in industry, however, in having robust tools supporting verification facilities for the development of this kind of critical system.

Although the available hardware and software technology has considerably increased the size of the specifications that can be exhaustively inspected, the state explosion still presents a major problem. The algorithms usually implemented produce a low quality analysis when the tool runs out of memory.

The automatic verification team in GISUM is working on areas of model checking, static analysis, abstract interpretation, and verification of software for critical systems, including communication protocols and embedded systems. A current topic of our research is the combination of model checking and static analysis techniques to improve the quality of verification with the abstract model-checking approach. This method consists in replacing the specification of the system being analysed with an abstract one that produces a smaller state space. When the abstraction is sound, then the verification of the abstract version provides information about the correctness of the original specification for given kinds of properties. Our aim is to develop both theoretical frameworks and tools to support abstraction by automatically transforming the specification.

One of the main current results is the development of a new approximation method to verify properties represented with temporal logic formulas using abstract models. The abstraction of the model is guided by the change in the type of some selected variables. This change reduces the domain of values for the variables, and must be followed by updating the instructions that manipulate the variables. Both changes can be implemented by program transformation. Similar ideas about approximation and code transformation have also been proposed for more commercial specification languages like SDL/MSC and UML StateCharts/Sequence Diagrams.

The snapshot of aSpin with the abstract specification of an elevator system. The transformation has been carried out applying abstraction to the variable "position". The structure of the specification, given as folders and sub-folders, helps the designer in the selection of the transformation.

Regarding tools, our purpose is to develop reusable modules to incorporate abstraction in existing model-checking toolsets. One main topic is to define standard representations for the specification of systems and properties. XML is now being used for this purpose. The availability of APIs to process XML makes the transformation work easier.

The current visible result is aSpin that extends the model checker Spin to support the theoretical proposals developed in the group (see 7th ERCIM FMICS Workshop).

We now plan to extend other tools. The verification of Messages Sequence Charts (MSC) against SDL (presented at 5th ERCIM FMICS Workshop) can be implemented on top of Telelogic Tau. The method for verifying StataCharts against Sequence Charts (see paper in JOT) can be implemented in VisualState, Rapshody or Rational Rose.

A further project is the development of transformation schemes for standard programming languages, in order to take advantage of future model-checking tools for these languages.

Links:
GISUM research group: http://www.lcc.uma.es/~gisum/
Verification tools and related papers: http://www.lcc.uma.es/~gisum/fmse/tools

Please contact:
María del Mar Gallardo, Jesús Martínez, Pedro Merino, Ernesto Pimentel, University of Málaga, Spain
E-mail: gallardo@lcc.uma.es, jmcruz@lcc.uma.es, pedro@lcc.uma.es, pimentel@lcc.uma.es