Compositional State Space Generation from Lotos Programs

. This paper describes a compositional approach to generate the labeled transition system representing the behavior 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 [GS90], which consist in representing the environment of a process by an interface, i.e., a set of "authorized" execution sequences. This generalization allows to handle both user-given interfaces and automatically computed ones. This compositional generation method has been implemented within the Cadp toolbox and experimented on several realistic case-studies. Introduction Formal verification is a part of software engineering that consists in evaluating a set of specifications on a formal description of a program. When this program is "finite state", which happens in particular when considering only essential features of par..