Istituto di Scienza e Tecnologie dell'Informazione     
Bernardeschi C., Fantechi A., Gnesi S. An industrial application for the JACK environment. Technical report, 1995.
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.
Subject JACK environment
D.2.4 Software/Program Verification: Formal methods
D.2.4 Software/Program Verification: Model Checking

Icona documento 1) Download Document PS

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