Trabalho em anais de evento

Context-Bounded Model Checking of LTL Properties for ANSI-C Software

MORSE, J.; CORDEIRO, L. C.; NICOLE, D.; FISCHER, BERND

2011 • 9th International Conference on Software Engineering and Formal Methods • 19 citações

Resumo

Context-bounded model checking has successfully been used to verify safety properties in multi-threaded systems automatically, even if they are implemented in low-level programming languages like ANSIC. In this paper, we describe and experiment with an approach to extend context-bounded model checking to liveness properties expressed in linear-time temporal logic (LTL). Our approach converts the LTL formulae into Buchi-automata and then further into C monitor threads, which are interleaved with the execution of the program under test. This combined system is then checked using the ESBMC model checker. Since this approach explores a larger number of interleavings than normal context-bounded model checking, we use a state hashing technique which substantially reduces the number of redundant interleavings that are explored and so mitigates state space explosion. Our experimental results show that we can verify non-trivial properties in the firmware of a medical device.

palavras-chave

Palavras-chave

linear temporal logicliveness propertiesANSI CBüchi automataESBMCstate space explosionmulti-threaded systemsfirmware verificationmedical device software

Status

Published

links