PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Anselmi A., Bernardeschi C., Fantechi A., Gnesi S., Larosa S., Mongardi G., Torielli F. An experience in formal verification of safety properties of a railway signalling control system. In: SAFECOMP'95 - Proceedings of 14th International Conference on Computer Safety, Reliabilty and Security (Belgirate, Italy, 11-13 october 1995). Proceedings, pp. 474 - 488. Gerhald Rabe (ed.). Springer, 1995.
 
 
Abstract
(English)
An experience on the specification and verification of a railway interlocking system produced in a joint project with Ansaldo and the Italian Railways is reported. In the project we have used the JACK environment both to build the algebraic and graphical specification of such a system and to perform the verification of logic formulae on the model of the system itself. JACK is an environment integrating a set of verification tools, supported by a graphical interface offering facilities to use these tools separately or in combination. The experiment carried on has shown that the methodology can be applied successfully in the verification of safety critical systems. 1
Subject Railway signalling
D.2.4 Software/Program Verification


Icona documento 1) Download Document PDF


Icona documento Open access Icona documento Restricted Icona documento Private

 


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional