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.

An Experience in Formal Verification of Safety Properties of a Railway Signalling Control System

BERNARDESCHI, CINZIA;
1995

Abstract

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.
9783540199625
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11568/22349
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact