The Integration Project for the JACK Environment.
Amar Bouali, Stefania Gnesi, Salvatore Larosa · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 1994
JACK, standing for Just Another Concurrency Kit, is a new environment integrating a set of verication tools, supported by a graphical interface oering facilities to use these tools separately or in combination.The environment proposes several functionalities for the design, analysis and verication of concurrent systems specied using process algebra.Tools exchange information through a text format called Fc2.Users are able to graphically layout their specications, that will be automatically converted into the Fc2 format and then minimised with respect to various kinds of equivalences.A branching time and action based logic, ACTL, is used to describe the properties that the specication must satisfy, and model checking of ACTL formulae on the specication is performed in linear time.A translator from Natural Language to ACTL formulae is provided, in order to simplify the job to describe the specication properties by A CTL formulae.A description of the graphical interface is given together with its functionalities and the exchange format used by the tools.As an example of use of JACK, we p resent a small case study within JACK, that covers both verication of a software system and verication of its properties.