计算机科学与探索 ›› 2014, Vol. 8 ›› Issue (6): 684-693.DOI: 10.3778/j.issn.1673-9418.1311033

• 系统软件与软件工程 • 上一篇    下一篇

硬实时软件建模与分析的进程代数方法

祝  义1+,黄志球2,张广泉3,周  航4,肖芳雄5   

  1. 1. 江苏师范大学 计算机科学与技术学院,江苏 徐州 221116
    2. 南京航空航天大学 计算机科学与技术学院,南京 210016
    3. 苏州大学 计算机科学与技术学院,江苏 苏州 215006
    4. 南京航空航天大学 民航学院,南京 210016
    5. 广西财经学院 信息与统计学院,南宁?530003
  • 出版日期:2014-06-01 发布日期:2014-05-30

Method for Modeling and Analyzing Hard Real-Time Software Based on Process Algebra

ZHU Yi1+, HUANG Zhiqiu2, ZHANG Guangquan3, ZHOU Hang4, XIAO Fangxiong5   

  1. 1. School of Computer Science and Technology, Jiangsu Normal University, Xuzhou, Jiangsu 221116, China
    2. College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 210016, China
    3. School of Computer Science and Technology, Soochow University, Suzhou, Jiangsu 215006, China
    4. College of Civil Aviation, Nanjing University of Aeronautics and Astronautics, Nanjing 210016, China
    5. School of Information and Statistics, Guangxi?University of Finance and Economics,?Nanning 530003, China
  • Online:2014-06-01 Published:2014-05-30

摘要: 针对硬实时软件缺乏有效的系统动态行为建模机制,提出了一种用于硬实时软件建模与分析的进程代数方法。首先在时间通信顺序进程的基础上扩展硬实时语义得到硬实时通信顺序进程;然后提出时间调度算法,用于检查硬实时系统单个指令截止期的可满足性以及计算完成任务所需的最少时间;最后通过航空领域的一个实例来说明该方法如何应用于硬实时软件的建模与分析。该方法可以很大程度上提高硬实时软件执行时间计算的准确性,计算结果有助于硬实时系统截止期的量化分析和优化设计。

关键词: 实时软件, 硬实时, 进程代数, 时间通信顺序进程, 模型检验

Abstract: Since the design of hard real-time software lacks the effective method for modeling system dynamic behaviors, this paper proposes the process algebra support for modeling and analyzing hard real-time software to solve this problem. Firstly, this paper introduces the hard real-time communicating sequential process (CSP) by extending hard real-time semantics of timed CSP. Then, this paper proposes the time scheduling algorithms to check whether all behaviors of the system are satisfied within the deadlines and figure out the shortest execution time of the system. Finally, this paper gives an instance of aviation field to describe how to apply this method to model and analyze hard real-time software. This method improves the accuracy and efficiency of the execution time calculation of hard real-time software, and the calculation results can be used to quantitatively analyze and optimize the deadline of hard real-time system.

Key words: real-time software, hard real-time, process algebra, timed communicating sequential process, model checking