A Formal Verification Environment for Railway Signaling System Design |
| |
Authors: | Cinzia Bernardeschi Alessandro Fantechi Stefania Gnesi Salvatore Larosa Giorgio Mongardi Dario Romano |
| |
Affiliation: | (1) Dipartimento di Ingegneria della Informazione, Università di Pisa, Italy.;(2) Istituto di Elaborazione della Informazione - C.N.R., Pisa, Italy.;(3) Ansaldo Trasporti, Genova - Napoli, Italy. |
| |
Abstract: | A fundamental problem in the design and development of embedded control systems is the verification of safety requirements. Formal methods, offering a mathematical way to specify and analyze the behavior of a system, together with the related support tools can successfully be applied in the formal proof that a system is safe. However, the complexity of real systems is such that automated tools often fail to formally validate such systems.This paper outlines an experience on formal specification and verification carried out in a pilot project aiming at the validation of a railway computer based interlocking system. Both the specification and the verification phases were carried out in the JACK (Just Another Concurrency Kit) integrated environment. The formal specification of the system was done by means of process algebra terms. The formal verification of the safety requirements was done first by giving a logical specification of such safety requirements, and then by means of model checking algorithms. Abstraction techniques were defined to make the problem of safety requirements validation tractable by the JACK environment. |
| |
Keywords: | safety critical systems mechanical verification temporal logic model checking |
本文献已被 SpringerLink 等数据库收录! |
|