Skip to main content
SpringerLink
Log in

Composition and Abstraction

  • Chapter
  • First Online:
Modeling and Verification of Parallel Processes (MOVEP 2000)

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

Included in the following conference series:

Abstract

This article is a tutorial on advanced automated processalgebraic verification of concurrent systems, and it is organised around a case study. The emphasis is on verification methods that rely on the inherent compositionality of process algebras. The fundamental concepts of labelled transition systems, strong bisimilarity, synchronous parallel composition, hiding, renaming, abstraction, CFFD-equivalence and CFFD-preorder are presented as the case study proceeds. The necessity of presenting assumptions about the users of the example system is discussed, and it is shown how CFFD-preorder supports their modelling. The assumptions are essential for the verification of so-called liveness properties. The correctness requirements of the system are stated, presented in linear temporal logic, and distributed to a number of more “localised” requirements. It is shown how they can be checked with the aid of suitably chosen CFFD-abstracted views to the system. The state explosion problem that hampers automatic verification is encountered. Compositional LTS construction, interface specifications and induction are used to solve the problem and, as a result, an infinite family of systems is verified with a limited amount of effort.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 52.95
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

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.

    Article  Google Scholar 

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

    Article  Google Scholar 

  3. 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.

    Article  MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

  5. Clarke, E. M., Grumberg, O. & Jha, S.: “Verifying Parameterized Networks using Abstraction and Regular Languages”. Proc.CONCUR’ 95, 6th International Conference on Concurrency Theory, Lecture Notes in Computer Science 962, Springer-Verlag 1995, pp. 395–407.

    Google Scholar 

  6. Courcoubetis, C., Vardi, M., Wolper, P. & Yannakakis, M.: “Memory-Efficient Algorithms for the Verification of Temporal Properties”. Formal Methods in System Design 1 (1992), pp. 275–288.

    Article  Google Scholar 

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

    Article  Google Scholar 

  8. Gerth, R., Peled, D., Vardi, M. & Wolper, P.: “Simple On-the-fly Automatic Verification of Linear Temporal Logic”. Proc.Pr otocol Specification, Testing and Verification 1995, Chapman & Hall 1995, pp. 3–18.

    Google Scholar 

  9. Graf, S. & Steffen, B.: “Compositional Minimization of Finite State Processes”. Proc.Computer-A ided Verification’ 90, AMS-ACM DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 3, 1991, pp. 57–73.

    Google Scholar 

  10. Helovuo, J. & Valmari, A.: “Checking for CFFD-Preorder with Tester Processes”. Proc.T ACAS 2000, Tools and Algorithms for the Construction and Analysis of Systems, 6th International Conference, Lecture Notes in Computer Science 1785, Springer-Verlag 2000, pp. 283–298.

    Chapter  Google Scholar 

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

    Google Scholar 

  12. Holzmann, G. J.: Design and Validation of Computer Protocols. Prentice-Hall 1991, 500 p.

    Google Scholar 

  13. ISO 8807 International Standard: Information processing systems-Open Systems Interconnection-LOTOS-A formal description technique based on the temporal ordering of observational behaviour. International Organization for Standardization 1989, 142 p.

    Google Scholar 

  14. Jard, C. & Jeron, T.: “On-Line Model Checking for Finite Linear Temporal Logic Specifications”. Proc.International Workshop on Automatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science 407, Springer-Verlag 1990, pp. 189–196.

    Google Scholar 

  15. Kaivola, R.: “Using Compositional Preorders in the Verification of Sliding Window Protocol”. Proc.Computer Aided Verification 1997, Lecture Notes in Computer Science 1254, Springer-Verlag 1997, pp. 48–59.

    Google Scholar 

  16. Kaivola, R. & Valmari, A.: “The Weakest Compositional Semantic Equivalence Preserving Nexttime-less Linear Temporal Logic”. Proc.CONCUR’ 92, Third International Conference on Concurrency Theory, Lecture Notes in Computer Science 630, Springer-Verlag 1992, pp. 207–221.

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  18. Karvi, T.: Partially Defined Lotos Specifications and their Refinement Relations. Ph.D. Thesis, Report A-2000-5, Department of Computer Science, University of Helsinki, Finland, Helsinki University Printing House 2000, 157 p.

    Google Scholar 

  19. Kokkarinen, I.: Reduction of Parallel Labelled Transition Systems with Stubborn Sets. M. Sc. (Eng.) Thesis (in Finnish), Tampere University of Technology, Finland, 1995, 49 p.

    Google Scholar 

  20. Kurshan, R. P., Merritt, M., Orda, A. & Sachs, S. R.: “A Structural Linearization Principle for Processes”. Formal Methods in System Design 5, 1994, pp. 227–244.

    Article  Google Scholar 

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

    Google Scholar 

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

    MathSciNet  Google Scholar 

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

    Google Scholar 

  24. Olderog, E.-R. & Hoare, C. A. R.: “Specification-Oriented Semantics for Communicating Processes”. Acta Informatica 23 (1986) 9–66.

    Article  MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

  26. Puhakka, A. & Valmari, A.: “Weakest-Congruence Results for Livelock-Preserving Equivalences”. Proc.CONCUR’ 99 (Concurrency Theory), Lecture Notes in Computer Science 1664, Springer-Verlag 1999, pp. 510–524.

    Google Scholar 

  27. Roscoe, A. W.: “Model-Checking CSP”. A Classical Mind: Essays in Honour of C.A.R.Ho are, Prentice-Hall 1994, pp. 353–378.

    Google Scholar 

  28. Roscoe, A. W.: The Theory and Practice of Concurrency. Prentice-Hall 1998, 565 p.

    Google Scholar 

  29. Schmidt, K.: “Stubborn Sets for Standard Properties”. Proc.Applic ation and Theory of Petri Nets 1999, Lecture Notes in Computer Science 1639, Springer-Verlag 1999, pp. 46–65.

    Chapter  Google Scholar 

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

    Google Scholar 

  31. Valmari, A.: “On-the-fly Verification with Stubborn Sets”. Proc.Computer-A ided Verification (CAV)’ 93, Lecture Notes in Computer Science 697, Springer-Verlag 1993, pp. 397–408.

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

  34. Valmari, A.: “Stubborn Set Methods for Process Algebras”. Proc.POMIV’96, Workshop on Partial Order Methods in Verification, DIMACS Series in Discrete Mathematics and Theoretical Computer Science Vol. 29, American Mathematical Society 1997, pp. 213–231.

    MathSciNet  Google Scholar 

  35. Valmari, A.: “The State Explosion Problem”. Lectures on Petri Nets I: Basic Models, Lecture Notes in Computer Science 1491, Springer-Verlag 1998, pp. 429–528.

    Google Scholar 

  36. Valmari, A.: “A Chaos-Free Failures Divergences Semantics with Applications to Verification”. Millennial Perspectives in Computer Science, Proceedings of the 1999 Oxford-Microsoft Symposium in Honour of sir Tony Hoare, Palgrave 2000, pp. 365–382.

    Google Scholar 

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

    Chapter  Google Scholar 

  38. Valmari, A. & Kokkarinen, I.: “Unbounded Verification Results by Finite-State Compositional Techniques: 10anyStates and Beyond”. Proc.1998 International Conference on Application of Concurrency to System Design, IEEE Computer Society 1998, pp. 75–85.

    Google Scholar 

  39. Valmari, A. & Setälä, M.: “Visual Verification of Safety and Liveness”. Proc.F ormal Methods Europe’ 96: Industrial Benefit and Advances in Formal Methods, Lecture Notes in Computer Science 1051, Springer-Verlag 1996, pp. 228–247.

    Google Scholar 

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

    Google Scholar 

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

    Article  MATH  Google Scholar 

  42. Vardi, M. Y. & Wolper, P.: “An Automata-Theoretic Approach to Automatic Program Verification”. Proc.1st Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press 1986, pp. 332–344.

    Google Scholar 

  43. 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 

  44. Wolper, P. & Lovinfosse, V.: “Verifying Properties of Large Sets of Processes with Network Invariants”. Proc.Workshop on Automatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science 407, Springer-Verlag 1989, pp. 68–80.

    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

Editors and Affiliations

  1. IRCCyN, CNRS, 1 rue de la Noe, 44321, Nantes Cedex 3, France

    Franck Cassez

  2. IRISA, CNRS, Campus de Beaulieu, 35042, Rennes, France

    Claude Jard

  3. Laboratoire de Recherche en Informatique, Université de Paris XI, Bâtiment 490, 91405, Orsay Cedex, France

    Brigitte Rozoy

  4. School of Computer Science, University of Birmingham, Edgbaston, Birmingham, B15 2TT, UK

    Mark Dermot Ryan

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Valmari, A. (2001). Composition and Abstraction. In: Cassez, F., Jard, C., Rozoy, B., Ryan, M.D. (eds) Modeling and Verification of Parallel Processes. MOVEP 2000. Lecture Notes in Computer Science, vol 2067. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45510-8_3

Download citation

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

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-42787-2

  • Online ISBN: 978-3-540-45510-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation