Effective verification for low-level software with competing interrupts
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...
| Main Authors: | , , , , |
|---|---|
| Format: | Journal article |
| Published: |
Association for Computing Machinery
2017
|
| _version_ | 1797106304187105280 |
|---|---|
| author | Liang, L Melham, T Kroening, DHF Schrammel, P Tautschnig, M |
| author_facet | Liang, L Melham, T Kroening, DHF Schrammel, P Tautschnig, M |
| author_sort | Liang, L |
| collection | OXFORD |
| description | 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 |
| first_indexed | 2024-03-07T06:59:50Z |
| format | Journal article |
| id | oxford-uuid:ff5a4b5a-fbfd-4c7b-8b57-5a1779ca8c9c |
| institution | University of Oxford |
| last_indexed | 2024-03-07T06:59:50Z |
| publishDate | 2017 |
| publisher | Association for Computing Machinery |
| record_format | dspace |
| spelling | oxford-uuid:ff5a4b5a-fbfd-4c7b-8b57-5a1779ca8c9c2022-03-27T13:44:21ZEffective verification for low-level software with competing interruptsJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:ff5a4b5a-fbfd-4c7b-8b57-5a1779ca8c9cSymplectic Elements at OxfordAssociation for Computing Machinery2017Liang, LMelham, TKroening, DHFSchrammel, PTautschnig, MInterrupt-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 |
| spellingShingle | Liang, L Melham, T Kroening, DHF Schrammel, P Tautschnig, M Effective verification for low-level software with competing interrupts |
| title | Effective verification for low-level software with competing interrupts |
| title_full | Effective verification for low-level software with competing interrupts |
| title_fullStr | Effective verification for low-level software with competing interrupts |
| title_full_unstemmed | Effective verification for low-level software with competing interrupts |
| title_short | Effective verification for low-level software with competing interrupts |
| title_sort | effective verification for low level software with competing interrupts |
| work_keys_str_mv | AT liangl effectiveverificationforlowlevelsoftwarewithcompetinginterrupts AT melhamt effectiveverificationforlowlevelsoftwarewithcompetinginterrupts AT kroeningdhf effectiveverificationforlowlevelsoftwarewithcompetinginterrupts AT schrammelp effectiveverificationforlowlevelsoftwarewithcompetinginterrupts AT tautschnigm effectiveverificationforlowlevelsoftwarewithcompetinginterrupts |