中断驱动系统模型检验
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:

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


Model Checking Technique for Interrupt-Driven System
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    Abstract:

    In this paper, an approach is proposed to model and verify a class of interrupt-driven systems. An interrupt-driven system usually consists of interrupt handlers and system-scheduling tasks. When an interrupt occurs, the corresponding interrupt-handler executes in response. The operating system schedules a set of tasks to deal with routine events and certain post-processing of some interrupts. In the real-time control system, it is important that interrupts are handled within their specific deadlines, otherwise, it may cause catastrophic system failures. In order to improve the reliability of interrupt-driven systems, model checking technique is introduced to the design and development process. Through analyzing numerous systems, the major system elements (including system scheduling tasks, interrupts and their handlers) and their parameters relevant to time-related failures are identified. When these parameters are specified by system designer in the design process, formal models can be constructed by the modeling method in this paper: The interrupt source is modeled as timed automata. The execution processes of interrupt handlers are modeled by the interrupt vector and the CPU process stack. A model-checking algorithm is provided to check the above formal model whether interrupt handlers can be executed within their response deadlines. Moreover, a variation of this algorithm is developed to check properties of the integrity of shared resources and the atomicity of subprograms.

    参考文献
    相似文献
    引证文献
引用本文

周筱羽,顾斌,赵建华,杨孟飞,李宣东.中断驱动系统模型检验.软件学报,2015,26(9):2212-2230

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2013-10-16
  • 最后修改日期:2014-04-18
  • 录用日期:
  • 在线发布日期: 2015-09-14
  • 出版日期:
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号