Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Automated Invariant Generation for Efficient Deductive Reasoning About Embedded Systems

  • Conference paper
  • First Online:
Software Engineering and Formal Methods (SEFM 2024)

Part of the book series: Lecture Notes in Computer Science ((volume 15280))

Included in the following conference series:

Abstract

Deductive verification is often more efficient than alternative techniques like model checking at reasoning about functional properties of programs. This is especially true when the program under verification contains very large or unbounded data ranges that model checkers struggle with. However, modular deductive verifiers struggle with verifying global properties, which are often crucial in concurrent and reactive embedded systems. Embedded systems often require complex user-defined invariants to capture the global state for the verification of local annotations, demanding high effort and expertise from the user. In this paper, we propose a method to automatically generate compact invariants that are sufficiently strong to enable effective deductive verification of global properties in embedded systems. Our key idea is that a good level of abstraction can be found automatically by choosing variables for refinement that influence relevant events and process interactions. We use this idea together with abstract interpretation to build a system’s state space, abstracted to the relevant part for a given global property. We demonstrate the effectiveness of our approach on a SystemC design of an automotive control system that has in the past proved challenging to verify.

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

Access this chapter

Log in via an institution

Institutional subscriptions

References

  1. Artifact. https://doi.org/10.4121/86963fe3-cc3f-45c3-b252-00d8780c4a1a

  2. Amighi, A., Haack, C., Huisman, M., Hurlin, C.: Permission-based separation logic for multithreaded Java programs. Log. Methods Comput. Sci. 11(1) (2015). https://doi.org/10.2168/LMCS-11(1:2)2015

  3. Armborst, L., et al.: The VerCors verifier: a progress report. In: Gurfinkel, A., Ganesh, V. (eds.) CAV 2024. LNCS, vol. 14682, pp. 3–18. Springer, Cham (2024). https://doi.org/10.1007/978-3-031-65630-9_1

    Chapter  Google Scholar 

  4. Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30080-9_7

    Chapter  Google Scholar 

  5. Bensalem, S., Lakhnech, Y.: Automatic generation of invariants. Form. Methods Syst. Des. 15, 75–92 (1999). https://doi.org/10.1023/A:1008744030390

    Article  Google Scholar 

  6. Beyer, D., Chien, P.C., Lee, N.Z.: Augmenting interpolation-based model checking with auxiliary invariants (2024). https://doi.org/10.48550/arXiv.2403.07821

  7. Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_16

    Chapter  Google Scholar 

  8. Blom, S., Darabi, S., Huisman, M., Oortwijn, W.: The VerCors tool set: verification of parallel and concurrent software. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 102–110. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66845-1_7

    Chapter  Google Scholar 

  9. Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70–87. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-18275-4_7

    Chapter  Google Scholar 

  10. Case, M.L., Mishchenko, A., Brayton, R.K.: Automated extraction of inductive invariants to aid model checking. In: Formal Methods in Computer-Aided Design, pp. 165–172. IEEE (2007). https://doi.org/10.1109/FAMCAD.2007.12

  11. Cimatti, A., Griggio, A.: Software model checking via IC3. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 277–293. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31424-7_23

    Chapter  Google Scholar 

  12. Cimatti, A., Narasamdya, I., Roveri, M.: Software model checking SystemC. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 32(5), 774–787 (2013). https://doi.org/10.1109/TCAD.2012.2232351

    Article  Google Scholar 

  13. Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000). https://doi.org/10.1007/10722167_15

    Chapter  Google Scholar 

  14. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 238–252. ACM Press (1977). https://doi.org/10.1145/512950.512973

  15. Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. J. Symb. Logic 22, 250–268 (1957). https://doi.org/10.2307/2963593

  16. Fedyukovich, G., Bodík, R.: Accelerating syntax-guided invariant synthesis. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 251–269. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89960-2_14

    Chapter  Google Scholar 

  17. Furia, C.A., Meyer, B., Velder, S.: Loop invariants: analysis, classification, and examples. ACM Comput. Surv. (CSUR) 46(3), 1–51 (2014). https://doi.org/10.1145/2506375

    Article  Google Scholar 

  18. Galeotti, J.P., Furia, C.A., May, E., Fraser, G., Zeller, A.: DynaMate: dynamically inferring loop invariants for automatic full functional verification. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 48–53. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-13338-6_4

    Chapter  Google Scholar 

  19. Große, D., Le, H.M., Drechsler, R.: Formal verification of SystemC-based cyber components. In: Jeschke, S., Brecher, C., Song, H., Rawat, D.B. (eds.) Industrial Internet of Things. SSWT, pp. 137–167. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-42559-7_6

    Chapter  Google Scholar 

  20. Herber, P., Glesner, S.: A HW/SW co-verification framework for SystemC. ACM Trans. Embed. Comput. Syst. (TECS) 12(1s), 1–23 (2013). https://doi.org/10.1145/2435227.2435257

    Article  Google Scholar 

  21. Herber, P., Hünnemeyer, B.: Formal verification of SystemC designs using the BLAST software model checker. In: ACESMB@ MoDELS, pp. 44–53 (2014). https://dblp.org/rec/conf/models/HerberH14

  22. Herber, P., Liebrenz, T.: Dependence analysis and automated partitioning for scalable formal analysis of SystemC designs. In: ACM-IEEE International Conference on Formal Methods and Models for System Design, pp. 1–6. IEEE (2020). https://doi.org/10.1109/MEMOCODE51338.2020.9314998

  23. Herdt, V., Große, D., Drechsler, R.: Formal verification of SystemC-based designs using symbolic simulation. In: Enhanced Virtual Prototyping, pp. 59–117. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-54828-5_4

    Chapter  Google Scholar 

  24. IEEE Standards Association: IEEE Std. 1666–2011, SystemC Language Reference Manual. IEEE Press (2011). https://doi.org/10.1109/IEEESTD.2012.6134619

  25. Karlsson, D., Eles, P., Peng, Z.: Formal verification of SystemC designs using a Petri-net based representation. In: Design, Automation and Test in Europe, pp. 1228–1233. IEEE Press (2006). https://doi.org/10.1109/DATE.2006.244076

  26. Man, K.L., Fedeli, A., Mercaldi, M., Boubekeur, M., Schellekens, M.: SC2SCFL: automated SystemC to \(SystemC^{\mathbb{F}\mathbb{L}}\) translation. In: Vassiliadis, S., Bereković, M., Hämäläinen, T.D. (eds.) SAMOS 2007. LNCS, vol. 4599, pp. 34–45. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73625-7_6

    Chapter  Google Scholar 

  27. McMillan, K.L.: Interpolation and SAT-based model checking. In: International Conference on Computer Aided Verification, pp. 1–13 (2003). https://doi.org/10.1007/978-3-540-45069-6_1

  28. O’Hearn, P.W.: Resources, concurrency and local reasoning. Theor. Comput. Sci. 375(1–3), 271–307 (2007). https://doi.org/10.1016/j.tcs.2006.12.035

    Article  MathSciNet  Google Scholar 

  29. Phan, Q.S., Malacaria, P.: All-solution satisfiability modulo theories: applications, algorithms and benchmarks. In: International Conference on Availability, Reliability and Security, pp. 100–109. IEEE (2015). https://doi.org/10.1109/ARES.2015.14

  30. Reif, K.: Bremsen und Bremsregelsysteme [Brakes and brake control systems]. Bosch Fachinformation Automobil, Vieweg+Teubner Verlag Wiesbaden (2010). https://doi.org/10.1007/978-3-8348-9714-5

  31. Tabar, A.H., Bubel, R., Hähnle, R.: Automatic loop invariant generation for data dependence analysis. In: IEEE/ACM International Conference on Formal Methods in Software Engineering, pp. 34–45 (2022). https://doi.org/10.1145/3524482.3527649

  32. Tasche, P., Monti, R.E., Drerup, S.E., Blohm, P., Herber, P., Huisman, M.: Deductive verification of parameterized embedded systems modeled in SystemC. In: Dimitrova, R., Lahav, O., Wolff, S. (eds.) VMCAI 2024. LNCS, vol. 14500, pp. 187–209. Springer, Cham (2024). https://doi.org/10.1007/978-3-031-50521-8_9

    Chapter  Google Scholar 

  33. Yu, Y., Subramanyan, P., Tsiskaridze, N., Malik, S.: All-SAT using minimal blocking clauses. In: International Conference on VLSI Design, pp. 86–91. IEEE (2014). https://doi.org/10.1109/VLSID.2014.22

Download references

Author information

Authors and Affiliations

  1. University of Twente, Enschede, The Netherlands

    Philip Tasche, Paula Herber & Marieke Huisman

  2. University of Münster, Münster, Germany

    Paula Herber

Authors
  1. Philip Tasche
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Paula Herber
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Marieke Huisman
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Philip Tasche .

Editor information

Editors and Affiliations

  1. Campus Gualtar, University of Aveiro, Aveiro, Portugal

    Alexandre Madeira

  2. University of Augsburg, Augsburg, Germany

    Alexander Knapp

Rights and permissions

Reprints and permissions

Copyright information

© 2025 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Tasche, P., Herber, P., Huisman, M. (2025). Automated Invariant Generation for Efficient Deductive Reasoning About Embedded Systems. In: Madeira, A., Knapp, A. (eds) Software Engineering and Formal Methods. SEFM 2024. Lecture Notes in Computer Science, vol 15280. Springer, Cham. https://doi.org/10.1007/978-3-031-77382-2_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-77382-2_23

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-77381-5

  • Online ISBN: 978-3-031-77382-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation