A case study within Jack

The JACK Environment [4] is an integrated system for specification and verification of concurrent systems that are modelled by finite-state Labelled Transition Systems. Within JACK the user is able to study such systems, specifying them by some process algebra [1,2, 12]and after manipulating the algebra terms in various ways. Then, logical properties of the specification can be checked by means of a model checker, or behavioural properties can be verificated by other tools. There is the possibility, too, to use a graphical tool to initially layout the specification and to have some graphical feedback from the various phases of the specification framework. The idea that is the corner stone of the JACK project is to make an integration among a set of tools that share a common format for the automata description, i.e. the Fc2 format [13]. Such tools offer various functionalities, and JACK, that rises from their integration,is able to use such functlonalities and to create some composed ones. So, JACK isable to cover a large extent of the formal software development process, such as formalization of requirements [9], rewriting techniques [6], behavioural equivalence proofs [11, 7], graph transformations [10], logic verifications. The logical properties are specified by an action based temporal logic, ACTL [7], suitable to express safety and liveness properties of reactive systems modelled by Labelled Transition Systems.