A formal verification environment for railway signaling system design

  • Bernardeschi C
  • Fantechi A
  • Gnesi S
 et al. 
  • 12


    Mendeley users who have this article in their library.
  • 47


    Citations of this article.


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.

Author-supplied keywords

  • Mechanical verification
  • Model checking
  • Safety critical systems
  • Temporal logic

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document


  • Cinzia Bernardeschi

  • Alessandro Fantechi

  • Stefania Gnesi

  • Salvatore Larosa

  • Giorgio Mongardi

  • Dario Romano

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free