×

zbMATH — the first resource for mathematics

Incremental bounded model checking for embedded software. (English) Zbl 1375.68081
Summary: 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.
MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] 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 · Zbl 1159.68403
[2] 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 · Zbl 1187.68168
[3] Brummayer, R; Biere, A, Lemmas on demand for the extensional theory of arrays, J Satisf Boolean Model Comput, 6, 165-201, (2009) · Zbl 1187.68168
[4] Brummayer R, Biere A (2009) Effective bit-width and under-approximation. In: Computer aided systems theory. Springer, Berlin, pp 304-311
[5] 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
[6] Beyer D, Dangl M, Wendler P (2015) Boosting k-induction with continuously-refined invariants. In Computer-aided verification. Springer, Berlin, pp 622-640
[7] Biere, A, Picosat essentials, J Satisf Boolean Model Comput, 4, 75-97, (2008) · Zbl 1159.68403
[8] 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
[9] 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 · Zbl 1186.68281
[10] Bryant, RE; Kroening, D; Ouaknine, J; Seshia, SA; Strichman, O; Brady, BA, An abstraction-based decision procedure for bit-vector arithmetic, J Softw Tools Technol Transf, 11, 95-104, (2009) · Zbl 1186.68281
[11] Brillout A, Kroening D, Wahl T (2009) Mixed abstractions for floating-point arithmetic. In: Formal methods in computer-aided design. IEEE, pp 69-76
[12] Bradley AR (2012) IC3 and beyond: incremental, inductive verification. In: Computer-aided verification. Springer, Berlin, p 4 · Zbl 1322.68054
[13] 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 · Zbl 0787.68049
[14] Clarke, E; Biere, A; Raimi, R; Zhu, Y, Bounded model checking using satisfiability solving, Form Methods Syst Des, 19, 7-34, (2001) · Zbl 0985.68038
[15] 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
[16] 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 · Zbl 1126.68470
[17] 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 · Zbl 0787.68049
[18] 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
[19] Dias Neto, AC; Horta Travassos, G, A picture from the model-based testing area: concepts, techniques, and challenges, Adv Comput, 80, 45-120, (2010)
[20] Donaldson A, Haller L, Kroening D, Rümmer P (2011) Software verification using \(k\)-induction. In: Static analysis symposium. Springer, Berlin, pp 351-368
[21] 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 · Zbl 0985.68038
[22] 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
[23] Eén N, Sörensson N (2003) An extensible SAT-solver. In: Theory and applications of satisfiability testing. Springer, Berlin, pp 502-518
[24] Eén, N; Sörensson, N, Temporal induction by incremental SAT solving, Electron Notes Theor Comput Sci, 89, 4-543560, (2003) · Zbl 1271.68215
[25] Fleming, P; Wallace, J, How not to Lie with statistics: the correct way to summarize benchmark results, Commun ACM,, 29, 218-221, (1986)
[26] Fraser, G; Wotawa, F; Ammann, P, Testing with model checkers: a survey, Softw Test Verif Reliab, 19, 215-261, (2009)
[27] 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 · Zbl 1271.68215
[28] Günther H, Weissenbacher G (2014) Incremental bounded software model checking. ACM, pp 40-47
[29] Halbwachs N (1993) Synchronous programming of reactive systems. Kluwer · Zbl 0828.68038
[30] Harman, M; Hierons, RM, An overview of program slicing, Softw Focus, 2, 85-92, (2001)
[31] He N, Hsiao MS (2008) A new testability guided abstraction to solving bit-vector formula. In: International workshop on bit-precise reasoning
[32] Hooker, JN, Solving the incremental satisfiability problem, J Log Algebraic Program, 15, 177-186, (1993) · Zbl 0787.68049
[33] 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
[34] 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 · Zbl 1206.68089
[35] 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
[36] Hayhurst KJ, Veerhusen DS, Chilenski JJ, Rierson LK (2001) A practical tutorial on modified condition/decision coverage. Technical report, NASA
[37] ISO 26262: Road vehicles—functional safety (2011)
[38] 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
[39] Jin, H; Somenzi, F, An incremental algorithm to check satisfiability for bounded model checking, Electron Notes Theor Comput Sci, 119, 2-5165, (2005) · Zbl 1272.68262
[40] Kroening, D; Lewis, M; Weissenbacher, G, Under-approximating loops in C programs for fast counterexample detection, Form Methods Syst Des, 47, 75-92, (2015) · Zbl 1322.68054
[41] 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 · Zbl 1360.68592
[42] Kroening D, Strichman O (2003) Efficient computation of recurrence diameters. In: Verification, model checking, and abstract interpretation. Springer, Berlin, pp 298-309 · Zbl 1022.68579
[43] 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
[44] 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
[45] 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
[46] Petrenko, A; daSilva Simão, A; Maldonado, JC, Model-based testing of software and systems: recent advances and challenges, J Softw Tools Technol Transf, 14, 383-386, (2012)
[47] 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
[48] Pnueli, A; Strichman, O, Reduced functional consistency of uninterpreted functions, Electron Notes Theor Comput Sci, 144, 53-65, (2006) · Zbl 1272.03071
[49] 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
[50] 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
[51] Silva JM, Sakallah KA (1997) Robust search algorithms for test pattern generation. IEEE, pp 152-161 · Zbl 1272.68262
[52] 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
[53] 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 · Zbl 06348250
[54] Strichman O (2001) Pruning techniques for the SAT-based bounded model checking problem. Springer, Berlin, pp 58-70 · Zbl 1002.68511
[55] Satpathy M, Yeolekar A, Ramesh S (2008) Randomized directed testing (REDIRECT) for simulink/stateflow models. In: International conference on embedded software, pp 217-226
[56] Tip F (1994) A survey of program slicing techniques. Technical report, CWI-Amsterdam
[57] Wieringa S (2011) On incremental satisfiability and bounded model checking. In: Design and implementation of formal tools and systems, pp 46-54
[58] Whittemore J, Kim J, Sakallah KA (2001) SATIRE: a new incremental satisfiability engine. In: Design automation conference. ACM, pp 542-545
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.