中断驱动系统模型检验

来源：软件学报杂志2015年第9期北京时间：

作者：周筱羽,顾斌,赵建华,杨孟飞,李宣东

单位：周筱羽，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023;南京大学 软件学院, 江苏 南京 21009311,顾斌，西北工业大学 计算机学院, 陕西 西安 71007202,赵建华，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023;南京大学 计算机科学与技术系, 江苏 南京 21002303,杨孟飞，中国空间技术研究院, 北京 10009404,李宣东，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023;南京大学 计算机科学与技术系, 江苏 南京 21002305

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

关键词：中断驱动系统;模型检验;超时检测

基金资助：国家自然科学基金(91118007); 国家高技术研究发展计划(863)(2011AA010103)