Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Incremental bounded model checking for embedded software
Schrammel P., Kroening D., Brain M., Martins R., Teige T., Bienmüller T. Formal Aspects of Computing29 (5):911-931,2017.Type:Article
Date Reviewed: Dec 4 2017

Bounded model checking is employed in tools for the formal verification of C programs such as the C bounded model checker (CBMC). The key idea of this technique is to unwind unbounded program loops to a fixed depth and to translate the resulting program into a formula whose satisfiability (determined by a Boolean satisfiability problem/satisfiability modulo theory (SAT/SMT) solver) indicates a runtime error or the failure of a safety property, respectively. Confidence in the program is established by checking programs for growing unwinding depths yielding growing formulas to be solved; this, however, is wasteful because it repeats work from solving previous formulas.

This paper capitalizes on recent advances in incremental SAT solving, which is able to reuse work spent on solving smaller formulas for solving extended formulas. Specifically, it demonstrates how the formulas derived from time-triggered systems such as automotive embedded systems (which only contain a single unbounded loop) are amenable to a formula encoding in which the problem of non-monotonic formula extensions is addressed by additional Boolean variables that “switch off” clauses from previously checked formulas; furthermore, this technique does not interfere with SAT optimization techniques like symbolic execution and slicing.

The paper clearly illustrates the core ideas also for nonexperts and demonstrates their advantages by benchmarking an extended version of CBMC on various industrial programs from the automotive industry; for these, with incremental checking, a speedup in the range of five to ten times can be achieved. The demonstrated results are promising with possible extensions to improve its performance and range of applicability, for example, to concurrent programs.

Reviewer:  Wolfgang Schreiner Review #: CR145694 (1802-0082)
Bookmark and Share
  Featured Reviewer  
 
Model Checking (D.2.4 ... )
 
 
Real-Time Systems And Embedded Systems (D.4.7 ... )
 
Would you recommend this review?
yes
no
Other reviews under "Model Checking": Date
Systems and software verification: model-checking techniques and tools
B ., Bidoit M., Finkel A., Laroussinie F., Petit A., Petrucci L., Schnoebelen P., McKenzie P., Springer-Verlag New York, Inc., New York, NY, 1999.  190, Type: Book (9783540415237)
Sep 30 2002
Module checking
Kupferman O., Vardi M., Wolper P. Information and Computation 164(2): 322-344, 2001. Type: Article
Mar 1 2002
SMC: a symmetry-based model checker for verification of safety and liveness properties
Sistla A., Gyuris V., Emerson E. ACM Transactions on Software Engineering and Methodology 9(2): 133-166, 2000. Type: Article
Sep 1 2000
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy