PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Bouali A., Gnesi S., Larosa S. Jack: just another concurrency kit : the integration project. In: Bulletin of the European Association for Theoretical Computer Science, vol. 54 pp. 207 - 224. EATCS, 1994.
 
 
Abstract
(English)
JACK, standing for Just Another Concurrency Kit, isa 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, analysisand verification of concurrent 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, ACTL, is used to describe the properties that a specification must satisfy, and model checking of ACTL formulae on the specification is performed in linear time. A translator from Natural Linguage to ACTL formulae is provided, in order to simplify the job of describing specification properties by ACTL formulae. A description of the graphical interface is given together with its functionalities and the exchange format used by the tools.
Subject JACK
verification
D.2.4 Software/Program Verification


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