Skip to main content
SpringerLink
Log in

View Abstraction for Systems with Component Identities

  • Conference paper
  • First Online:
Formal Methods (FM 2018)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10951))

Included in the following conference series:

Abstract

The parameterised verification problem seeks to verify all members of some family of systems. We consider the following instance: each system is composed of an arbitrary number of similar component processes, together with a fixed number of server processes; processes communicate via synchronous message passing; in particular, each component process has an identity, which may be included in messages, and passed to third parties. We extend Abdulla et al.’s technique of view abstraction, together with techniques based on symmetry reduction, to this setting. We give an algorithm and implementation that allows such systems to be verified for an arbitrary number of components. We show how this technique can be applied to a concurrent datatype built from reference-linked nodes, such as a linked list. Further, we show how to capture the specification of a queue or of a stack.

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 79.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 99.99
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

Notes

  1. 1.

    We write \(\mathbb {M}\) for a finite multiset type constructor. We mostly use set notation for multisets, but write “\(\uplus \)” for a multiset union.

  2. 2.

    The implementation and the scripts for the examples in the next section are available from www.cs.ox.ac.uk/people/gavin.lowe/ViewAbstraction/index.html.

References

  1. Abdulla, P., Haziza, F., Holík, L.: Parameterized verification through view abstraction. Int. J. Softw. Tools Technol. Transf. 18, 495–516 (2016)

    Article  Google Scholar 

  2. Abdulla, P.A., Jonsson, B., Nilsson, M., d’Orso, J.: Regular model checking made simple and effcient\(^{*}\). In: Brim, L., Křetínský, M., Kučera, A., Jančar, P. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 116–131. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45694-5_9

    Chapter  Google Scholar 

  3. Abdulla, P.A., Jonsson, B., Nilsson, M., Saksena, M.: A survey of regular model checking. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 35–48. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-28644-8_3

    Chapter  Google Scholar 

  4. Abdullah, P., Haziza, F., Holík, L., Jonsson, B., Rezine, A.: An integrated specification and verification technique for highly concurrent data structures. Int. J. Softw. Tools Technol. Transf. 19, 549–563 (2017)

    Article  Google Scholar 

  5. Apt, K.R., Kozen, D.C.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307–309 (1986)

    Article  MathSciNet  Google Scholar 

  6. Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract regular model checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 372–386. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27813-9_29

    Chapter  Google Scholar 

  7. Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 403–418. Springer, Heidelberg (2000). https://doi.org/10.1007/10722167_31

    Chapter  Google Scholar 

  8. Bošnački, D., Dams, D., Holenderski, L.: Symmetric spin. Int. J. Softw. Tools Technol. Transf. 4, 92–106 (2002)

    Article  Google Scholar 

  9. Clarke, E.M., Emerson, E.A., Jha, S., Sistla, A.P.: Symmetry reductions in model checking. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 147–158. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0028741

    Chapter  Google Scholar 

  10. Clarke, E.M., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. Formal Methods Syst. Des. 9, 77–104 (1996)

    Article  Google Scholar 

  11. Clarke, E.M., Grumberg, O.: Avoiding the state explosion problem in temporal logic model checking. In: Proceedings of the 6th Annual Association for Computing Machinery Symposium on Principles of Distributed Computing, pp. 294–303 (1987)

    Google Scholar 

  12. Dams, D., Lakhnech, Y., Steffen, M.: Iterating transducers. J. Logic Algebraic Program. 52–53, 109–127 (2002)

    Article  MathSciNet  Google Scholar 

  13. Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: Proceedings of the Symposium on Principles of Programming Languages (POPL 1995) (1995)

    Google Scholar 

  14. Emerson, E.A., Sistla, A.P.: Symmetry and model checking. Formal Methods Syst. Des. 9, 105–131 (1996)

    Article  Google Scholar 

  15. German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3), 675–735 (1992)

    Article  MathSciNet  Google Scholar 

  16. Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3: a parallel refinement checker for CSP. Int. J. Softw. Tools Technol. Transf. 18(2), 149–167 (2015)

    Article  Google Scholar 

  17. Gibson-Robinson, T., Lowe, G.: Symmetry Reduction in CSP Model Checking (2017, Submitted for publication). http://www.cs.ox.ac.uk/people/gavin.lowe/SymmetryReduction/

  18. Goldsmith, M., Moffat, N., Roscoe, B., Whitworth, T., Zakiuddin, I.: Watchdog transformations for property-oriented model-checking. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 600–616. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45236-2_33

    Chapter  Google Scholar 

  19. Ip, C.N., Dill, D.L.: Better verification through symmetry. Formal Methods Syst. Des. 9, 41–75 (1996)

    Article  Google Scholar 

  20. Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic model checking with rich assertional languages. Theoret. Comput. Sci. 256, 93–112 (2001)

    Article  MathSciNet  Google Scholar 

  21. Lowe, G.: Analysing lock-free linearizable datatypes using CSP. In: Gibson-Robinson, T., Hopcroft, P., Lazić, R. (eds.) Concurrency, Security, and Puzzles. LNCS, vol. 10160, pp. 162–184. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-51046-0_9

    Chapter  Google Scholar 

  22. Lubachevsky, B.: An approach to automating the verification of compact parallel coordination programs. Acta Inform. 21(2), 125–169 (1984)

    Article  MathSciNet  Google Scholar 

  23. Mazur, T., Lowe, G.: CSP-based counter abstraction for systems with node identifiers. Sci. Comput. Program. 81, 3–52 (2014)

    Article  Google Scholar 

  24. Michael, M., Scott, M.: Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: Proceedings of the Fifteenth Annual ACM Symposium on Principles of Distributed Computing, pp. 267–275 (1996)

    Google Scholar 

  25. Pnueli, A., Xu, J., Zuck, L.: Liveness with \((0,1, \infty )\)-counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 107–122. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45657-0_9

    Chapter  Google Scholar 

  26. Roscoe, A.W.: Understanding Concurrent Systems. Springer, London (2010). https://doi.org/10.1007/978-1-84882-258-0

    Book  MATH  Google Scholar 

  27. Roscoe, A.W., Creese, S.: Data independent induction over structured networks. In: Proceedings of PDPTA 2000 (2000)

    Google Scholar 

  28. Sistla, A.P., Gyuris, V., Emerson, E.A.: SMC: a symmetry-based model checker for verification of safety and linveness properties. ACM Trans. Softw. Eng. Methodol. 9(2), 133–166 (2000)

    Article  Google Scholar 

  29. Touili, T.: Regular model checking using widening techniques. Electr. Notes Theoret. Comput. Sci. 50(4), 342–356 (2001). Proceedings of VEPAS 2001

    Article  Google Scholar 

  30. Wolper, P.: Expressing interesting properties of programs in propositional temporal logic. In: Thirteenth Annual ACM Symposium on Principles of Programming Languages, pp. 184–193 (1986)

    Google Scholar 

  31. Wolper, P., Boigelot, B.: Verifying systems with infinite but regular state spaces. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 88–97. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0028736

    Chapter  Google Scholar 

  32. Wolper, P., Lovinfosse, V.: Verifying properties of large sets of processes with network invariants. In: Sifakis, J. (ed.) Automatic Verification Methods for Finite State Systems. LNCS, vol. 407, pp. 68–80. Springer, Heidelberg (1989). https://doi.org/10.1007/3-540-52148-8

    Chapter  Google Scholar 

Download references

Acknowledgements

I would like to thank Tom Gibson-Robinson for useful discussions concerning this work, and for extending the FDR4 API to support various functions necessary for the implementation from Sect. 6.1.

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Oxford, Oxford, UK

    Gavin Lowe

Authors
  1. Gavin Lowe
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Gavin Lowe .

Editor information

Editors and Affiliations

  1. NASA Jet Propulsion Laboratory, Pasadena, California, USA

    Klaus Havelund

  2. University of Bremen, Bremen, Germany

    Jan Peleska

  3. University of Oxford, Oxford, United Kingdom

    Bill Roscoe

  4. Eindhoven University of Technology, Eindhoven, The Netherlands

    Erik de Vink

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Lowe, G. (2018). View Abstraction for Systems with Component Identities. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds) Formal Methods. FM 2018. Lecture Notes in Computer Science(), vol 10951. Springer, Cham. https://doi.org/10.1007/978-3-319-95582-7_30

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-95582-7_30

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-95581-0

  • Online ISBN: 978-3-319-95582-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation