Name
Abstract | ||
|---|---|---|
Context-bounded model checking has been used successfully to verify safety properties in multi-threaded systems automatically, even if they are implemented in low-level programming languages such as C. In this paper, we describe and experiment with an approach to extend context-bounded software model checking to safety and liveness properties expressed in linear-time temporal logic (LTL). Our approach checks the actual C program, rather than an extracted abstract model. It converts the LTL formulas into Büchi automata for the corresponding never claims and then further into C monitor threads that are interleaved with the execution of the program under analysis. This combined system is then checked using the ESBMC model checker. We use an extended, four-valued LTL semantics to handle the finite traces that bounded model checking explores; we thus check the combined system several times with different acceptance criteria to derive the correct truth value. In order to mitigate the state space explosion, we use a dedicated scheduler that selects the monitor thread only after updates to global variables occurring in the LTL formula. We demonstrate our approach on the analysis of the sequential firmware of a medical device and a small multi-threaded control application. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1007/s10270-013-0366-0 | Software and Systems Modeling (SoSyM) |
Keywords | Field | DocType |
software verification,model checking,linear temporal logic | Computation tree logic,Abstraction model checking,Model checking,Programming language,ANSI C,Computer science,Theoretical computer science,Linear temporal logic,Büchi automaton,Liveness,Global variable | Journal |
Volume | Issue | ISSN |
14 | 1 | 1619-1374 |
Citations | PageRank | References |
11 | 0.56 | 35 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jeremy Morse | 1 | 80 | 7.10 |
| Lucas Cordeiro | 2 | 360 | 38.38 |
| Denis Nicole | 3 | 41 | 2.96 |
| Bernd Fischer | 4 | 371 | 28.86 |