Real-time process algebra (RTPA) is a denotational mathematical structure for denoting and manipulating system behavioral processes. RTPA is designed as a coherent algebraic system for intelligent and software system modeling, specification, refinement, and implementation. RTPA encompasses 17 metaprocesses and 17 relational process operations. RTPA can be used to describe both logical and physical models of software and intelligent systems. Logic views of system architectures and their physical platforms can be described using the same set of notations. When a system architecture is formally modeled, the static and dynamic behaviors performed on the architectural model can be specified by a three-level refinement scheme at the system, class, and object levels in a top-down approach. RTPA has been successfully applied in real-world system modeling and code generation for software systems, human cognitive processes, and intelligent systems.
TopIntroduction
The modeling and refinement of software and intelligent systems require new forms of denotational mathematics that possess enough expressive power for rigorously describing system architectures and behaviors. Real-time process algebra (RTPA) is a new denotational mathematical structure for software system modeling, specification, refinement, and implementation for both real-time and nonreal-time systems (Wang, 2002b, 2007d; Wang & King, 2000). An important finding in formal methods is that a software system can be perceived and described as the composition of a set of processes, which are constructed on the basis of algebraic operations. Theories on process algebras can be traced back to Hoare’s Communicating Sequential Processes (CSP) (Hoare, 1978, 1985) and Milner’s Calculus of Communicating Systems (CCS) (Milner, 1980). The process metaphor of software systems has evolved from concurrent processes to real-time process systems in the area of operating system research and formal methods (Boucher & Gerth, 1987; Hoare, 1978, 1985; Milner, 1980, 1989; Reed & Roscoe, 1986; Schneider, 1991).
Definition 1.A process is an abstract model of a unit of meaningful system behaviors that represents a transition procedure of the system from one state to another by changing values of the sets of inputs, outputs, and/or internal variables.
It is recognized that generic computing problems are 3-D problems, known as those of the behavior, space, and time dimensions, which require a denotational mathematical means for addressing the requirements in all dimensions, particularly the time dimension (Wang, 2002b, 2003b, 2007d). However, conventional process models are hybrid (Hoare, 1985), which do not distinguish the concepts of fundamental metaprocesses and process operations between them. The CSP notation models a major part of elementary software behaviors that may be used in system specification and description. However, it lacks many useful processes that are perceived essential in system modeling, such as addressing, memory manipulation, timing, and system dispatch. CSP models all input and output (I/O) as abstract channel operations that are not expressive enough to denote complex system interactions, particularly for those of real-time systems.
A number of timed extensions and variations of process algebra have been proposed (Baeten & Bergstra, 1991; Boucher & Gerth, 1987; Cerone, 2000; Corsetti, Montanari, & Ratto, 1991; Dierks, 2000; Fecher, 2001; Gerber, Gunter, & Lee, 1992; Jeffrey, 1992; Klusener, 1992; Nicollin & Sifakis, 1991; Reed & Roscoe, 1986; Schneider, 1991; Vereijken, 1995). It is found that the existing work on process algebra and their timed variations can be extended and refined to a new form of denotational mathematics, RTPA, based on a set of algebraic process operations and laws (Wang, 2002b, 2003b, 2006a, 2006c, 2007d, 2008a). RTPA can be used to formally and precisely describe and specify architectures and behaviors of software systems on the basis of algebraic process notations and rules.
Definition 2.A process P in RTPA is a composed component of n metastatements si and sj, 1 ≤ i < n, j = i + 1, according to certain composing relations rij, i.e.:
(1)
where rij∈ℜ
, which is a set of relational process operators of RTPA that will be formally defined in Lemma 2.