University of Sussex
Browse

File(s) under permanent embargo

Effective verification of low-level software with nested interrupts

chapter
posted on 2023-06-09, 00:29 authored by Daniel Kroening, Lihao Liang, Tom Melham, Peter Schrammel, Michael Tautschnig
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.

History

Publication status

  • Published

File Version

  • Published version

Publisher

ACM

Page range

229-234

Event name

Design, Automation & Test in Europe Conference & Exhibition, DATE 2015

Book title

Proceedings of the 2015 Design, Automation & Test in Europe Conference & Exhibition

ISBN

9783981537048

Department affiliated with

  • Informatics Publications

Full text available

  • No

Peer reviewed?

  • Yes

Legacy Posted Date

2016-05-09

First Compliant Deposit (FCD) Date

2016-05-09

Usage metrics

    University of Sussex (Publications)

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC