Compositional State Space Generation from Lotos Programs

Jean-Pierre Krimm and Laurent Mounier

Proceedings of TACAS'97 Tools and Algorithms for the Construction and Analysis of Systems (University of Twente, Enschede, The Netherlands), April 1997

Extended version with proofs available as Research Report VERIMAG RR97-01.

Abstract:

This paper describes a compositional approach to generate the labeled transition system representing the behaviour of a Lotos program by repeatedly alternating composition and reduction operations on subsets of its processes. To restrict the size of the intermediate LTSs generated, we generalize to the LOTOS parallel composition operator the results proposed in [Graf-Steffen-90], which consist in representing the environment of a process as an interface, i.e., a set of "autorized" execution sequences. This generalization allows to handle both user-given interfaces and automatically computed ones. This compositional method has been implemented within the CADP toolbox and experimented on several realistic case studies.

20 pages

PDF

PostScript