by Cinzia Bernardeschi, Alessandro Fantechi and Stefania Gnesi
JACK, Just Another Concurrency Kit, is an environment integrating a set of formal verification tools. Functionalities for the design, analysis and verification of concurrent systems specified using formal methods are provided. It is supported by a graphical interface that offers facilities to use the tools separately or in combination (see also ERCIM News No.21). JACK is now being experimented in a pilot project for the formal validation of a railway signal interlocking system produced by ANSALDO Trasporti. Our tests show that this approach can be successfully applied in the verification of real safety critical systems.
Formal Methods can be used to specify and model the behaviour of a system at different levels of abstraction, and to mathematically verify that the system design and implementation satisfy certain functional and safety properties. A variety of methodologies and techniques have recently been developed for this purpose. When the specification of a system is given through a formal method, all the phases of the software life cycle will benefit. The formal specification acts as a bridge between the informal requirements and the final software product and can be used in its validation. Over the last few years, international standards and guidelines have tended to stipulate that formal methods be adopted in the development of highly dependable computer controlled systems.
We report here an experience on formal specification and verification carried out in a pilot project on the re-validation of the functional specification of a railway computer-based interlocking system. The interlocking system is that part of the application software responsible for controlling the equipment of a signalling system. This system includes both hardware and software fault-tolerant features that meet very stringent safety requirements. The main aim of the experiment was to study the interactions between the control units of different components of the railway system, in particular a level-crossing and a shunting route control.
The formal specification of the level-crossing and the shunting route control units was performed textually in terms of process algebra and graphically by automata. Certain safety requirements on the system behaviour were verified formally by giving a logical presentation of these safety requirements and then verifying their satisfiability on the model (automaton) of the interlocking system. Both the specification and the verification phases were carried within the integrated verification environment - JACK.
The formal specification of the operations of interlocking system units implied the definition of many processes. Since the dimension of the model tends to grow exponentially with the number of component processes, this has meant the increase of state explosion problems during the construction of the global model on which the safety properties should be verified. To deal with such problems, which at times cause all the available memory to be consumed during the generation of the automaton, we have adopted some correctness preserving "abstraction" techniques. These allow parts of the specification, which are not of immediate interest, to be excluded while still preserving the satisfiabilty of the property on the global model.