ISSN:
1433-299X
Keywords:
Keywords: Formal methods; Model checking; Industrial applications; Safety critical systems; spin
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
Abstract. In this paper we describe an industrial application of formal methods. We have used model checking techniques to model and formally verify a rather complex software, i.e. part of the “safety logic” of a railway interlocking system. The formal model is structured to retain the reusability and scalability properties of the system being modelled. Part of it is defined once for all at a low cost, and re-used. The rest of the model can be mechanically generated from the designers' current specification language. The model checker is “hidden” to the user, it runs as a powerful debugger. Its performances are impressive: exhaustive analysis of quite complex configurations with respect to rather complex properties are run in the order of minutes. The main reason for this achievement is essentially a carefully designed model, which exploits all the behaviour evolution constraints. The re-usability/scalability of the model and the fact that formal verification is automatic and efficient are the key factors which open up the possibility of a real usage by designers at design time. We have thus assessed the possibility of introducing the novel technique in the development cycle with an advantageous costs/benefits relation.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1007/s001650050022
Permalink