| 本文已被：浏览 3582次 下载 5942次 |
码上扫一扫！ |
|
|
| 中断驱动控制系统的有界模型检验技术 |
|
周筱羽1,2, 顾斌3, 赵建华1,4, 杨孟飞5
|
|
1.计算机软件新技术国家重点实验室南京大学, 江苏 南京 210023;2.南京大学 软件学院, 江苏 南京 210093;3.西北工业大学 计算机学院, 陕西 西安 710072;4.南京大学 计算机科学与技术系, 江苏 南京 210023;5.中国空间技术研究院, 北京 100094
|
|
| 摘要: |
| 针对一类中断驱动的航天控制系统,给出了有界模型检验的算法.这类系统由中断处理程序和操作系统调度的任务组成.当中断发生时,对应的中断处理程序响应中断事件,并可以修改控制变量值,以便在系统任务中完成后续工作.操作系统周期性地调度任务序列处理日常事务以及中断事件的后续工作.使用了带中断标记的时间自动机对中断事件和任务调度事件进行建模,并使用中断向量表和中断处理程序的伪代码模型共同描述中断的处理过程.控制变量将中断处理过程和系统任务相关联,中断处理程序可以设定某个控制变量,而系统任务则通过检查该控制变量来确定是否需要进行后续处理.对于这样的形式化模型,给出了检验关键时序性质的有界模型检验算法.该算法使用深度优先的方式遍历所有长度小于等于K的可行路径,并使用SMT Z3实现了对时间约束和规约的处理. |
| 关键词: 中断驱动系统 有界模型检验 超时检测 |
| DOI：10.13328/j.cnki.jos.004790 |
| 分类号: |
| 基金项目:国家自然科学基金(91118007,61321491);国家高技术研究发展计划(863)(2012AA011205) |
|
| Bounded Model Checking Technique for Interrupt-Driven Systems |
|
ZHOU Xiao-Yu1,2, GU Bin3, ZHAO Jian-Hua1,4, YANG Meng-Fei5
|
|
1.State Key Laboratory for Novel Software Technology Nanjing University, Nanjing 210023, China;2.Institute of Software Engineering, Nanjing University, Nanjing 210093, China;3.School of Computer Science and Engineering, Northwestern Polytechnical University, Xi'an 710072, China;4.Department of Computer Science and Technology, Nanjing University, Nanjing 210023, China;5.China Academy of Space Technology, Beijing 100094, China
|
| Abstract: |
| 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. |
| Key words: interrupt-driven system bounded model checking deadline detection |
