PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Bernardeschi C., Fantechi A., Gnesi S., Larosa S., Mongardi G., Romano D. A formal verification environment for railway signalling system design. In: ERCIM Workshop on Formal Methods for Industrial Critical Applications (Oxford, 1996). Proceedings, pp. 39 - 55. ERCIM, 1996.
 
 
Abstract
(English)
An experience is reported OIl the specificatiou and verification of safety requirements of a railway interlocking system using formal methods. A model theoretical approach has been used for both the specification and the proof of the safety properties of the system. We used the JACK environment which integrates a set of verification tools, supported by a graphical interface offering facilities to use these tools separately or in combination. The experiment carried out has shown that the methodology can be applied successfully in the verification of industrial safety critical systems.
Subject Formal methods
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