主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
周筱羽,顾斌,赵建华,杨孟飞.中断驱动控制系统的有界模型检验技术.软件学报,2015,26(10):2485-2503
中断驱动控制系统的有界模型检验技术
Bounded Model Checking Technique for Interrupt-Driven Systems
投稿时间:2014-07-01  修订日期:2014-10-31
DOI:10.13328/j.cnki.jos.004790
中文关键词:  中断驱动系统  有界模型检验  超时检测
英文关键词:interrupt-driven system  bounded model checking  deadline detection
基金项目:国家自然科学基金(91118007,61321491);国家高技术研究发展计划(863)(2012AA011205)
作者单位E-mail
周筱羽 计算机软件新技术国家重点实验室南京大学, 江苏 南京 210023
南京大学 软件学院, 江苏 南京 210093 
 
顾斌 西北工业大学 计算机学院, 陕西 西安 710072  
赵建华 计算机软件新技术国家重点实验室南京大学, 江苏 南京 210023
南京大学 计算机科学与技术系, 江苏 南京 210023 
zhaojh@mail.nju.edu.cn 
杨孟飞 中国空间技术研究院, 北京 100094  
摘要点击次数: 1528
全文下载次数: 1904
中文摘要:
      针对一类中断驱动的航天控制系统,给出了有界模型检验的算法.这类系统由中断处理程序和操作系统调度的任务组成.当中断发生时,对应的中断处理程序响应中断事件,并可以修改控制变量值,以便在系统任务中完成后续工作.操作系统周期性地调度任务序列处理日常事务以及中断事件的后续工作.使用了带中断标记的时间自动机对中断事件和任务调度事件进行建模,并使用中断向量表和中断处理程序的伪代码模型共同描述中断的处理过程.控制变量将中断处理过程和系统任务相关联,中断处理程序可以设定某个控制变量,而系统任务则通过检查该控制变量来确定是否需要进行后续处理.对于这样的形式化模型,给出了检验关键时序性质的有界模型检验算法.该算法使用深度优先的方式遍历所有长度小于等于K的可行路径,并使用SMT Z3实现了对时间约束和规约的处理.
英文摘要:
      This paper proposes an approach to model and verify a certain class of interrupt-driven aerospace control systems. These interrupt-driven systems consist of interrupt handlers and system-scheduling tasks. When an interrupt event occurs, the corresponding interrupt-handler executes in response. An interrupt-handler may leave some post-processing works to the system tasks by setting some control variables to certain values. The operating system schedules a set of tasks periodically to deal with routine tasks and some post-processing of interrupt events. In this paper, timed automata labeled with interrupts are used to model interrupt events and task scheduling events. The execution processes of interrupts are modeled by pseudo-code of interrupt handlers and the interrupt vector. Control variables are used to model the interactions between interrupt processing and system tasks while the tasks perform post-processing of interrupts according to the values of control variables set by interrupt handlers. A bounded model checking algorithm is presented in this paper to check these models w.r.t some important timing properties. The algorithm explores all feasible paths in K steps using the depth-first searching method. During the exploring process, time constraints and time requirements in the specification are calculated by the SMT solver Z3.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利