A method to build symbolic representations of LOTOS specifications
A symbolic representation of a large state/transition system, based on Binary Decision Diagrams (BDD’s), is generally much more compact than an explicit representation like a Labelled Transition System (LTS). This is due to regular and repetitive patterns occurring in state/transition systems. By exploiting this property, huge state spaces can be represented symbolically, and the resulting BDD representations can be profitably used for activities such as model checking and sequential circuit synthesis. This paper presents a method to build BDD representations from process algebraic specifications, taking LOTOS as a reference. The method exploits the compositionality of process algebras to avoid the enumeration of all the states and transitions. First, small labelled transition systems are created for representing the basic building blocks of the specification. These are converted to BDDs, which in turn are combined together, according to the various process algebraic operators, to obtain the overall BDD. An example is used throughout the paper to illustrate the method.
KeywordsProtocol Engineering LOTOS Symbolic Model Checking Binary Decision Diagrams.
- ISO (1989) IS8807: Information Processing Systems, Open Systems Interconnection, LOTOS - A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour.Google Scholar
- Bolognesi T. and Caneve M. (1989) Equivalence verification:theory, algorithms and a tool in The formal description technique LOTOS, Elsevier Science.Google Scholar
- Cousot P., and Cousot R. (1977) Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints, in Proc. of !th ACM Symp. on Principles of Programming Languages, pp. 238–252.Google Scholar
- Fernandez J.C., Jard C., Jeron T., and Mounier L. (1992) On the fly verification of finite transition systems, in Formal Methods in System Design, Kluwer Academic Publishers.Google Scholar
- Garavel H., and Najm E. (1989) TILT: from LOTOS to labelled transition systems, in The formal description technique LOTOS, Elsevier Science.Google Scholar
- Higashino Y., Yasumoto K., Kitamichi J., and Taniguchi K. (1994) Hardware Synthesis from a Restricted Class of LOTOS Expressions, in Protocol Specification, Testing and Verification XIV, Chapman amp; Hall.Google Scholar
- Holzmann G.J. (1994) An Improvement in Formal Verification, in Proc. of 7th Int. Conference on Formal Description Techniques, Berne, Switzerland.Google Scholar
- Quemada J. (1992) Compressed State Space Representation in LOTOS with the Interleaved Expansion, in Protocol Specification, Testing and Verification XI, Elsevier Science.Google Scholar
- Valmari A. (1990) A Stubborn Attack on State Explosion, in 2nd Int. Conf. on Computer Aided Verification, Dimacs Series.Google Scholar
- West H.C. (1986) Protocol validation by random state exploration, in Protocol Specification, Testing, and Verification VI, Elsevier Science.Google Scholar
- Winksel G. (1989) An Introduction to Event Structures, LNCS 35.4, 364–397, Springer-Verlag.Google Scholar