中断驱动系统模型检验

针对一类中断驱动系统提出了一种建模和模型检验的方法.该系统通常由中断处理程序和操作系统调度的任务组成,前者由中断源触发后处理中断事件,后者则负责处理系统的日常任务以及某些中断处理事件的后续处理.因为这类系统是实时控制系统,对中断事件的处理需要在规定时间内响应并完成,否则可能造成严重的系统失效.为了帮助系统设计人员在系统设计过程中应用模型检验技术来提高系统的正确性,首先确定了此类系统中与时序性质相关的系统要素(包括系统调度任务、中断源、中断处理程序)和相关参数,并要求设计人员在设计阶段明确指出这些要素的参数.然后,提出了将这些要素和参数自动转化为形式化模型的方法:使用时间自动机对中断事件进行建模,使用中断向量表和CPU处理栈对中断处理过程进行建模.对于得到的形式化模型,给出了针对中断处理超时错误的检测方法,并在此基础上给出了针对共享资源的完整性、子程序原子性的检验方法.

Model Checking Technique for Interrupt-Driven System

In this paper, an approach is proposed to model and verify a class of interrupt-driven systems. An interrupt-driven system usually consists of interrupt handlers and system-scheduling tasks. When an interrupt occurs, the corresponding interrupt-handler executes in response. The operating system schedules a set of tasks to deal with routine events and certain post-processing of some interrupts. In the real-time control system, it is important that interrupts are handled within their specific deadlines, otherwise, it may cause catastrophic system failures. In order to improve the reliability of interrupt-driven systems, model checking technique is introduced to the design and development process. Through analyzing numerous systems, the major system elements (including system scheduling tasks, interrupts and their handlers) and their parameters relevant to time-related failures are identified. When these parameters are specified by system designer in the design process, formal models can be constructed by the modeling method in this paper: The interrupt source is modeled as timed automata. The execution processes of interrupt handlers are modeled by the interrupt vector and the CPU process stack. A model-checking algorithm is provided to check the above formal model whether interrupt handlers can be executed within their response deadlines. Moreover, a variation of this algorithm is developed to check properties of the integrity of shared resources and the atomicity of subprograms.