| 硬实时软件建模与分析的进程代数方法 |
| |
| 引用本文： | 祝义,;黄志球,;张广泉,;周航,;肖芳雄. 硬实时软件建模与分析的进程代数方法[J]. 计算机科学与探索, 2014, 0(6): 684-693 |
| |
| 作者姓名： | 祝义, 黄志球, 张广泉, 周航, 肖芳雄 |
| |
| 作者单位： | [1]江苏师范大学计算机科学与技术学院,江苏徐州221116; [2]南京航空航天大学计算机科学与技术学院,南京210016; [3]苏州大学计算机科学与技术学院,江苏苏州215006; [4]南京航空航天大学民航学院,南京210016; [5]广西财经学院信息与统计学院,南宁530003 |
| |
| 基金项目： | The National Natural Science Foundation of China under Grant Nos.61272083,61262002，the Natural Science Foundation of Jiangsu Province of China under Grant No. BK2011281，the Natural Science Foundation of Jiangsu Normal University under Grant No.11XLR20 |
| |
| 摘 要： | 针对硬实时软件缺乏有效的系统动态行为建模机制，提出了一种用于硬实时软件建模与分析的进程代数方法。首先在时间通信顺序进程的基础上扩展硬实时语义得到硬实时通信顺序进程；然后提出时间调度算法，用于检查硬实时系统单个指令截止期的可满足性以及计算完成任务所需的最少时间；最后通过航空领域的一个实例来说明该方法如何应用于硬实时软件的建模与分析。该方法可以很大程度上提高硬实时软件执行时间计算的准确性，计算结果有助于硬实时系统截止期的量化分析和优化设计。
|
| 关 键 词： | 实时软件 硬实时 进程代数 时间通信顺序进程 模型检验 |
Method forModeling andAnalyzingHardReal-Time Software Based on ProcessAlgebra |
| |
| Affiliation: | ZHU Yi, HUANG Zhiqiu, ZHANG Guangquan, ZHOU Hang, XIAO Fangxiong (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, Nanj ing University of Aeronautics and Astronautics, Nanjing 210016, China 5. School of Information and Statistics, Guangxi University of Finance and Economics, Nanning 530003, China) |
| |
| 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. |
| |
| Keywords: | real-time software hard real-time process algebra timed communicating sequential process model checking |
| 本文献已被 维普 等数据库收录！ |
|
