JACK is a new environment integrating a set of formal verification tools, supported by a graphical interface offering facilities to use these tools separately or in combination. The environment proposes several functionalities for the design, analysis and verification of concurrent systems specified using formal methods. In this paper we outline an experience on formal specification of a real railway interlocking system using JACK. Then we verify, by using JACK's checking capabilities, the correctness of the specification with respect to safety requirements. Our experience shows that the JACK environment can be applied successfully in the verification of real safety critical systems.
An industrial application for the JACK environment
Fantechi A;Gnesi S
1995
Abstract
JACK is a new environment integrating a set of formal verification tools, supported by a graphical interface offering facilities to use these tools separately or in combination. The environment proposes several functionalities for the design, analysis and verification of concurrent systems specified using formal methods. In this paper we outline an experience on formal specification of a real railway interlocking system using JACK. Then we verify, by using JACK's checking capabilities, the correctness of the specification with respect to safety requirements. Our experience shows that the JACK environment can be applied successfully in the verification of real safety critical systems.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
