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. ISSN 1539-9087 (Accepted)

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

Download (436kB)

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 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
Q Science > QA Mathematics > QA0076 Computer software
Depositing User: Peter Schrammel
Date Deposited: 02 Aug 2017 08:05
Last Modified: 02 Aug 2017 08:08
URI: http://sro.sussex.ac.uk/id/eprint/69534

View download statistics for this item

📧 Request an update