Effective verification for low-level software with competing interrupts

Liang, Lihao, Melham, Tom, Kroening, Daniel, Schrammel, Peter and Tautschnig, Michael (2017) Effective verification for low-level software with competing interrupts. ACM Transactions on Embedded Computing Systems, 17 (2). 36:1-36:26. ISSN 1539-9087

[img] PDF (© ACM, 2017. This is the author's version of the work. It is posted here by permission of ACM. Not for redistribution. The definitive version was published inACM Transactions on Embedded Computing Systems https://doi.org/10.1145/3147432) - Accepted Version
Download (436kB)


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 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.

Item Type: Article
Keywords: verification, concurrency, interrupts, bounded model checking
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: 02 Aug 2017 08:05
Last Modified: 12 Dec 2017 14:35
URI: http://srodev.sussex.ac.uk/id/eprint/69534

View download statistics for this item

📧 Request an update