一种中断驱动系统的时间约束验证方法

摘要

Interrupt is an important mechanism for embedded systems to support real-time response.Classical testing based approaches lost efficiency in treating those systems,since the space of possible execution traces are infinite.The paper proposes a new method to verify the time constraints of interrupt-driven systems based on bounded verification technology for linear hybrid systems.It models interrupt-driven systems as the linear hybrid automata and translates the problem of verifying time constraints into the problem of deciding the reach ability of giving paths in hybrid automata.The model checker BACH is introduced to solve the reach ability problem.A case study is taken on a system driven by periodic interrupt.It shows the availability and effectiveness of our approach.%中断是嵌入式系统进行实时响应的重要机制.以测试为基础的传统方法在处理中断驱动的系统时,由于系统可能的运行轨迹空间无穷,其有效性受到很大的影响.本文基于线性混成自动机有界验证技术提出一种对中断驱动系统的时间约束进行验证的方法,应用线性混成自动机对中断驱动的系统建模,将时间约束验证问题转换成线性混成自动机上的路径可达性判定问题,并借助模型检验工具BACH来进行验证,以周期性中断源驱动的嵌入式系统为例,说明了方法的可行性和有效性.