Skip to main content
SpringerLink
Log in

Every Component Matters: Generating Parallel Verification Benchmarks with Hardness Guarantees

  • Conference paper
  • First Online:
Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends (ISoLA 2020)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 12479))

Included in the following conference series:

  • 633 Accesses

Abstract

In this paper, we show how to automatically generate hard verification tasks in order to support events like the Model Checking Contest or the Rigorous Examination of Reactive Systems Challenge with tailored benchmark problems for analyzing the validity of linear-time properties in parallel systems. Characteristic of the generated benchmarks are two hardness guarantees: (i) every parallel component is relevant and (ii) the state space of the analyzed system is exponential in the number of its parallel components. Generated benchmarks can be made available, e.g., as Promela code or Petri nets.

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 EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

Similar content being viewed by others

Notes

  1. 1.

    This means that property \(\varphi \) does not hold in the final task.

  2. 2.

    To be precise, the information of whether or not such violation witnesses exist is lost during abstraction.

  3. 3.

    Note that \(\varSigma ({M}) = \varSigma ({\mathord {\dashrightarrow }})\) is not guaranteed in general.

  4. 4.

    These laws are meant to hold up to graph isomorphism.

  5. 5.

    Please note that every must transition is also a may transition.

  6. 6.

    Note that other CE-handles for \(\varphi \) exist, for example the transition labeled a itself.

  7. 7.

    Please recall that the precedence relation \(\mathrel {\lessdot _{\pi }}\) has been introduced in Definition 2.

  8. 8.

    https://graphviz.org/doc/info/lang.html.

  9. 9.

    http://www.rers-challenge.org/2020/.

  10. 10.

    https://learnlib.de/projects/automatalib/. Support for modal contracts is planned to be made publicly available with the next release (0.11).

References

  1. Baier, C., Katoen, J.P., Larsen, K.G.: Principles of Model Checking. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  2. Bauer, S.S., et al.: Moving from specifications to contracts in component-based design. In: de Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 43–58. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28872-2_3

    Chapter  Google Scholar 

  3. Benveniste, A., Caillaud, B.: Synchronous interfaces and assume/guarantee contracts. In: Aceto, L., Bacci, G., Bacci, G., Ingólfsdóttir, A., Legay, A., Mardare, R. (eds.) Models, Algorithms, Logics and Tools. LNCS, vol. 10460, pp. 233–248. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63121-9_12

    Chapter  MATH  Google Scholar 

  4. Benveniste, A., et al.: Contracts for system design. Found. Trends Electron. Des. Autom. 12(2–3), 124–400 (2018). https://doi.org/10.1561/1000000053

    Article  Google Scholar 

  5. Cardoso, R.C., Farrell, M., Luckcuck, M., Ferrando, A., Fisher, M.: Heterogeneous verification of an autonomous curiosity rover. In: Lee, R., Jha, S., Mavridou, A., Giannakopoulou, D. (eds.) NFM 2020. LNCS, vol. 12229, pp. 353–360. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-55754-6_20

    Chapter  Google Scholar 

  6. Chandra, S., Godefroid, P., Palm, C.: Software model checking in practice: an industrial case study. In: Proceedings of the 24th International Conference on Software Engineering, ICSE 2002, pp. 431–441 (2002). https://doi.org/10.1145/581339.581393

  7. Garavel, H.: Nested-unit Petri nets. J. Log. Algebraic Methods Program. 104, 60–85 (2019). https://doi.org/10.1016/j.jlamp.2018.11.005

    Article  MathSciNet  MATH  Google Scholar 

  8. Geske, M., Jasper, M., Steffen, B., Howar, F., Schordan, M., van de Pol, J.: RERS 2016: parallel and sequential benchmarks with focus on LTL verification. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 787–803. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47169-3_59

    Chapter  Google Scholar 

  9. Giannakopoulou, D., Magee, J.: Fluent model checking for event-based systems. ACM SIGSOFT Softw. Eng. Notes 28(5), 257–266 (2003). https://doi.org/10.1145/940071.940106

    Article  Google Scholar 

  10. Goga, N., Costache, S., Moldoveanu, F.: A formal analysis of ISO/IEEE P11073-20601 standard of medical device communication. In: 3rd Annual IEEE Systems Conference, pp. 163–166 (2009). https://doi.org/10.1109/SYSTEMS.2009.4815792

  11. Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Trans. Program. Lang. Syst. (TOPLAS) 16(3), 843–871 (1994). https://doi.org/10.1145/177492.177725

    Article  Google Scholar 

  12. Hoare, C.A.R.: Communicating sequential processes. In: The Origin of Concurrent Programming, pp. 413–443. Springer (1978). https://doi.org/10.1145/359576.359585

  13. Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual, 1st edn. Addison-Wesley Professional, Boston (2011)

    Google Scholar 

  14. Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D., Păsăreanu, C.: Rigorous examination of reactive systems. The RERS challenges 2012 and 2013. STTT 16(5), 457–464 (2014). https://doi.org/10.1007/s10009-014-0337-y

    Article  Google Scholar 

  15. Howar, F., Jasper, M., Mues, M., Schmidt, D., Steffen, B.: The RERS challenge: towards controllable and scalable benchmark synthesis. Int. J. Softw. Tools Technol. Transfer. (2021). https://doi.org/10.1007/s10009-021-00617-z

  16. Jasper, M., et al.: The RERS 2017 challenge and workshop (invited paper). In: Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software. SPIN 2017, pp. 11–20. ACM (2017). https://doi.org/10.1145/3092282.3098206

  17. Jasper, M., et al.: RERS 2019: combining synthesis with real-world models. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019. LNCS, vol. 11429, pp. 101–115. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17502-3_7

    Chapter  Google Scholar 

  18. Jasper, M., Mues, M., Schlüter, M., Steffen, B., Howar, F.: RERS 2018: CTL, LTL, and reachability. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 433–447. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03421-4_27

    Chapter  Google Scholar 

  19. Jasper, M., Steffen, B.: Synthesizing subtle bugs with known witnesses. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 235–257. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03421-4_16

    Chapter  Google Scholar 

  20. Kordon, F., et al.: Report on the model checking contest at Petri nets 2011. In: Jensen, K., van der Aalst, W.M., Ajmone Marsan, M., Franceschinis, G., Kleijn, J., Kristensen, L.M. (eds.) Transactions on Petri Nets and Other Models of Concurrency VI. LNCS, vol. 7400, pp. 169–196. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-35179-2_8

    Chapter  Google Scholar 

  21. Lang, F., Mateescu, R., Mazzanti, F.: Compositional verification of concurrent systems by combining bisimulations. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 196–213. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30942-8_13

    Chapter  Google Scholar 

  22. Lang, F., Mateescu, R., Mazzanti, F.: Sharp congruences adequate with temporal logics combining weak and strong modalities. In: TACAS 2020. LNCS, vol. 12079, pp. 57–76. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-45237-7_4

  23. Larsen, K.G.: Modal specifications. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 232–246. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-52148-8_19

    Chapter  Google Scholar 

  24. Guldstrand Larsen, K.: Ideal specification formalism = expressivity + compositionality + decidability + testability + ... In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 33–56. Springer, Heidelberg (1990). https://doi.org/10.1007/BFb0039050

  25. Peterson, J.L.: Petri Net Theory and the Modeling of Systems. Prentice Hall PTR (1981)

    Google Scholar 

  26. Raclet, J.B., Badouel, E., Benveniste, A., Caillaud, B., Legay, A., Passerone, R.: A modal interface theory for component-based design. Fund. Inform. 108(1–2), 119–149 (2011). https://doi.org/10.3233/FI-2011-416

    Article  MathSciNet  MATH  Google Scholar 

  27. Siegel, S.F., Yan, Y.: Action-based model checking: logic, automata, and reduction. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 77–100. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-53291-8_6

    Chapter  Google Scholar 

  28. Steffen, B., Jasper, M., Meijer, J., van de Pol, J.: Property-preserving generation of tailored benchmark Petri nets. In: 2017 17th International Conference on Application of Concurrency to System Design (ACSD), pp. 1–8 (2017). https://doi.org/10.1109/ACSD.2017.24

  29. Steffen, B., Jasper, M.: Property-preserving parallel decomposition. In: Aceto, L., Bacci, G., Bacci, G., Ingólfsdóttir, A., Legay, A., Mardare, R. (eds.) Models, Algorithms, Logics and Tools. LNCS, vol. 10460, pp. 125–145. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63121-9_7

    Chapter  Google Scholar 

  30. Steffen, B., Jasper, M.: Generating hard benchmark problems for weak bisimulation. In: Bartocci, E., Cleaveland, R., Grosu, R., Sokolsky, O. (eds.) From Reactive Systems to Cyber-Physical Systems. LNCS, vol. 11500, pp. 126–145. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-31514-6_8

    Chapter  Google Scholar 

  31. Warford, J.S., Vega, D., Staley, S.M.: A calculational deductive system for linear temporal logic. ACM Comput. Surv. 53(3) (2020). https://doi.org/10.1145/3387109

Download references

Author information

Authors and Affiliations

  1. TU Dortmund University, Dortmund, Germany

    Marc Jasper, Maximilian Schlüter, David Schmidt & Bernhard Steffen

Authors
  1. Marc Jasper
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Maximilian Schlüter
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. David Schmidt
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Bernhard Steffen
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Marc Jasper or Bernhard Steffen .

Editor information

Editors and Affiliations

  1. University of Limerick and Lero, Limerick, Ireland

    Tiziana Margaria

  2. TU Dortmund, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2021 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Jasper, M., Schlüter, M., Schmidt, D., Steffen, B. (2021). Every Component Matters: Generating Parallel Verification Benchmarks with Hardness Guarantees. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends. ISoLA 2020. Lecture Notes in Computer Science(), vol 12479. Springer, Cham. https://doi.org/10.1007/978-3-030-83723-5_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-83723-5_16

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-83722-8

  • Online ISBN: 978-3-030-83723-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation