Name
Abstract | ||
|---|---|---|
Safety property checking is mandatory in the validation process of critical software. When formal verification tools fail to prove some properties, the automatic generation of counterexamples for a given loop depth is an important issue in practice. We investigate in this paper the capabilities of constraint-based bounded model checking for program verification and counterexample generation on real applications. We introduce dynamic post-condition variable-driven strategy (DPVS), a new backjumping strategy we developed to handle an industrial application from a car manufacturer, the Flasher Manager. This backjumping strategy is used to search a faulty path and to collect the constraints of such a path. The simplified control flow graph (CFG) of the program is explored in a backward way, starting from the post-condition and jumping to the most promising node where the variables of the post-condition are defined. In other words, the constraints are collected by exploring the CFG in a dynamic and non-sequential backward way. The Flasher Manager application has been designed and simulated using the Simulink platform. However, this module is concretely embedded as a C program in a car computer, thus we have to check that the safety properties are preserved on this C code. We report experiments on the Flasher Manager with our constraint-based bounded model checker, and with CBMC, a state-of-the-art bounded model checker. Experiments show that DPVS and CBMC have similar performances on one property of the Flasher Manager; DPVS outperforms CBMC to find a counterexample for two properties; two of the properties of the Flasher Manager remain intractable for CBMC and DPVS. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1007/s10009-012-0258-6 | STTT |
Keywords | DocType | Volume |
Embedded systems, Validation, Constraint-based bounded model checking, Counterexample generation | Journal | 16 |
Issue | ISSN | Citations |
1 | 1433-2787 | 1 |
PageRank | References | Authors |
0.36 | 24 | 5 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Hélène Collavizza | 1 | 146 | 13.12 |
| Nguyen Le Vinh | 2 | 3 | 0.74 |
| Olivier Ponsini | 3 | 46 | 4.49 |
| Michel Rueher | 4 | 613 | 59.81 |
| Antoine Rollet | 5 | 62 | 9.53 |