Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Formal Methods

FM 2018: Formal Methods pp 485–504Cite as

To Compose, or Not to Compose, That Is the Question: An Analysis of Compositional State Space Generation

  • Conference paper
  • First Online:

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

Abstract

To combat state space explosion several compositional verification approaches have been proposed. One such approach is compositional aggregation, where a given system consisting of a number of parallel components is iteratively composed and minimised. Compositional aggregation has shown to perform better (in the size of the largest state space in memory at one time) than classical monolithic composition in a number of cases. However, there are also cases in which compositional aggregation performs much worse.

It is unclear when one should apply compositional aggregation in favor of other techniques and how it is affected by action hiding and the scale of the model.

This paper presents a descriptive analysis following the quantitiative experimental approach. The experiments were conducted in a controlled test bed setup in a computer laboratory environment. A total of eight scalable models with different network topologies considering a number of varying properties were investigated comprising 119 subjects. This makes it the most comprehensive study done so far on the topic. We investigate whether there is any systematic difference in the success of compositional aggregation based on the model, scaling, and action hiding. Our results indicate that both scaling up the model and hiding more behaviour has a positive influence on compositional aggregation.

S. de Putter—This work is supported by ARTEMIS Joint Undertaking project EMC2 (grant nr. 621429).

This is a preview of subscription content, 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

Learn about institutional subscriptions

Notes

  1. 1.

    paradise.fi.muni.cz/beem.

  2. 2.

    http://laser.cs.umass.edu/breakingup-examples.

  3. 3.

    http://www.win.tue.nl/mdse/property_preservation/FAC2017_experiments.zip.

  4. 4.

    The models are available at http://www.win.tue.nl/mdse/composition/test_cases.zip.

  5. 5.

    All generated data is available at http://www.win.tue.nl/mdse/composition/test_cases_data.zip.

References

  1. Abd Elkader, K., Grumberg, O., Păsăreanu, C.S., Shoham, S.: Automated circular assume-guarantee reasoning with N-way decomposition and alphabet refinement. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 329–351. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41528-4_18

    Chapter  Google Scholar 

  2. Andersen, H.: Partial model checking. In: LICS, pp. 398–407. IEEE Computer Society Press (1995)

    Google Scholar 

  3. Anderson, J.H., Kim, Y.J., Herman, T.: Shared-memory mutual exclusion: major research trends since 1986. Distrib. Comput. 16(2–3), 75–110 (2003)

    Article  Google Scholar 

  4. ASCI: The Distributed ASCI Supercomputer DAS4. http://www.cs.vu.nl/das4/. Accessed 09-08-2017

  5. Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  6. Cheung, S.C., Kramer, J.: Context constraints for compositional reachability analysis. ACM Trans. Softw. Eng. Methodol. 5(4), 334–377 (1996)

    Article  Google Scholar 

  7. Cobleigh, J.M., Avrunin, G.S., Clarke, L.A.: Breaking up is hard to do: an evaluation of automated assume-guarantee reasoning. ACM Trans. Softw. Eng. Methodol. 17(2), 7:1–7:52 (2008)

    Article  Google Scholar 

  8. Crouzen, P., Lang, F.: Smart reduction. In: Giannakopoulou, D., Orejas, F. (eds.) FASE 2011. LNCS, vol. 6603, pp. 111–126. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19811-3_9

    Chapter  Google Scholar 

  9. Crouzen, P., Hermanns, H.: Aggregation ordering for massively compositional models. In: 10th International Conference on Application of Concurrency to System Design, pp. 171–180. IEEE (2010)

    Google Scholar 

  10. Fernandez, J.: ALDEBARAN: un système de vérification par réduction de processus communicants. (Aldebaran : a system of verification of communicating processes by using reduction). Ph.D. thesis, Joseph Fourier University, Grenoble, France (1988)

    Google Scholar 

  11. Garavel, H., Lang, F., Mateescu, R.: Compositional Verification of Asynchronous Concurrent Systems using CADP (extended version). Research Report RR-8708, INRIA Grenoble - Rhône-Alpes, Apr 2015. https://hal.inria.fr/hal-01138749

  12. Garavel, H., Sighireanu, M.: A graphical parallel composition operator for process algebras. In: FORTE/PSTV 1999. IFIP Conference Proceedings, vol. 156, pp. 185–202. Kluwer (1999)

    Google Scholar 

  13. Garavel, H., Lang, F.: SVL: a scripting language for compositional verification. In: 21st International Conference on Formal Techniques for Networked and Distributed Systems, pp. 377–392. Kluwer, Boston, MA (2002)

    Google Scholar 

  14. Gheorghiu Bobaru, M., Păsăreanu, C.S., Giannakopoulou, D.: Automated assume-guarantee reasoning by abstraction refinement. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 135–148. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-70545-1_14

    Chapter  Google Scholar 

  15. Glabbeek, R.V., Luttik, S., Trčka, N.: Branching bisimilarity with explicit divergence. Fundam. Inform. 93(4), 371–392 (2009)

    MathSciNet  MATH  Google Scholar 

  16. Gupta, A., McMillan, K.L., Fu, Z.: Automated assumption generation for compositional verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 420–432. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73368-3_45

    Chapter  MATH  Google Scholar 

  17. Heimbold, D., Luckham, D.: Debugging ada tasking programs. IEEE Softw. 2, 47–57 (1985)

    Article  Google Scholar 

  18. Hintze, J., Nelson, R.: Violin plots: a box plot-density trace synergism. Am. Stat. 52(2), 181–184 (1998)

    Google Scholar 

  19. Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress, vol. 83, pp. 321–332 (1983)

    Google Scholar 

  20. Keller, R.K., Cameron, M., Taylor, R.N., Troup, D.B.: User interface development and software environments: the Chiron-1 system. In: Proceedings of the 13th International Conference on Software Engineering, pp. 208–218. IEEE (1991)

    Google Scholar 

  21. Kendall, M., Gibbons, J.: Rank correlation methods, chap. 3, 5th edn. Oxford University Press, Oxford (1990)

    MATH  Google Scholar 

  22. Lang, F.: Refined interfaces for compositional verification. In: Najm, E., Pradat-Peyre, J.-F., Donzeau-Gouge, V.V. (eds.) FORTE 2006. LNCS, vol. 4229, pp. 159–174. Springer, Heidelberg (2006). https://doi.org/10.1007/11888116_13

    Chapter  Google Scholar 

  23. Le Lann, G.: Distributed systems - towards a formal approach. In: IFIP Congress, pp. 155–160 (1977)

    Google Scholar 

  24. Mateescu, R., Wijs, A.: Property-dependent reductions adequate with divergence-sensitive branching bisimilarity. Sci. Comput. Program. 96(3), 354–376 (2014)

    Article  Google Scholar 

  25. O’Leary, Z.: The Essential Guide to Doing Research. SAGE Publications, Thousand Oaks (2004)

    Google Scholar 

  26. Păsăreanu, C.S., Giannakopoulou, D., Bobaru, M.G., Cobleigh, J.M., Barringer, H.: Learning to divide and conquer: applying the l* algorithm to automate assume-guarantee reasoning. Form. Methods Syst. Des. 32(3), 175–205 (2008)

    Article  Google Scholar 

  27. Pelánek, R.: BEEM: benchmarks for explicit model checkers. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 263–267. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73370-6_17

    Chapter  Google Scholar 

  28. Peterson, G.L.: Myths about the mutual exclusion problem. IPL 12, 115–116 (1981)

    Article  Google Scholar 

  29. Pnueli, A.: In transition from global to modular temporal reasoning about programs. Logics and Models of Concurrent Systems. NATO ASI, vol. 13, pp. 123–144. Springer, Berlin (1985). https://doi.org/10.1007/978-3-642-82453-1_5

    Chapter  Google Scholar 

  30. de Putter, S., Wijs, A.: Compositional model checking is lively. In: Proença, J., Lumpe, M. (eds.) FACS 2017. LNCS, vol. 10487, pp. 117–136. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68034-7_7

    Chapter  Google Scholar 

  31. de Putter, S., Wijs, A.: A formal verification technique for behavioural model-to-model transformations. Form. Asp. Comput. 30, 3–43 (2017). https://doi.org/10.1007/s00165-017-0437-z

    Article  MathSciNet  MATH  Google Scholar 

  32. Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall PTR, Upper Saddle River (1997)

    Google Scholar 

  33. Sabnani, K.K., Lapone, A.M., Uyar, M.U.: An algorithmic procedure for checking safety properties of protocols. IEEE Trans. Commun. 37(9), 940–948 (1989)

    Article  Google Scholar 

  34. Tai, K.C., Koppol, P.V.: Hierarchy-based incremental analysis of communication protocols. In: 1993 International Conference on Network Protocols, pp. 318–325. IEEE (1993)

    Google Scholar 

  35. Tai, K.C., Koppol, P.V.: An incremental approach to reachability analysis of distributed programs. In: Proceedings of the 7th International Workshop on Software Specification and Design, pp. 141–150. IEEE Computer Society Press (1993)

    Google Scholar 

  36. Valmari, A.: Compositional state space generation. In: Rozenberg, G. (ed.) ICATPN 1991. LNCS, vol. 674, pp. 427–457. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-56689-9_54

    Chapter  Google Scholar 

  37. Wijs, A., Engelen, L.: REFINER: towards formal verification of model transformations. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 258–263. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-06200-6_21

    Chapter  Google Scholar 

Download references

Acknowledgements

The authors would like to thank Vrije Universiteit Amsterdam for their generosity in supplying the computing resources for the experiments.

Author information

Authors and Affiliations

  1. Eindhoven University of Technology, PO Box 513, 5600 MB, Eindhoven, The Netherlands

    Sander de Putter & Anton Wijs

Authors
  1. Sander de Putter
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Anton Wijs
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Sander de Putter or Anton Wijs .

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

de Putter, S., Wijs, A. (2018). To Compose, or Not to Compose, That Is the Question: An Analysis of Compositional State Space Generation. 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_29

Download citation

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

  • 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