中断驱动控制系统的有界模型检验技术

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

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

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

摘要：针对一类中断驱动的航天控制系统,给出了有界模型检验的算法.这类系统由中断处理程序和操作系统调度的任务组成.当中断发生时,对应的中断处理程序响应中断事件,并可以修改控制变量值,以便在系统任务中完成后续工作.操作系统周期性地调度任务序列处理日常事务以及中断事件的后续工作.使用了带中断标记的时间自动机对中断事件和任务调度事件进行建模,并使用中断向量表和中断处理程序的伪代码模型共同描述中断的处理过程.控制变量将中断处理过程和系统任务相关联,中断处理程序可以设定某个控制变量,而系统任务则通过检查该控制变量来确定是否需要进行后续处理.对于这样的形式化模型,给出了检验关键时序性质的有界模型检验算法.该算法使用深度优先的方式遍历所有长度小于等于K的可行路径,并使用SMT Z3实现了对时间约束和规约的处理.

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

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