Skip to main content
SpringerLink
Log in

Compositionality in state space verification methods

  • Invited Papers
  • Conference paper
  • First Online:
Application and Theory of Petri Nets 1996 (ICATPN 1996)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1091))

Included in the following conference series:

Abstract

The purpose of this article is to introduce the concepts and ideas that are necessary for understanding computerised process-algebraic compositional verification. Furthermore, by describing two recent case studies an attempt is made to demonstrate the power of the compositional approach and to describe some advanced ways of using the basic techniques. The case studies are given first so that the basic concepts may be introduced in an informal manner. Then the article attempts to elucidate the process-algebraic way of modelling systems and their behaviours. The idea of compositionality is explained. The most important process-algebraic semantic models are described in detail and related to each other, paying special emphasis on algorithmic issues. The representation is at the semantic and state space level; process-algebraic languages are not discussed. Therefore, the techniques presented should be immediately applicable to a wide range of formalisms that can be given semantics in terms of state spaces and transition occurrences.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bartlett, K. A., Scantlebury, R. A. & Wilkinson, P. T.: A Note on Reliable Full-Duplex Transmission over Half-Duplex Links. Communications of the ACM 12 (5) 1969, pp. 260–261.

    Google Scholar 

  2. Bergstra, J. A. & Klop., J. W.: Process Theory Based on Bisimulation Semantics. Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, Lecture Notes in Computer Science 354, Springer-Verlag 1989, pp. 50–122.

    Google Scholar 

  3. Bergstra, J. A., Klop, J. W. & Olderog, E.-R.: Failures Without Chaos: A New Process Semantics for Fair Abstraction. Formal Description of Programming Concepts III, North-Holland 1987, pp. 77–103.

    Google Scholar 

  4. Bolognesi, T. & Brinksma, E.: Introduction to the ISO Specification Language LOTOS. Computer Networks and ISDN Systems 14 1987 pp. 25–59.

    Google Scholar 

  5. Bolognesi, T. & Smolka, S. A.: Fundamental Results for the Verification of Observational Equivalence: a Survey. Proc. Protocol Specification, Testing and Verification VII, North-Holland 1988, pp. 165–179.

    Google Scholar 

  6. Brand, D. & Joyner, W. H.: Verification of HDLC. IEEE Transactions on Communications, Vol. 30, no. 5, 1982, pp. 1136–1142.

    Google Scholar 

  7. Brinksma, E.: A Theory for the Derivation of Tests. Proc. Protocol Specification, Testing and Verification VIII, North-Holland 1988, pp. 63–74.

    Google Scholar 

  8. Brookes, S. D., Hoare, C. A. R. & Roscoe, A. W.: A Theory of Communicating Sequential Processes. Journal of the ACM, 31 (3) 1984, pp. 560–599.

    Google Scholar 

  9. Brookes, S. D. & Roscoe, A. W.: An Improved Failures Model for Communicating Sequential Processes. Proc. NSF-SERC Seminar on Concurrency, Lecture Notes in Computer Science 197, Springer-Verlag 1985, pp. 281–305.

    Google Scholar 

  10. Brookes, S. D. & Rounds, W. C.: Behavioural Equivalence Relationships Induced by Programming Logics. Proc. 10th International Colloquium on Automata, Languages, and Programming, Lecture Notes in Computer Science 154, Springer-Verlag 1983, pp. 97–108.

    Google Scholar 

  11. Cheung, S. C. & Kramer, J.: Enhancing Compositional Reachability Analysis with Context Constraints. Proc. ACM SIGSOFT '93: Symposium on the Foundations of Software Engineering, ACM Software Engineering Notes Vol. 18 Nr 5, 1993, pp. 115–125.

    Google Scholar 

  12. Clarke, E. M., Emerson, E. A. & Sistla, A. P.: Automatic Verification of Finite State Concurrent Systems Using Temporal Logic. ACM Transactions on Programming Languages and Systems, 8 (2) 1986, pp. 244–263.

    Google Scholar 

  13. Cleaveland, R. & Hennessy, M.: Testing Equivalence as a Bisimulation Equivalence. Proc. Workshop on Automatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science 407, Springer-Verlag 1990, pp. 11–23.

    Google Scholar 

  14. Cleaveland, R., Parrow, J. & Steffen, B.: The Concurrency Workbench. Proc. Workshop on Automatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science 407, Springer-Verlag 1990, pp. 24–37.

    Google Scholar 

  15. Darondeau, P. & Gamatie, B.: Infinitary Behaviours and Infinitary Observations. Fundamenta Informaticae XIII (1990) pp. 353–386.

    Google Scholar 

  16. De Nicola, R. & Vaandrager, F.: Three Logics for Branching Bisimulation. Report CSR9012, Centrum voor Wiskunde en Informatica, Amsterdam 1990.

    Google Scholar 

  17. Eloranta, J.: Minimizing the Number of Transitions with Respect to Observation Equivalence. BIT 31 (1991) pp. 576–590.

    Google Scholar 

  18. Eloranta, J.: Minimal Transition Systems with Respect to Divergence Preserving Behavioural Equivalences. PhD Thesis, University of Helsinki, Department of Computer Science, Report A-1994-1, Helsinki, Finland 1994, 162 p.

    Google Scholar 

  19. Emerson, E. A.: Temporal and Modal Logic. Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, Elsevier Science Publishers 1990, pp. 995–1072.

    Google Scholar 

  20. Fernandez, J.-C.: An Implementation of an Efficient Algorithm for Bisimulation Equivalence. Science of Computer Programming 13 (1989/90) pp. 219–236.

    Google Scholar 

  21. Garey, M. R. & Johnson, D. S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman and Company, 1979, 340 p.

    Google Scholar 

  22. Gerth, R., Kuiper, R., Peled, D. & Penczek, W.: A Partial Order Approach to Branching Time Model Checking. Proc. Third Israeli Symposium on the Theory of Computing Systems, 1994.

    Google Scholar 

  23. Graf, S. & Steffen, B.: Compositional Minimization of Finite State Processes. Proc. Computer-Aided Verification '90, AMS-ACM DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 3, American Mathematical Society 1991, pp. 57–73.

    Google Scholar 

  24. Groote, J. F. & Vaandrager, F: An Efficient Algorithm for Branching Bisimulation and Stuttering Equivalence. Proc. 17th International Colloquium on Automata, Languages, and Programming, Lecture Notes in Computer Science 443, Springer-Verlag 1990, pp. 626–638.

    Google Scholar 

  25. Hennessy, M.: Acceptance Trees. Journal of the ACM 32 (4) 1985, pp. 896–928.

    Google Scholar 

  26. Hoare, C. A. R.: Communicating Sequential Processes. Prentice-Hall 1985, 256 p.

    Google Scholar 

  27. Inverardi, P. & Priami, C.: Evaluation of Tools for the Analysis of Communicating Systems. EATCS Bulletin 45, October 1991, pp. 158–185.

    Google Scholar 

  28. Kaivola, R.: Equivalences, Preorders and Compositional Verification for Linear Time Temporal Logic and Concurrent Systems. PhD Thesis, University of Helsinki, Department of Computer Science, Report A-1996-1, Helsinki, Finland 1996, 185 p.

    Google Scholar 

  29. Kaivola, R. & Valmari, A.: The Weakest Compositional Semantic Equivalence Preserving Nexttime-less Linear Temporal Logic. Proc. CONCUR '92, Lecture Notes in Computer Science 630, Springer-Verlag 1992, pp. 207–221.

    Google Scholar 

  30. Kanellakis, P. C. & Smolka, S. A.: CCS Expressions, Finite State Processes, and Three Problems of Equivalence. Information and Computation 86 (1990) pp. 43–68.

    Google Scholar 

  31. Madelaine, E. & Vergamini, D.: AUTO: A Verification Tool for Distributed Systems Using Reduction of Finite Automata Networks. Proc. Formal Description Techniques II (FORTE '89), North-Holland 1990, pp. 61–66.

    Google Scholar 

  32. Manna, Z. & Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag 1992, 427 p.

    Google Scholar 

  33. Milner, R.: Communication and Concurrency. Prentice-Hall 1989, 260 p.

    Google Scholar 

  34. Park, D.: Concurrency and Automata on Infinite Sequences. 5th GI Conference on Theoretical Computer Science, Lecture Notes in Computer Science 104, Springer-Verlag 1981, pp. 167–183.

    Google Scholar 

  35. Richier, J. L., Rodriguez, C., Sifakis, J. & Voiron, J.: Verification in Xesar of the Sliding Window Protocol. Proc. Protocol Specification, Testing and Verification VII, North-Holland 1988, pp. 235–248.

    Google Scholar 

  36. Roscoe, A. W.: Model-Checking CSP. A Classical Mind: Essays in Honour of C. A. R. Hoare, Prentice-Hall 1994, pp. 353–378.

    Google Scholar 

  37. Sabnani, K. K., Lapone, A. M. & Uyar, M. Ü.: An Algorithmic Procedure for Checking Safety Properties of Protocols. IEEE Transactions on Communications, Vol. 37, no. 9, 1989, pp. 940–948.

    Google Scholar 

  38. Savola, R.: A State Space Generation Tool for LOTOS Specifications. VTT Publications 241, Technical Research Centre of Finland (VTT), Espoo, Finland 1995, 107 p.

    Google Scholar 

  39. Stenning, N. V.: A Data Transfer Protocol. Computer Networks, vol. 11, 1976, pp. 99–110.

    Google Scholar 

  40. Valmari, A.: Alleviating State Explosion during Verification of Behavioural Equivalence. Department of Computer Science, University of Helsinki, Report A-1992-4, Helsinki, Finland 1992, 57 p.

    Google Scholar 

  41. Valmari, A.: Compositional State Space Generation. Advances in Petri Nets 1993, Lecture Notes in Computer Science 674, Springer-Verlag 1993, pp. 427–457.

    Google Scholar 

  42. Valmari, A.: On-the-fly Verification with Stubborn Sets. Proc. Computer-Aided Verification '93, Lecture Notes in Computer Science 697, Springer-Verlag 1993, pp. 397–408.

    Google Scholar 

  43. Valmari, A.: Compositional Analysis with Place-Bordered Subnets. Proc. Application and Theory of Petri Nets 1994, Lecture Notes in Computer Science 815, Springer-Verlag 1994, pp. 531–547.

    Google Scholar 

  44. Valmari, A.: The Weakest Deadlock-Preserving Congruence. Information Processing Letters 53 (1995) 341–346.

    Google Scholar 

  45. Valmari, A.: Failure-based Equivalences Are Faster Than Many Believe. Proc. Structures in Concurrency Theory, Springer-Verlag “Workshops in Computing” series 1995, pp. 326–340.

    Google Scholar 

  46. Valmari, A., Karsisto, K. & Setälä, M.: Visualisation of Reduced Abstracted Behaviour as a Design Tool. Proc. PDP'96, the Fourth Euromicro Workshop on Parallel and Distributed Processing, IEEE Computer Society Press 1996, pp. 187–194.

    Google Scholar 

  47. Valmari, A., Kemppainen, J., Clegg, M. & Levanto, M.: Putting Advanced Reachability Analysis Techniques Together: the “ARA” Tool. Proc. Formal Methods Europe '93, Lecture Notes in Computer Science 670, Springer-Verlag 1993, pp. 597–616.

    Google Scholar 

  48. Valmari, A. & Setälä, M.: Visual Verification of Safety and Liveness. Proc. Formal Methods Europe '96, Lecture Notes in Computer Science 1051, Springer-Verlag 1996, pp. 228–247.

    Google Scholar 

  49. Valmari, A. & Tienari, M.: An Improved Failures Equivalence for Finite-State Systems with a Reduction Algorithm. Protocol Specification, Testing and Verification XI, North-Holland 1991, pp. 3–18.

    Google Scholar 

  50. Valmari, A. & Tienari, M.: Compositional Failure-Based Semantic Models for Basic LOTOS. Formal Aspects of Computing (1995) 7:440–468.

    Google Scholar 

  51. van Glabbeek, R.: Comparative Concurrency Semantics and Refinement of Actions. PhD Thesis, Centrum voor Wiskunde en Informatica, Amsterdam 1990.

    Google Scholar 

  52. van Glabbeek, R.: The Linear Time — Branching Time Spectrum II: The Semantics of Sequential Systems with Silent Moves. Proc. CONCUR '93, Lecture Notes in Computer Science 715, Springer-Verlag 1993, pp. 66–81.

    Google Scholar 

  53. van Glabbeek, R. & Weijland, W.: Branching Time and Abstraction in Bisimulation Semantics (Extended Abstract). Proc. IFIP International Conference on Information Processing '89, North-Holland 1989, pp. 613–618.

    Google Scholar 

  54. Vardi, M. Y. & Wolper, P.: An Automata-theoretic Approach to Automatic Program Verification. Proc. IEEE Symposium on Logic in Computer Science, 1986, pp. 322–331.

    Google Scholar 

  55. Wolper, P.: Expressing Interesting Properties of Programs in Propositional Temporal Logic. Proc. 13th ACM Symposium on Principles of Programming Languages, 1986, pp. 184–193.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Software Systems Laboratory, Tampere University of Technology, PO Box 553, FIN-33101, Tampere, Finland

    Antti Valmari

Authors
  1. Antti Valmari
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jonathan Billington Wolfgang Reisig

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Valmari, A. (1996). Compositionality in state space verification methods. In: Billington, J., Reisig, W. (eds) Application and Theory of Petri Nets 1996. ICATPN 1996. Lecture Notes in Computer Science, vol 1091. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61363-3_3

Download citation

  • DOI: https://doi.org/10.1007/3-540-61363-3_3

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61363-3

  • Online ISBN: 978-3-540-68505-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation