Advertisement

A method to build symbolic representations of LOTOS specifications

  • Riccardo Sisto
Chapter
Part of the IFIP Advances in Information and Communication Technology book series (IFIPAICT)

Abstract

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.

Keywords

Protocol Engineering LOTOS Symbolic Model Checking Binary Decision Diagrams. 

References

  1. ISO (1989) IS8807: Information Processing Systems, Open Systems Interconnection, LOTOS - A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour.Google Scholar
  2. Bolognesi T. and Caneve M. (1989) Equivalence verification:theory, algorithms and a tool in The formal description technique LOTOS, Elsevier Science.Google Scholar
  3. Bryant R.E. (1986) Graph-based Algorithms for Boolean Function Manipulation, IEEE Trans. on Computers, 35, 677–691.CrossRefzbMATHGoogle Scholar
  4. Burch J.R., Clarke E.M., Long D.E., McMillan K.L., Dill D.L. (1994) Symbolic Model Checking for Sequential Circuit Verification, IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems, 13, 401–424.CrossRefGoogle Scholar
  5. 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
  6. 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
  7. Garavel H., and Najm E. (1989) TILT: from LOTOS to labelled transition systems, in The formal description technique LOTOS, Elsevier Science.Google Scholar
  8. 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
  9. Holzmann G.J. (1994) An Improvement in Formal Verification, in Proc. of 7th Int. Conference on Formal Description Techniques, Berne, Switzerland.Google Scholar
  10. Nicollin X., Sifakis J., Yovine S. (1992) Compiling Real-Time Specifications into Extended Automata, IEEE Trans. on Software Engineering, 18, 794–804CrossRefGoogle Scholar
  11. Quemada J. (1992) Compressed State Space Representation in LOTOS with the Interleaved Expansion, in Protocol Specification, Testing and Verification XI, Elsevier Science.Google Scholar
  12. Valmari A. (1990) A Stubborn Attack on State Explosion, in 2nd Int. Conf. on Computer Aided Verification, Dimacs Series.Google Scholar
  13. West H.C. (1986) Protocol validation by random state exploration, in Protocol Specification, Testing, and Verification VI, Elsevier Science.Google Scholar
  14. Winksel G. (1989) An Introduction to Event Structures, LNCS 35.4, 364–397, Springer-Verlag.Google Scholar

Copyright information

© IFIP International Federation for Information Processing 1996

Authors and Affiliations

  • Riccardo Sisto
    • 1
  1. 1.Dip. di Automatica e Informatica, Politecnico di TorinoPolitecnico di TorinoTorinoItaly

Personalised recommendations