Istituto di Scienza e Tecnologie dell'Informazione     
Bernardeschi C., Fantechi A., Gnesi S. An industrial application for the jack environment. In: Journal of Systems and Software, vol. 39 (3) pp. 249 - 264. Elsevier, 1997.
JACK, Just Another Concurrency Kit, 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 Formal method
Formal verification
D.2.4 Software/Program Verification

Icona documento 1) 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