The need for new forms of mathematics to express software engineering concepts and entities has been widely recognized. Real-time process algebra (RTPA) is a denotational mathematical structure and a system modeling methodology for describing the architectures and behaviors of real-time and nonrealtime software systems. This article presents an operational semantics of RTPA, which explains how syntactic constructs in RTPA can be reduced to values on an abstract reduction machine. The operational semantics of RTPA provides a comprehensive paradigm of formal semantics that establishes an entire set of operational semantic rules of software. RTPA has been successfully applied in real-world system modeling and code generation for software systems, human cognitive processes, and intelligent systems.
TopIntroduction
Real-time process algebra (RTPA) is a denotational mathematical structure and a system modeling methodology for describing the architectures and behaviors of real-time and nonreal-time software systems (Wang, 2002, 2003, 2006a, 2006b, 2007a, 2008a-c). RTPA provides a coherent notation system and a rigorous mathematical structure for modeling software and intelligent systems. RTPA can be used to describe both logical and physical models of systems, where logic views of the architecture of a software system and its operational platform can be described using the same set of notations. When the system architecture is formally modelled, the static and dynamic behaviors that perform on the system architectural model, can be specified by a three-level refinement scheme at the system, class, and object levels in a top-down approach. Although CSP (Hoare, 1978, 1985), the timed CSP (Boucher & Gerth, 1987; Fecher, 2001; Nicollin & Sifakis, 1991), and other process algebra (Baeten & Bergstra, 1991; Milner, 1980, 1989) treated a computational operation as a process, RTPA distinguishes the concepts of meta processes from complex and derived processes by algebraic process operations.
Definition 1: Operational semantics of a programming language or a formal notation system is the semantics perceived on a given virtual machine, known as the abstract reduction machine, that denotes the semantics of programs or formal system models by its equivalent behaviors implemented on the reduction machine.
One way to define an operational semantics for a language or formal notation system is to provide a state transition system for the language, which allows a formal analysis of the language and permits the study of relations between programs (Jones, 2003; Plotkin, 1981; Schneider, 1995). An alternative way is to describe the operations of the language on an abstract deductive machine whose operations are precisely defined (Sloneger & Barry, 1995; Winskel, 1993). In operational semantics, the reduction machine is a virtual machine that is adopted for reducing a given program to values of identifiers modeled in the machine by a finite set of permissible operations (Louden, 1993; McDermid, 1995).
This article presents a comprehensive operational semantics for RTPA on the basis of an abstract reduction machine, which defines inference rules for repetitively reducing a system model in RTPA into the computational values of identifiers and data objects. The abstract syntaxes of RTPA are introduced, and the reduction machine of RTPA is elaborated. Based on these, the operational semantics of 17 RTPA meta processes and 17 RTPA process relations are systematically developed. A comparative analysis of a set of comprehensive formal semantics for RTPA may be referred to (Wang, 2007a). The deductive semantics of RTPA is presented in Wang (2006a, 2008b). The denotational semantics of RTPA is reported in Tan and Wang (2008).