JACK3 - Just Another Concurrency Kit [Release 1.0]

Trentanni G.

Process calculi  Automata  Bisimulation  Verification  Model checking 

JACK is an environment based on the use of process algebras, automata and temporal logic formalisms, which supports many phases of the system development process. The idea behind the JACK environment is to integrate different specication and verication tools, independently developed at different research institutes (I.E.I.- C.N.R. and the University of Rome La Sapienza in Italy, and INRIA in France), to provide an environment in which a user can choose from several verication tools by means of auser-friendly graphic interface. This last feature is quite an important one since it is nowadays widely recognized that there is no single specication and verication technique which can cover all aspects of system design in a satisfactory way; rather, different techniques and tools match different stages of design. JACK includes also a model-checker for ACTL, a branching time temporal logic suitable to express proper ties of reactive systems whose behaviour is characterized by the actions they perform and whose semantics is dened by means of Labelled Transition Systems.