中断驱动系统模型检验

• 作者: 周筱羽 李宣东 杨孟飞 赵建华 顾斌
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 中断驱动系统 模型检验 超时检测
• 年，卷（期）: 2015,（9）
• 所属期刊栏目: 系统软件与软件工程
• 页码范围: 2212-2230
• 页数: 19页
• 分类号: TP311
• 字数: 19749字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.004713

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	杨孟飞		45	222	10.0	12.0
2	顾斌	西北工业大学计算机学院	8	27	3.0	5.0