###
Journal of Software:2015.26(9):2212-2230

中断驱动系统模型检验
周筱羽,顾斌,赵建华,杨孟飞,李宣东
(计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023;南京大学 软件学院, 江苏 南京 210093;西北工业大学 计算机学院, 陕西 西安 710072;计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023;南京大学 计算机科学与技术系, 江苏 南京 210023;中国空间技术研究院, 北京 100094)
Model Checking Technique for Interrupt-Driven System
ZHOU Xiao-Yu,GU Bin,ZHAO Jian-Hua,YANG Meng-Fei,LI Xuan-Dong
(State Key Laboratory for Novel Software Technology (Nanjing University), Nanjing 210023, China;Institute of Software Engineering, Nanjing University, Nanjing 210093, China;School of Computer Science and Engineering, Northwestern Polytechnical University, Xi'an 710072, China;State Key Laboratory for Novel Software Technology (Nanjing University), Nanjing 210023, China;Department of Computer Science and Technology, Nanjing University, Nanjing 210023, China;China Academy of Space Technology, Beijing 100094, China)
Abstract
Chart / table
Reference
Similar Articles
Article :Browse 2748   Download 2182
Received:October 16, 2013    Revised:April 18, 2014
> 中文摘要: 针对一类中断驱动系统提出了一种建模和模型检验的方法.该系统通常由中断处理程序和操作系统调度的任务组成,前者由中断源触发后处理中断事件,后者则负责处理系统的日常任务以及某些中断处理事件的后续处理.因为这类系统是实时控制系统,对中断事件的处理需要在规定时间内响应并完成,否则可能造成严重的系统失效.为了帮助系统设计人员在系统设计过程中应用模型检验技术来提高系统的正确性,首先确定了此类系统中与时序性质相关的系统要素(包括系统调度任务、中断源、中断处理程序)和相关参数,并要求设计人员在设计阶段明确指出这些要素的参数.然后,提出了将这些要素和参数自动转化为形式化模型的方法:使用时间自动机对中断事件进行建模,使用中断向量表和CPU处理栈对中断处理过程进行建模.对于得到的形式化模型,给出了针对中断处理超时错误的检测方法,并在此基础上给出了针对共享资源的完整性、子程序原子性的检验方法.
Abstract: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.
文章编号:     中图分类号:    文献标志码:
基金项目:国家自然科学基金(91118007); 国家高技术研究发展计划(863)(2011AA010103) 国家自然科学基金(91118007); 国家高技术研究发展计划(863)(2011AA010103)
Foundation items:
Reference text:

周筱羽,顾斌,赵建华,杨孟飞,李宣东.中断驱动系统模型检验.软件学报,2015,26(9):2212-2230

ZHOU Xiao-Yu,GU Bin,ZHAO Jian-Hua,YANG Meng-Fei,LI Xuan-Dong.Model Checking Technique for Interrupt-Driven System.Journal of Software,2015,26(9):2212-2230