AN INDUSTRIAL APPLICATION FOR THE JACK ENVIRONMENT

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. T he environment proposes several functionalities for the design, analys is and verification of concurrent systems specified using formal metho ds. In this paper we outline an experience on formal specification of a real railway interlocking system using JACK. Then we verify, by usin g JACK's checking capabilities, the correctness of the specification w ith respect to safety requirements. Our experience shows that the JACK environment can be applied successfully in the verification of real s afety critical systems. (C) 1997 Elsevier Science Inc.