一句话：提出中断序列图 ISD 及其自动机语义，将中断驱动系统转换为混合自动机以复用模型检测器。
中断驱动系统广泛存在于实时嵌入式领域，其中断到达不可预测、处理可抢占，导致行为状态空间巨大，正确性保障困难且昂贵。现有建模方法基于演算或自动机理论，学习曲线陡峭。本文提出建模语言 ISD（中断序列图），扩展 UML 序列图以直观简洁地刻画中断的关键特性；并给出基于自动机的语义，将 ISD 转换为混合自动机子集，从而复用现有模型检测器。来自真实世界和文献的实例实验表明该方法可用且有效。
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.
@inproceedings{PanCP0L19,
title = {Easy Modelling and Verification of Unpredictable and Preemptive Interrupt-Driven Systems},
author = {Minxue Pan and Shouyu Chen and Yu Pei and Tian Zhang and Xuandong Li},
booktitle = {ICSE},
year = {2019},
doi = {10.1109/icse.2019.00037}
}