Istituto di Scienza e Tecnologie dell'Informazione     
Fantechi A., Gnesi S., Leporatti M., Ristori G. Model checking for LOTOS. In: 2nd Lotosphere Workshop. (Berlin, Germany, 16 - 17 May 1991). Proceedings, pp. 1 - 11. 1991.
In this paper we present a prototypal environment to analyse LOTOS specifications, based on the integration between Squiggles, an equivalence verifier, and EMC, a model cheker for CTL formulae. Hence, the functionalities of our environment range from the reduction of a finite state LOTOS specification into its corresponding Labelled Transition System, possibly minimized with respect to an equivalence relation, to the verification of equivalence between specifications and to the check of validity of properties expressed in a temporal logic as CTL.
Subject LOTOS
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