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

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