Abstract
Program analysis is on the brink of mainstream usage in embedded systems development. Formal verification of behavioural requirements, finding runtime errors and test case generation are some of the most common applications of automated verification tools based on bounded model checking (BMC). Existing industrial tools for embedded software use an off-the-shelf bounded model checker and apply it iteratively to verify the program with an increasing number of unwindings. This approach unnecessarily wastes time repeating work that has already been done and fails to exploit the power of incremental SAT solving. This article reports on the extension of the software model checker CBMC to support incremental BMC and its successful integration with the industrial embedded software verification tool BTC EMBEDDED TESTER. We present an extensive evaluation over large industrial embedded programs, mainly from the automotive industry. We show that incremental BMC cuts runtimes by one order of magnitude in comparison to the standard non-incremental approach, enabling the application of formal verification to large and complex embedded software. We furthermore report promising results on analysing programs with arbitrary loop structure using incremental BMC, demonstrating its applicability and potential to verify general software beyond the embedded domain.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Alur R, Kanade A, Ramesh S, Shashidhar KC (2008) Symbolic analysis for improving simulation coverage of Simulink/Stateflow models. In: International conference on embedded software. ACM, pp 89–98
Brummayer R, Biere A (2009) Boolector: an efficient SMT solver for bit-vectors and arrays. In: Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 174–177
Brummayer R, Biere A (2009) Lemmas on demand for the extensional theory of arrays. J Satisf Boolean Model Comput 6(1–3): 165–201
Brummayer R, Biere A (2009) Effective bit-width and under-approximation. In: Computer aided systems theory. Springer, Berlin, pp 304–311
Biere A, Cimatti A, Clarke EM, Zhu Y (1999) Symbolic model checking without BDDs. In: Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 193–207
Beyer D, Dangl M, Wendler P (2015) Boosting k-induction with continuously-refined invariants. In Computer-aided verification. Springer, Berlin, pp 622–640
Biere A (2008) PicoSAT essentials. J Satisf Boolean Model Comput 4(2–4): 75–97
Brain M, Joshi S, Kroening D, Schrammel P (2015) Safety verification and refutation by k-invariants and k-induction. In: Static analysis symposium. Springer, Berlin, pp 145–161
Bryant RE, Kroening D, Ouaknine J, Seshia SA, Strichman O, Brady BA (2007) Deciding bit-vector arithmetic with abstraction. In: Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 358–372
Bryant RE, Kroening D, Ouaknine J, Seshia SA, Strichman O, Brady BA (2009) An abstraction-based decision procedure for bit-vector arithmetic. J Softw Tools Technol Transf 11(2): 95–104
Brillout A, Kroening D, Wahl T (2009) Mixed abstractions for floating-point arithmetic. In: Formal methods in computer-aided design. IEEE, pp 69–76
Bradley AR (2012) IC3 and beyond: incremental, inductive verification. In: Computer-aided verification. Springer, Berlin, p 4
Buechi Julius R (1962) On a decision method in restricted second-order arithmetic. In: International congress on logic, methodology, and philosophy of science. Stanford University Press, Stanford, pp 1–11
Clarke E, Biere A, Raimi R, Zhu Y (2001) Bounded model checking using satisfiability solving. Form Methods Syst Des 19(1): 7–34
Cadar C, Dunbar D, Engler DR (2008) KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Operating systems design and implementation. USENIX Association, pp 209–224
Clarke EM, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. In: Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 168–176
Cimatti A, Micheli A, Narasamdya I, Roveri M (2010) Verifying SystemC: a software model checking approach. In: Form Methods Comput Aided Des. IEEE, pp 51–59
Chakraborty S, Ramesh S, Teich J (2010) Model-based analysis, synthesis and testing of automotive hardware/software architectures. In: International conference on embedded software. ACM, pp 299–300
Dias Neto AC, Horta Travassos G (2010) A picture from the model-based testing area: concepts, techniques, and challenges. Adv Comput 80: 45–120
Donaldson A, Haller L, Kroening D, Rümmer P (2011) Software verification using k-induction. In: Static analysis symposium. Springer, Berlin, pp 351–368
Eén N, Mishchenko A, Amla N (2010) A single-instance incremental SAT formulation of proof- and counterexample-based abstraction. In: Formal methods in computer-aided design. IEEE, pp 181–188
Eén N, Mishchenko A, Brayton RK (2011) Efficient implementation of property directed reachability. In: Formal Methods in Computer-Aided Design. IEEE, pp 125–134
Eén N, Sörensson N (2003) An extensible SAT-solver. In: Theory and applications of satisfiability testing. Springer, Berlin, pp 502–518
Eén N, Sörensson N (2003) Temporal induction by incremental SAT solving. Electron Notes Theor Comput Sci 89: 4–543560
Fleming P, Wallace J (1986) How not to lie with statistics: the correct way to summarize benchmark results. Commun ACM, 29(3): 218–221
Fraser G, Wotawa F, Ammann P (2009) Testing with model checkers: a survey. Softw Test Verif Reliab 19(3): 215–261
Gunnarsson D, Kuntz S, Farrall G, Iwai A, Ernst R (2012) Trends in automotive embedded systems. In: International conference on hardware/software codesign and system synthesis. IEEE, pp 9–10
Günther H, Weissenbacher G (2014) Incremental bounded software model checking. ACM, pp 40–47
Halbwachs N (1993) Synchronous programming of reactive systems. Kluwer
Harman M, Hierons RM (2001) An overview of program slicing. Softw Focus 2(3): 85–92
He N, Hsiao MS (2008) A new testability guided abstraction to solving bit-vector formula. In: International workshop on bit-precise reasoning
Hooker JN (1993) Solving the incremental satisfiability problem. J Log Algebraic Program 15(1&2): 177–186
Herber P, Reicherdt R, Bittner P (2013) Bit-precise formal verification of discrete-time MATLAB/Simulink models using SMT solving. In: International conference on embedded software, pp 1–10
Holzer A, Schallhart C, Tautschnig M, Veith H (2009) Query-driven program testing. In: Verification, model checking, and abstract interpretation. Springer, Berlin, pp 151–166
Hagen G, Tinelli C (2008) Scaling up the formal verification of Lustre programs with SMT-based techniques. In: Formal methods in computer-aided design. IEEE, pp 1–9
Hayhurst KJ, Veerhusen DS, Chilenski JJ, Rierson LK (2001) A practical tutorial on modified condition/decision coverage. Technical report, NASA
ISO 26262: Road vehicles—functional safety (2011)
Inverso O, Tomasco E, Fischer B, La Torre S, Parlato G (2014) Bounded model checking of multi-threaded C programs via lazy sequentialization. In: Computer-aided verification. Springer, Berlin, pp 585–602
Jin H, Somenzi F (2005) An incremental algorithm to check satisfiability for bounded model checking. Electron Notes Theor Comput Sci 119: 2–5165
Kroening D, Lewis M, Weissenbacher G (2015) Under-approximating loops in C programs for fast counterexample detection. Form Methods Syst Des 47(1): 75–92
Kroening D, Ouaknine J, Strichman O, Wahl T, Worrell J (2011) Linear completeness thresholds for bounded model checking. In: Computer-aided verification. Springer, pp 557–572
Kroening D, Strichman O (2003) Efficient computation of recurrence diameters. In: Verification, model checking, and abstract interpretation. Springer, Berlin, pp 298–309
Kroening D, Tautschnig M (2014) CBMC—C bounded model checker—(competition contribution). In: Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 389–391
Kim J, Whittemore J, Sakallah KA, Marques Silva JP (2000) On applying incremental satisfiability to delay fault testing. In: Design automation and test in Europe. IEEE, pp 380–384
Manamcheri K, Mitra S, Bak S, Caccamo M (2011) A step towards verification and synthesis from simulink/stateflow models. In: Hybrid systems: computation and control. ACM, pp 317–318
Petrenko A, daSilva Simão A, Maldonado JC (2012) Model-based testing of software and systems: recent advances and challenges. J Softw Tools Technol Transf 14(4): 383–386
Peranandam P, Raviram S, Satpathy M, Yeolekar A, Gadkari AA, Ramesh S (2012) An integrated test generation tool for enhanced coverage of simulink/stateflow models. In: Design automation and test in Europe. IEEE, pp 308–311
Pnueli A, Strichman O (2006) Reduced functional consistency of uninterpreted functions. Electron Notes Theor Comput Sci 144(2): 53–65
Schrammel P, Kroening D (2016) 2LS for program analysis—(competition contribution). In: Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 905–907
Schrammel P, Kroening D, Brain M, Martins R, Teige T, Bienmüller T (2015) Successful use of incremental BMC in the automotive industry. In: Formal methods for industrial critical systems. Springer, Berlin, pp 62–76
Silva JM, Sakallah KA (1997) Robust search algorithms for test pattern generation. IEEE, pp 152–161
Sheeran M, Singh S, Stålmarck G (2000) Checking safety properties using induction and a SAT-solver. In: Formal methods in computer-aided design, volume 1954 of LNCS. IEEE, pp 108–125
Stump A, Sutcliffe G, Tinelli C (2014) StarExec: a cross-community infrastructure for logic solving. In: International joint conference on automated reasoning, pp 367–373
Strichman O (2001) Pruning techniques for the SAT-based bounded model checking problem. Springer, Berlin, pp 58–70
Satpathy M, Yeolekar A, Ramesh S (2008) Randomized directed testing (REDIRECT) for simulink/stateflow models. In: International conference on embedded software, pp 217–226
Tip F (1994) A survey of program slicing techniques. Technical report, CWI-Amsterdam
Wieringa S (2011) On incremental satisfiability and bounded model checking. In: Design and implementation of formal tools and systems, pp 46–54
Whittemore J, Kim J, Sakallah KA (2001) SATIRE: a new incremental satisfiability engine. In: Design automation conference. ACM, pp 542–545
Author information
Authors and Affiliations
Corresponding author
Additional information
Communicated by Michael Butler and Jim Woodcock
The research leading to these results has received funding from the ARTEMIS Joint Undertaking under Grant Agreement Number 295311 “VeTeSS” and ERC Project 280053 “CPROVER”.
Rights and permissions
Open Access This article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.
About this article
Cite this article
Schrammel, P., Kroening, D., Brain, M. et al. Incremental bounded model checking for embedded software. Form Asp Comp 29, 911–931 (2017). https://doi.org/10.1007/s00165-017-0419-1
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-017-0419-1