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.
Chapter PDF
Similar content being viewed by others
References
ISO (1989) IS8807: Information Processing Systems, Open Systems Interconnection, LOTOS - A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour.
Bolognesi T. and Caneve M. (1989) Equivalence verification:theory, algorithms and a tool in The formal description technique LOTOS, Elsevier Science.
Bryant R.E. (1986) Graph-based Algorithms for Boolean Function Manipulation, IEEE Trans. on Computers, 35, 677–691.
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.
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.
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.
Garavel H., and Najm E. (1989) TILT: from LOTOS to labelled transition systems, in The formal description technique LOTOS, Elsevier Science.
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.
Holzmann G.J. (1994) An Improvement in Formal Verification, in Proc. of 7th Int. Conference on Formal Description Techniques, Berne, Switzerland.
Nicollin X., Sifakis J., Yovine S. (1992) Compiling Real-Time Specifications into Extended Automata, IEEE Trans. on Software Engineering, 18, 794–804
Quemada J. (1992) Compressed State Space Representation in LOTOS with the Interleaved Expansion, in Protocol Specification, Testing and Verification XI, Elsevier Science.
Valmari A. (1990) A Stubborn Attack on State Explosion, in 2nd Int. Conf. on Computer Aided Verification, Dimacs Series.
West H.C. (1986) Protocol validation by random state exploration, in Protocol Specification, Testing, and Verification VI, Elsevier Science.
Winksel G. (1989) An Introduction to Event Structures, LNCS 35.4, 364–397, Springer-Verlag.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1996 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Sisto, R. (1996). A method to build symbolic representations of LOTOS specifications. In: Dembiński, P., Średniawa, M. (eds) Protocol Specification, Testing and Verification XV. PSTV 1995. IFIP Advances in Information and Communication Technology. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-34892-6_21
Download citation
DOI: https://doi.org/10.1007/978-0-387-34892-6_21
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-5041-2925-1
Online ISBN: 978-0-387-34892-6
eBook Packages: Springer Book Archive