[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

Incremental design-space model checking via reusable reachable state approximations

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

The design of safety-critical systems often requires design space exploration: comparing several system models that differ in terms of design choices, capabilities, and implementations. Model checking can compare different models in such a set, however, it is continuously challenged by the state space explosion problem. Therefore, learning and reusing information from solving related models becomes very important for future checking efforts. For example, reusing variable ordering in BDD-based model checking leads to substantial performance improvement. In this paper, we present a SAT-based algorithm for checking a set of models. Our algorithm, FuseIC3, extends IC3 to minimize time spent in exploring the common state space between related models. Specifically, FuseIC3 accumulates artifacts from the sequence of over-approximated reachable states, called frames, from earlier runs when checking new models, albeit, after careful repair. It uses bidirectional reachability; forward reachability to repair frames, and IC3-type backward reachability to block predecessors to bad states. We extensively evaluate FuseIC3 over a large collection of challenging benchmarks. FuseIC3 is on-average up to 5.48\(\times \) (median 1.75\(\times \)) faster than checking each model individually, and up to 3.67\(\times \) (median 1.72\(\times \)) faster than the state-of-the-art incremental IC3 algorithm. Moreover, we evaluate the performance improvement of FuseIC3 by smarter ordering of models and property grouping using a linear-time hashing approach.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5

Similar content being viewed by others

Notes

  1. http://temporallogic.org/research/FMCAD17/.

  2. https://github.com/aappleby/smhasher.

  3. http://www.satcompetition.org/2009/format-benchmarks2009.html.

  4. https://es-static.fbk.eu/people/griggio/ic3ia/.

  5. http://fmv.jku.at/hwmcc15/.

References

  1. Bauer C, Lagadec K, Bès C, Mongeau M (2007) Flight control system architecture optimization for fly-by-wire airliners. J Guid Control Dyn 30(4):1023–1029. https://doi.org/10.2514/1.26311

    Article  Google Scholar 

  2. Gario M, Cimatti A, Mattarei C, Tonetta S, Rozier KY (2016) Model checking at scale: automated air traffic control design space exploration. In: Chaudhuri S, Farzan A (eds) Computer aided verification. Springer, Cham, pp 3–22. https://doi.org/10.1007/978-3-319-41540-6_1

    Chapter  Google Scholar 

  3. Mattarei C, Cimatti A, Gario M, Tonetta S, Rozier KY (2015) Comparing different functional allocations in automated air traffic control design. In: Formal methods in computer-aided design. FMCAD Inc, Austin, pp 112–119. https://doi.org/10.5555/2893529.2893551

  4. Bozzano M, Cimatti A, Pires AF, Jones D, Kimberly G, Petri T, Robinson R, Tonetta S (2015) Formal design and safety analysis of AIR6110 wheel brake system. In: Computer aided verification. Springer, Cham, pp 518–535. https://doi.org/10.1007/978-3-319-21690-4_36

  5. James P, Moller F, Nga Nguyen H, Roggenbach M, Schneider S, Treharne H (2014) On modelling and verifying railway interlockings: tracking train lengths. Sci Comput Program 96:315–336. https://doi.org/10.1016/j.scico.2014.04.005

    Article  Google Scholar 

  6. Moller F, Nguyen HN, Roggenbach M, Schneider S, Treharne H (2013) Defining and model checking abstractions of complex railway models using CSP\(\vert \)\(\vert \)B. In: Hardware and software: verification and testing. Springer, Berlin, pp 193–208. https://doi.org/10.1007/978-3-642-39611-3_20

  7. Dureja R, Rozier EWD, Rozier KY (2017) A case study in safety, security, and availability of wireless-enabled aircraft communication networks. In: Aviation technology, integration, and operations conference. AIAA, Denver, Colorado. https://doi.org/10.2514/6.2017-3112

  8. Dureja R, Rozier KY (2020) Formal framework for safety, security, and availability of aircraft communication networks. J Aerosp Inf Syst 17(7):322–335. https://doi.org/10.2514/1.I010769

    Article  Google Scholar 

  9. Bradley AR (2011) SAT-based model checking without unrolling. In: Cousot R (ed) Verification, model checking, and abstract interpretation. Springer, Berlin, pp 70–87. https://doi.org/10.1007/978-3-642-18275-4_7

    Chapter  Google Scholar 

  10. Een N, Mishchenko A, Brayton R (2011) Efficient implementation of property directed reachability. In: Formal methods in computer-aided design. FMCAD Inc, Austin, pp 125–134. https://doi.org/10.5555/2157654.2157675

  11. Yang B, Bryant RE, O’Hallaron DR, Biere A, Coudert O, Janssen G, Ranjan RK, Somenzi F (1998) A performance study of BDD-based model checking. In: Hunt WA, Johnson SD (eds) Formal methods in computer-aided design. Springer, Berlin, pp 255–289. https://doi.org/10.1007/3-540-49519-3_18

  12. Beer I, Ben-David S, Eisner C, Landver A (1996) Rulebase: an industry-oriented formal verification tool. In: Design automation conference. Association for Computing Machinery, New York, pp 655–660. https://doi.org/10.1145/240518.240642

  13. Marques-Silva J (2007) Interpolant learning and reuse in sat-based model checking. Electron Notes Theor Comput Sci 174(3):31–43. https://doi.org/10.1016/j.entcs.2006.12.021

    Article  MATH  Google Scholar 

  14. Schrammel P, Kroening D, Brain M, Martins R, Teige T, Bienmüller T (2017) Incremental bounded model checking for embedded software. Formal Aspects Comput 29(5):911–931. https://doi.org/10.1007/s00165-017-0419-1

    Article  MathSciNet  MATH  Google Scholar 

  15. Chockler H, Ivrii A, Matsliah A, Moran S, Nevo Z (2011) Incremental formal verification of hardware. In: Formal methods in computer-aided design. FMCAD Inc, Austin, pp 135–143. https://doi.org/10.5555/2157654.2157676

  16. Yang G, Dwyer MB, Rothermel G (2009) Regression model checking. In: International conference on software maintenance. IEEE, New York, pp 115–124. https://doi.org/10.1109/icsm.2009.5306334

  17. Chockler H, KupfermanO Vardi MY (2006) Coverage metrics for temporal logic model checking. Formal Methods Syst Des 28(3):189–212. https://doi.org/10.1007/s10703-006-0001-6

    Article  MATH  Google Scholar 

  18. Classen A, Heymans P, Schobbens P-Y, Legay A, Raskin J-F (2010) Model checking lots of systems: efficient verification of temporal properties in software product lines. In: International conference on software engineering. Association for Computing Machinery, New York, pp 335–344. https://doi.org/10.1145/1806799.1806850

  19. Classen A, Heymans P, Schobbens P-Y, Legay A (2011) Symbolic model checking of software product lines. In: International conference on software engineering. Association for Computing Machinery, New York, pp 321–330. https://doi.org/10.1145/1985793.1985838

  20. Classen A, Cordy M, Heymans P, Legay A, Schobbens P-Y (2012) Model checking software product lines with SNIP. Softw Tools Technol Transf 14(5):589–612. https://doi.org/10.1007/s10009-012-0234-1

    Article  Google Scholar 

  21. Ben-David S, Sterin B, Atlee JM, Beidu S (2015) Symbolic model checking of product-line requirements using SAT-based methods. In: International conference on software engineering. IEEE Press, New York, pp 189–199. https://doi.org/10.5555/2818754.2818780

  22. Classen A, Cordy M, Schobbens P-Y, Heymans P, Legay A, Raskin J-F (2013) Featured transition systems: foundations for verifying variability-intensive systems and their application to LTL model checking. IEEE Trans Softw Eng 39(8):1069–1089. https://doi.org/10.1109/TSE.2012.86

    Article  Google Scholar 

  23. Dureja R, Rozier KY (2018) More scalable LTL model checking via discovering design-space dependencies (D\(^3\)). In: Tools and algorithms for the construction and analysis of systems. Springer, Cham, pp 309–327. https://doi.org/10.1007/978-3-319-89960-2_17

  24. Cimatti A, Griggio A, Mover S, Tonetta S (2013) Parameter synthesis with IC3. In: Formal methods in computer-aided design. FMCAD Inc, Austin, pp 165–168. https://doi.org/10.1109/fmcad.2013.6679406

  25. Emerson EA, Kahlon V (2000) Reducing model checking of the many to the few. In: International conference on automated deduction. Springer, Berlin, pp 236–254. https://doi.org/10.1007/10721959_19

  26. Goldberg E, Güdemann M, Kroening D, Mukherjee R (2018) Efficient verification of multi-property designs (the benefit of wrong assumptions). In: Design, automation test in Europe (DATE), pp 43–48. https://doi.org/10.23919/DATE.2018.8341977

  27. Dureja R, Rozier KY (2017) FuseIC3: an algorithm for checking large design spaces. In: Formal methods in computer-aided design. FMCAD Inc, Austin, pp 164–171. https://doi.org/10.23919/FMCAD.2017.8102255

  28. Andoni A, Indyk P (2008) Near-optimal hashing algorithms for approximate nearest neighbor in high dimensions. Commun ACM 51(1):117–122. https://doi.org/10.1145/1327452.1327494

    Article  Google Scholar 

  29. Biere A, Cimatti A, Clarke E, Zhu Y (1999) Symbolic model checking without BDDs. In: Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 193–207. https://doi.org/10.1007/3-540-49059-0_14

  30. McMillan KL (2003) Interpolation and sat-based model checking. In: Computer aided verification. Springer, Berlin, pp 1–13. https://doi.org/10.1007/978-3-540-45069-6_1

  31. Vizel Y, Grumberg O (2009) Interpolation-sequence based model checking. In: Formal methods in computer-aided design. FMCAD Inc, Austin, pp 1–8. https://doi.org/10.1109/FMCAD.2009.5351148

  32. Li J, Dureja R, Pu G, Rozier KY, Vardi MY (2018) SimpleCAR: an efficient bug-finding tool based on approximate reachability. In: Computer aided verification. Springer, Cham, pp 37–44. https://doi.org/10.1007/978-3-319-96142-2_5

  33. Bradley AR (2012) Understanding IC3. In: Theory and applications of satisfiability testing. Springer, Berlin, pp 1–14. https://doi.org/10.1007/978-3-642-31612-8_1

  34. Griggio A, Roveri M (2016) Comparing different variants of the IC3 algorithm for hardware model checking. IEEE Trans Comput Aided Des Integr Circuits Syst 35(6):1026–1039. https://doi.org/10.1109/TCAD.2015.2481869

    Article  Google Scholar 

  35. Somenzi F, Bradley AR (2011) Ic3: where monolithic and incremental meet. In: Formal methods in computer-aided design. FMCAD Inc, Austin, pp 3–8. https://doi.org/10.5555/2157654.2157657

  36. Chi L, Zhu X (2017) Hashing techniques: a survey and taxonomy. ACM Comput Surv 50(1):11–11136. https://doi.org/10.1145/3047307

    Article  Google Scholar 

  37. Broder AZ, Charikar M, Frieze AM, Mitzenmacher M (2000) Min-wise independent permutations. J Comput Syst Sci 60(3):630–659. https://doi.org/10.1006/jcss.1999.1690

    Article  MathSciNet  MATH  Google Scholar 

  38. Rajaraman A, Ullman JD (2011) Mining of massive datasets, Chap. 3. Cambridge University Press, New York, pp 55–111. https://doi.org/10.1017/CBO9781139924801

    Book  Google Scholar 

  39. Cabodi G, Camurati PE, Loiacono C, Palena M, Pasini P, Patti D, Quer S (2017) To split or to group: from divide-and-conquer to sub-task sharing for verifying multiple properties in model checking. J Softw Tools Technol Transf. https://doi.org/10.1007/s10009-017-0451-8

    Article  Google Scholar 

  40. Cabodi G, Nocco S (2011) Optimized model checking of multiple properties. In: Design, automation test in Europe. IEEE, New York, pp 1–4. https://doi.org/10.1109/DATE.2011.5763279

  41. Cimatti A, Griggio A, Schaafsma BJ, Sebastiani R (2013) The MathSAT5 smt solver. In: Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 93–107. https://doi.org/10.1007/978-3-642-36742-7_7

  42. Dureja R, Baumgartner J, Ivrii A, Kanzelman R, Rozier KY (2019) Boosting verification scalability via structural grouping and semantic partitioning of properties. In: Formal methods in computer aided design. FMCAD Inc, Austin, pp 1–9. https://doi.org/10.23919/FMCAD.2019.8894265

  43. Dureja R, Baumgartner J, Kanzelman R, Williams M, Rozier KY (2020) Accelerating parallel verification via complementary property partitioning and strategy exploration. In: Formal methods in computer aided design. FMCAD Inc, Austin, pp 16–25. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_8

  44. Claessen K, Sörensson N (2012) A liveness checking algorithm that counts. In: Formal methods in computer-aided design. FMCAD Inc, Austin, pp 52–59

Download references

Acknowledgements

Thanks to NSF CAREER Award CNS-1664356 for supporting this work. We thank Armin Biere for discussion and feedback on the use of hashing to find the exact same models in a design space.

Author information

Authors and Affiliations

  1. IBM Corporation, Texas, USA

    Rohit Dureja

  2. Iowa State University, Ames, USA

    Kristin Y. Rozier

Authors
  1. Rohit Dureja
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Kristin Y. Rozier
    View author publications

    You can also search for this author in PubMed Google Scholar

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Dureja, R., Rozier, K.Y. Incremental design-space model checking via reusable reachable state approximations. Form Methods Syst Des 58, 375–398 (2021). https://doi.org/10.1007/s10703-022-00389-5

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-022-00389-5

Keywords

Search

Navigation