Effective verification of low-level software with nested interrupts

Kroening, Daniel, Liang, Lihao, Melham, Tom, Schrammel, Peter and Tautschnig, Michael (2015) Effective verification of low-level software with nested interrupts. In: Proceedings of the 2015 Design, Automation & Test in Europe Conference & Exhibition. ACM, pp. 229-234. ISBN 9783981537048

[img] PDF - Published Version
Restricted to SRO admin only

Download (193kB)


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.

Item Type: Book Section
Keywords: software verification, concurrency, interrupts, partial order encoding
Schools and Departments: School of Engineering and Informatics > Informatics
Subjects: Q Science > QA Mathematics > QA0075 Electronic computers. Computer science
Depositing User: Peter Schrammel
Date Deposited: 09 May 2016 05:32
Last Modified: 09 May 2016 05:32
URI: http://srodev.sussex.ac.uk/id/eprint/59914

View download statistics for this item

📧 Request an update