LORETO: a tool for reducing state explosion in verification of LOTOS programs

Citation
R. Barbuti et al., LORETO: a tool for reducing state explosion in verification of LOTOS programs, SOFTW PR EX, 29(12), 1999, pp. 1123-1147
Citations number
34
Categorie Soggetti
Computer Science & Engineering
Journal title
SOFTWARE-PRACTICE & EXPERIENCE
ISSN journal
00380644 → ACNP
Volume
29
Issue
12
Year of publication
1999
Pages
1123 - 1147
Database
ISI
SICI code
0038-0644(199910)29:12<1123:LATFRS>2.0.ZU;2-B
Abstract
LOTOS is a formal specification language for concurrent and distributed sys tems. Basic LOTOS is the version of LOTOS without value-passing. A widely u sed approach to the verification of temporal properties is model checking. Often, in this approach the formal specification is translated into a label ed transition system on which formulae expressing properties are checked. A problem with this verification technique is state explosion: concurrent sy stems are often represented by automata with a prohibitive number of states . In this paper we show how, given a set rho of actions, it is possible to automatically obtain for a Basic LOTOS program a reduced transition system to which only the arcs labeled by actions in rho belong. The set rho of act ions plays a fundamental role in conjunction with a temporal logic defined by the authors in a previous paper: selective mu-calculus. The reduced syst em with respect to rho preserves the truth value of all selective mu-calcul us formulae with actions from the set rho. We act at both syntactic and sem antic levels. From a syntactic point of view, we define a set of transforma tion rules obtaining a smaller program. On the semantic side, we define a n on-standard semantics which dynamically reduces the transition system durin g generation, We present a tool implementing both the syntactic and the sem antic reduction. Copyright (C) 1999 John Wiley & Sons, Ltd.