RTPA: a new approach to real-time system specification

The specification of real-time software systems is a 3D problem known as system architectures, time and event manipulation, and dynamic memory allocation. A real-time system consists of two types of component, architectural and operational. The former were often overlooked in real-time software system design, particularly when adopting a formal approach. Real-time process algebra (RTPA) is a set of new mathematical notations for formally describing system architectures, and static and dynamic behaviors. This paper describes a new approach to the specification and refinement of real-time systems by using RTPA. First, the RTPA meta-processes, algebraic relations, and system architectural notations are introduced. The RTPA system specification method and refinement scheme for real-time system are then described. The expressive power of RTPA on formal specification of software system architectures as well as behaviors is demonstrated by examples. Applications of RTPA in a number of case studies show that the extremely small set of formal notations of RTPA is sufficient for modeling and specifying architectures of real-time systems, as well as their static and dynamic behaviors.