JACK - Formal Specification and Verification of Reactive Systems

by Stefania Gnesi

A new support environment for the formal specification and verification of reactive systems specified by means of process algebras has been developed by groups working at IEI-CNR, Pisa, and at the University "La Sapienza", Rome, in the context of the LAMBRUSCO project, supported by the CNR Finalized Project for Information Systems and Parallel Computation. This environment, called JACK - Just Another Concurrency Kit, integrates a set of verification tools, and is supported by a graphical interface offering facilities so that these tools can be used separately or in combination.

Process algebras are generally recognized as a convenient tool for describing reactive systems at different levels of abstraction. They rely on a small set of basic operators which correspond to primitive notions of concurrent systems and on one or more notions of behavioural equivalence or preorder. The operators are used to build complex systems from more elementary ones. The behavioural equivalences are used to study the relationships between different descriptions (e.g. specification and implementation) of the same system at different levels of abstraction and thus to perform part of the analysis.

Logic is also a good candidate to provide more abstract specifications, since it makes it possible to describe system properties rather than system behaviour. Different types of temporal and modal logics have been proposed for the abstract specification of concurrent systems; in particular, modal and temporal logics, due to their ability to deal with notions such as necessity, possibility, eventuality, etc., have been recognized as suitable formalisms for specifying properties of concurrent systems.

Modal and temporal logics have been equipped with model checkers to prove satisfiability of formulae and thus properties: a system, usually finite state, is considered as a potential model for the formula expressing the desired property. Specific logics for process algebras have been proposed, among them we recall the new action-based logic ACTL. Recently, a collaboration between IEI-CNR, Pisa, and the University "La Sapienza", Rome has produced a verification environment, JACK, defined to support reasoning with ACTL.

The purpose of JACK is to provide a general environment that offers a series of functionalities, ranging from the specification of reactive systems to the verification of behavioural and logical properties. This environment has been built starting from the development of a number of independent tools that were successively integrated. The tools were developed separately by different research groups: some at IEI-CNR and University "La Sapienza", others at INRIA (Sophia-Antipolis). JACK covers much of the formal software development process, including the formalization of requirements, behavioural equivalence proofs, graph transformations and logic verifications by model checking algorithms.

JACK provides a user friendly interface that allows the user-environment dialog to be performed by means of graphical widgets. It also provides a generator of ACTL formulae, which produces an ACTL formula from a natural language sentence, thus giving an assistance in the formalization of informal systems requirements.