A Denotational Semantics of Real-Time Process Algebra (RTPA)

A Denotational Semantics of Real-Time Process Algebra (RTPA)

Yingxu Wang, Xinming Tan
Copyright: © 2010 |Pages: 18
DOI: 10.4018/978-1-60566-902-1.ch011
OnDemand:
(Individual Chapters)
Available
$37.50
Current Special Offers
No Current Special Offers
TOTAL SAVINGS: $37.50

Abstract

Real-time process algebra (RTPA) is a form of denotational mathematics for dealing with fundamental system behaviors such as timing, interrupt, concurrency, and event/time/interrupt-driven system dispatching. Because some key RTPA processes cannot be described adequately in conventional denotational semantic paradigms, a new framework for modeling time and processes is sought in order to represent RTPA in denotational semantics. Within this framework, time is modeled by the elapse of process execution. The process environment encompasses states of all variables represented as mathematical maps, which project variables to their corresponding values. Duration is introduced as a pair of time intervals and the environment to represent the changes of the process environment during a time interval. Temporal ordered durations and operations on them are used to denote process executions. On the basis of these means, a comprehensive set of denotational semantics for RTPA are systematically developed and formally expressed.
Chapter Preview
Top

The Activity Duration Calculus

The activity duration calculus (ADC) is developed to describe system behaviors over time where each activity happens in a timely order and will last for a period of time or an interval. At any specific time moment, the state of the system is represented by the values of its variables at the moment (Wang, 2006a, 2008b). The time sequence of the instantaneous moments expresses the behaviors of a system. ADC uses a semantic environment, which is a map from variables to values, to record an instantaneous system state (Wang, 2006a, 2008b). It uses a duration adopted as a 2-tuple of an interval and an environment to represent a system state for a given period of time. A temporal ordered duration sequence is therefore a semantics model of system behaviors.

Variables and Values

ADC uses variables with a universal type by default. When different types of variables, such as integer, real, and Boolean, are needed, it can be considered that the various variables are in the form of set sum (Winskel, 1993), as used in the denotational semantics of RTPA.

978-1-60566-902-1.ch011.m01 - The set of all variables. (1)978-1-60566-902-1.ch011.m02 - Domain of all possible values. (2)

When multiple variables are modeled, a subscript will be used, such as x1, …, xn, xi ∈ 978-1-60566-902-1.ch011.m03. So do the values vi ∈ 978-1-60566-902-1.ch011.m04.

Complete Chapter List

Search this Book:
Reset