Paper Info
Title
Effective verification of low-level software with nested interrupts
Abstract
Interrupt-driven software is difficult to test and debug, especially when interrupts can be nested and subject to priorities. Interrupts can arrive at arbitrary times, leading to an explosion in the number of cases to be considered. We present a new formal approach to verifying interrupt-driven software based on symbolic execution. The approach leverages recent advances in the encoding of the execution traces of interacting, concurrent threads. We assess the performance of our method on benchmarks drawn from embedded systems code and device drivers, and experimentally compare it to conventional formal approaches that use source-to-source transformations. Our experimental results show that our method significantly outperforms conventional techniques. To the best of our knowledge, our technique is the first to demonstrate effective formal verification of low-level embedded software with nested interrupts.
Year
Venue
Keywords
2015
DATE
simulation,multicore,fpga,radio frequency,embedded systems,emulation,encoding,semantics,interrupts,formal verification,instruction sets,benchmark testing
Field
DocType
ISSN
Programming language,Embedded software,Computer science,Parallel computing,Real-time computing,Software,Symbolic execution,Formal methods,Software construction,Formal verification,Software verification,Debugging
Conference
1530-1591
Citations 
PageRank 
References 
8
0.52
14
Authors
5
Name
Order
Citations
PageRank
Daniel Kroening13084187.60
Lihao Liang2121.37
Thomas F. Melham338435.63
Peter Schrammel413419.10
Michael Tautschnig542525.84