Abstract
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.
An extended version can be found in [KM97].
Chapter PDF
Keywords
- Parallel Composition
- Label Transition System
- Execution Sequence
- Context Constraint
- Compositional Generation
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
André Arnold. MEC: A System for Constructing and Analysing Transition Systems. In Joseph Sifakis, editor, Proceedings of the 1st Workshop on Automatic Verification Methods for Finite State Systems (Grenoble, France), volume 407 of Lecture Notes in Computer Science, pages 117–132. Springer Verlag, June 1989.
Simon Bainbridge and Laurent Mounier. Specification and Verification of a Reliable Multicast Protocol. Technical Report HPL-91-163, Hewlett-Packard Laboratories, Bristol, U.K., October 1991.
S.C. Cheung and J. Kramer. Enhancing Compositional Reachability Analysis with Context Constraints. In Proceedings of the 1st ACM International Symposium on the Foundations of Software Engineering, pages 115–125, Los Angeles, California, December 1993.
S.C. Cheung and J. Kramer. Compositional Reachability Analysis of Finite-State Distributed Systems with User-Specified Constraints. In Proceedings of SIGSOFT'95, 1995.
R. Cleaveland, J. Parrow, and B. Steffen. The Concurrency Workbench. In J. Sifakis, editor, Proceedings of the 1st Workshop on Automatic Verification Methods for Finite State Systems (Grenoble, France), volume 407 of Lecture Notes in Computer Science, pages 24–37. Springer Verlag, June 1989.
Jean-Claude Fernandez. An Implementation of an Efficient Algorithm for Bisimulation Equivalence. Science of Computer Programming, 13(2–3):219–236, May 1990.
J.C. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier, and M. Sighireanu. CADP: A Protocol Validation and Verification Toolbox. In Rajeev Alur and Thomas A. Henzinger, editors, Proceedings of the 8th Conference on Computer-Aided Verification (New Brunswick, New Jersey, USA), August 1996.
J.C. Fernandez, A. Kerbrat, and L. Mounier. Symbolic Equivalence Checking. In C. Courcoubetis, editor, Proceedings of the 5th Workshop on Computer-Aided Verification (Heraklion, Greece), volume 697 of Lecture Notes in Computer Science. Springer Verlag, June 1993.
S. Graf, G. Lüttgen, and B. Steffen. Compositional Minimisation of Finite State Systems using Interface Specifications. Formal Aspects of Computation, 3, 1996. appeared as Passauer Informatik Bericht MIP-9505.
Hubert Garavel and Laurent Mounier. Specification and Verification of various Distributed Leader Election Algorithms for Unidirectional Ring Networks. Science of Computer Programming, 1996. Special issue on Industrially Relevant Applications of Formal Analysis Techniques. Full version available as INRIA Research Report 2986.
Susanne Graf and Bernhard Steffen. Compositional Minimization of Finite State Processes. In Workshop on Computer-Aided Verification, Rutgers, USA, June 1990. DIMACS, R.P. Kurshan and E.M. Clarke.
Jan Friso Groote and Frits Vaandrager. An Efficient Algorithm for Branching Bisimulation and Stuttering Equivalence. In M. S. Patterson, editor, Proceedings of the 17th ICALP (Warwick), volume 443 of Lecture Notes in Computer Science, pages 626–638. Springer Verlag, 1990.
C. A. R. Hoare. Communicating Sequential Processes. Communications of the ACM, 21(8):666–677, August 1978.
Gerard J. Holzmann. Design and Validation of Computer Protocols. Software Series. Prentice Hall, 1991.
ISO/IEC. LOTOS — A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. International Standard 8807, International Organization for Standardization — Information Processing Systems — Open Systems Interconnection, Genève, September 1988.
Jean-Pierre Krimm and Laurent Mounier. Compositional State Space Generation from Lotos Programs. Technical Report RR97-01, VER-IMAG, January 1997.
P. Kanellakis and S. Smolka. CCS Expressions, Finite State Processes and Three Problems of Equivalence. Information and Computation, 86(1), May 1990.
Robin Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer Verlag, 1980.
Rocco De Nicola, Ugo Montanari, and Frits Vaandrager. Back and Forth Bisimulations. CS R9021, Centrum voor Wiskunde en Informatica, Amsterdam, May 1990.
David Park. Concurrency and Automata on Infinite Sequences. In Peter Deussen, editor, Theoretical Computer Science, volume 104 of Lecture Notes in Computer Science, pages 167–183. Springer Verlag, March 1981.
Robert Paige and Robert E. Tarjan. Three Partition Refinement Algorithms. SIAM Journal of Computing, 16(6):973–989, December 1987.
Valérie Roy and Robert de Simone. Auto/Autograph. In R. P. Kurshan and E. M. Clarke, editors, Proceedings of the 2nd Workshop on Computer-Aided Verification (Rutgers, New Jersey, USA), volume 3 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 477–491. AMS-ACM, June 1990.
Santosh K. Shrivastava and Paul. D. Ezhilchelvan. rel/REL: A Family of Reliable Multicast Protocol for High-Speed Networks. Technical Report, University of Newcastle, Dept. of Computer Science, U.K, 1990.
Antti Valmari. Compositionality in State Space Verification. In Application and Theory of Petri Nets, volume 1091 of Lecture Notes in Computer Science, pages 29–56. Springer Verlag, June 1996.
R. J. van Glabbeek and W. P. Weijland. Branching-Time and Abstraction in Bisimulation Semantics (extended abstract). CS R8911, Centrum voor Wiskunde en Informatica, Amsterdam, 1989. Also in proc. IFIP 11th World Computer Congress, San Francisco, 1989
C. Vissers, G. Scollo, M. van Sinderen, and E. Brinksma. On the use of specification styles in the design of distributed systems. Theoretical Computer Science, 89(1):179–206, October 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Krimm, JP., Mounier, L. (1997). Compositional state space generation from Lotos programs. In: Brinksma, E. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1997. Lecture Notes in Computer Science, vol 1217. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0035392
Download citation
DOI: https://doi.org/10.1007/BFb0035392
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62790-6
Online ISBN: 978-3-540-68519-7
eBook Packages: Springer Book Archive