Easy Modelling and Verification of Unpredictable and Preemptive Interrupt-Driven Systems

Minxue Pan, Shouyu Chen, Yu Pei, Tian Zhang, Xuandong Li

Research output: Chapter in book / Conference proceedingConference article published in proceeding or bookAcademic researchpeer-review

4 Citations (Scopus)

Abstract

The widespread real-time and embedded systems are mostly interrupt-driven because their heavy interaction with the environment is often initiated by interrupts. With the interrupt arrival being unpredictable and the interrupt handling being preemptive, a large number of possible system behaviours are generated, which makes the correctness assurance of such systems difficult and costly. Model checking is considered to be one of the effective methods for exhausting behavioural state space for correctness. However, existing modelling approaches for interrupt-driven systems are based on either calculus or automata theory, and have a steep learning curve. To address this problem, we propose a new modelling language called interrupt sequence diagram (ISD). By extending the popular UML sequence diagram notations, the ISD supports the modelling of interrupts' essential features visually and concisely. We also propose an automata-based semantics for ISD, based on which ISD can be transformed to a subset of hybrid automata so as to leverage the abundant off-the-shelf checkers. Experiments on examples from both real-world and existing literature were conducted, and the results demonstrate our approach's usability and effectiveness.

Original languageEnglish
Title of host publicationProceedings - 2019 IEEE/ACM 41st International Conference on Software Engineering, ICSE 2019
PublisherIEEE Computer Society
Pages212-222
Number of pages11
ISBN (Electronic)9781728108698
DOIs
Publication statusPublished - May 2019
Event41st IEEE/ACM International Conference on Software Engineering, ICSE 2019 - Montreal, Canada
Duration: 25 May 201931 May 2019

Publication series

NameProceedings - International Conference on Software Engineering
Volume2019-May
ISSN (Print)0270-5257

Conference

Conference41st IEEE/ACM International Conference on Software Engineering, ICSE 2019
CountryCanada
CityMontreal
Period25/05/1931/05/19

Keywords

  • Interrupt-driven systems
  • Model checking
  • Sequence diagrams
  • System modelling

ASJC Scopus subject areas

  • Software

Cite this