paper.pdf (426.67 kB)
Effective verification for low-level software with competing interrupts
journal contribution
posted on 2023-06-09, 07:30 authored by Lihao Liang, Tom Melham, Daniel Kroening, Peter Schrammel, Michael TautschnigInterrupt-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 exponential blow-up in the number of cases to consider. 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 approaches that use source-to-source transformations. Our results show that our method significantly outperforms these techniques. To the best of our knowledge, our work is the first to demonstrate effective verification of low-level embedded software with nested interrupts.
History
Publication status
- Published
File Version
- Accepted version
Journal
ACM Transactions on Embedded Computing SystemsISSN
1539-9087Publisher
Association for Computing MachineryExternal DOI
Issue
2Volume
17Page range
1-26Article number
a36Department affiliated with
- Informatics Publications
Full text available
- Yes
Peer reviewed?
- Yes
Legacy Posted Date
2017-08-02First Open Access (FOA) Date
2017-12-12First Compliant Deposit (FCD) Date
2017-08-01Usage metrics
Categories
No categories selectedLicence
Exports
RefWorks
BibTeX
Ref. manager
Endnote
DataCite
NLM
DC