direkt zum Inhalt springen

direkt zum Hauptnavigationsmenü

Sie sind hier

TU Berlin

Inhalt des Dokuments

Gastvorträge 2013

Model Checking LTL Properties over C Programs with Bounded Traces
Bernd Fischer, Stellenbosch University, SA
Tuesday, September 17, 2013, 2 p.m., TU Hochhaus, 10th floor, room 1011

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. 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 Buechi automata (BA) for the corresponding never claims and then further into C monitor threads, which 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. We demonstrate our approach on the analysis of the sequential firmware of a medical device, a small multi-threaded control application and the RERS Greybox Challenge tasks.

Contact

Alexandra Mehlhase, SWT

Zusatzinformationen / Extras

Direktzugang

Schnellnavigation zur Seite über Nummerneingabe