JACK3 - Just Another Concurrency Kit [Release 3.0]

Trentanni G.

Process calculi  Automata  Bisimulation  Verification  Model checking 

JACK3 stands for /Just Another Concurrency Kit/. It is an environment integrating a set of 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 process algebra. In particular, the concurrent systems that are suitable to be studied by means of the latest release JACK3-Lite are that ones described by process algebrae as Esterel, Meije, CCS and Basic Lotos. The basic idea of JACK3-Lite is simple: to put together tools for drawing, minimising and partitioning automata, for transforming algebraic processes into automata and to perform model checking on them, under an unified environment with a graphical user interface with the aim of automatizing the various ways by which these tools exchange data each other and giving to the user a general system to build up the preferred specification/verification development cycle in an expandable environment.