PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Bernadeschi C., Fantechi A., Gnesi S., Larosa S., Mongardi G., Romano D. A Formal Verication Environment for Railway Signaling System Design. Technical report, 1995.
 
 
Abstract
(English)
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 veri cation carried out in a pilot project aiming at the validation of a railway computer based interlocking system. Both the specifi cation 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. Ab- straction techniques were defined to make the problem of safety requirements validation tractable by the JACK environment.
Subject Safety critical systems
Software Engineering
Requirements/Specifications
Mechanical verification


Icona documento 1) Download Document PS
Icona documento 2) 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