PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Bouali A., Gnesi S., Larosa S. The integration project for the jack environment. Internal note IEI-B4-15, 1994.
 
 
Abstract
(English)
JACK, standing for Just Another Concurrency Kit, is a new 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 cuncurrent systems specified using process algebra. Tools exchange information through a text format called Fc2. Users are able to graphically layout their specifications, 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, ACTIVE, is used to describe the properties that a specification must satisfy, and a model checking of ACTI, formulae on the specification is performed in linear time. A translator from Natural Language to ACTI, furmulae is provided, in order to simplify the job of describing specification properties by ACTI, formulae. A description of the graphical interface is given together with its functionalities and the exchange format used by the tools.
Subject Specification tools
Verification tools
Reactive systems
Integrated environment
Methodology
Bisimulation
Model checking
D.2.4 Software/Program Verification. Model checking


Icona documento 1) Download Document PDF


Icona documento Open access Icona documento Restricted Icona documento Private

 


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional