Timed CSP(ID:6808/tim001)Extension of CSP to include timing constructsfor Timed Communicating Sequential Processes Extension of CSP to include timing constructs Related languages
References: This monograph contains two papers on Timed CSP. The first of these introduces the language of Timed CSP, aimed at those familiar with Hoare's book on CSP. The second presents a complete proof system for reasoning about the most useful class of Timed CSP specifications: behavioural specifications on timed failures. Together, these two papers provide a foundation for the specification and design of real-time concurrent systems using Timed CSP. External link: online copy Introduction There has been considerable effort recently in extending Hoare?s [1985] CSP and Milner?s [1980; 1989] CCS to allow formal reasoning about real-time systems. Examples of such systems are commonly found in communication protocols where the response to a message is required before the message becomes obsolete, or where message outputs need to be spaced so as to avoid overflow conditions at the receiving end. We propose some informal time (and probability) extensions to CSP in Zic [1986] where a special DELAY process allowed temporal separation between any two successive events. At approximately the same time, Reed and Roscoe [1986] introduced a similar special process WMZ? into CSP and provided a complete semantics based on timed failures for their Timed CSP language. Gerber et al. [1988] introduced a timed-action operatio~ (effectively, a time was associated with each prefix operation) to separate adjacent events temporally into their extended CSP. They also provided a Timed-Acceptance semantics for the language. Quemada and Fernandez [1987] proposed an extension to the LOTOS specification language [Brinksma 1987] by associating an enabling interval with each event. This time interval represents the time over which a process may engage the event. There are difficulties in describing and specifying complex system timings using this type of construction, where an event timing is defined solely by its immediate predecessor. Complex timings and the ability to define the future behavior of a system will inevitably rely on a set with more than one element of preceding events in the process? execution. Furthermore, these events may have occurred a long time in the past execution of the process. To address these problems, Zic [ 1991] proposed an extended CSP called CSP + T that associated an enabling interval with each event and allowed this interval to be expressed as a function of one or more marker events. It will be seen that the CSP + T approach differs fundamentally from the Timed CSP solutions. Timed CSP captures timing constraints by the parallel composition of a set of processes, each of which describes a specific timing constraint. These timing constraints are viewed as representing timed refinements of the system and facilitate the specification and proof of system timings. However, the algebraic manipulation of complex timing requirements from a parallel composed system into, essentially, a simpler sequential system may, in some cases, be impossible without extending Timed CSP to allow a way of recording and using the time at which specific events occurred in the system?s execution. On the other hand, CSP + T describes timing constraints of sequential processes in sequential terms as much as possible, reducing the need for adding any parallel processes to express timing constraints. Furthermore, the additional expressive power of the language now allows some complex parallel systems to be rendered as sequential processes, something that could not be done with only interevent timing constructs such as DELAY. This article is organized as follows. First, we present the problem, which is the modeling of a store-and-forward communication system with a specific quality of service requirements. This is done by representing the system as a finite-length buffer with appropriate input, transit, and output timing requirements. Second, we present the CSP extensions for CSP + T. Third, we develop a solution in terms of existing Timed CSP algebra. Finally, we present an alternative solution using the CSP + T notation. DOI Extract: Introduction Introduction The language described in this paper is very di erent to the original CSP notation of [Hoa78]. The language and models of Timed CSP have undergone a gradual evolution, from [ReR86] to [DaS92]. The forthcoming text on CSP and Timed CSP should provide for some degree of standardisation; until then, we offer this document as a guide to the current state of Timed CSP. The paper begins with a description of the language of Timed CSP, and the model of computation. In Section 3, we show how timed and untimed models for the language may be used to capture requirements and establish results about program behaviour. Two complete compositional proof systems are presented: for the untimed traces, and timed failures models. In Section 4, a notion of timed refinement is introduced, relating timed programs to untimed specifications. In Section 5, we provide a complete list of the changes made to the language of Timed CSP since [ReR86]. The mathematical foundations provided by [ReR87, Ree88] are suciently robust to support such improvements without the need to restructure the semantic models. These changes have been motivated by case studies and applications, rather than by any need to modify the original intuition. The paper ends with a brief discussion of other timed process algebras. Extract: The language of Timed CSP The language of Timed CSP A program in Timed CSP is a term in the abstract syntax, a language construct such as a ! Stop. An observation of a program is a record of observable behaviour during an execution. A model is a denotational semantic model for the language, in which each program is identified with a set of observations. The di erent models are named according to the type of observations made: in the timed traces model, observations are sequences of timed events. A process is an element of a semantic model: a set of observations which defines a pattern of behaviour. We find it useful to maintain a distinction between programs and processes, although it is not strictly necessary|valid programs are identified with elements of the semantic model. The construction of the semantic models is influenced by the properties of our model of computation: these include This model of computation is consistent with that employed in [Hoa85]. pdf Introduction An operational semantics for a computer programming language defines the meaning of programs written in that language in terms of how a machine is intended to execute them step by step. It therefore offers a direct intuition of how program constructs are intended to behave, in contrast with denotational approaches, which often abstract away from such considerations, and with algebraic approaches, where operators are defined in terms of the algebraic laws they satisfy. In providing an operational semantics for a language which is already endowed with a denotational semantics, our intention is to provide an operational intuition for the language constructs, and hence gain some insight into the design decisions that were incorporated into the denotational definitions; in this way we may highlight those aspects of behaviour which derive from our philosophy of how programs should be executed, and expose those design decisions that have viable alternatives. Timed Communicating Sequential Processes is an extension of the CSP language of (Hoare, 1985) to include timing constructs. It first appeared in (Reed and Roscoe, 1986), and a variety of denotational semantic models have since been provided for the lan- guage (Reed and Roscoe, 1987), (Reed 1988); the report (Davies and Schneider, 1989) provides an introduction to these models. More recently the language and models have been refined to take a more abstract view of time. The alterations are chronicled in (Davies and Schneider, 1992); we will use the timed model discussed there for the pur- poses of this paper. All of these approaches define the meaning of a CSP program to be a set of possible behaviours. The nature of a behaviour differs between models, the simplest kind being simply sequences of events (untimed traces). Behaviours in the more sophisticated timed models contain times at which events are performed and refused. In order to verify that these denotational models are consistent with some intuition of how timed CSP programs should be executed, we present an operational semantics for timed CSP. We consider the execution of a timed CSP program as a sequence of timed transitions: timed communication events (drawn from the alphabet ) and timed internal events ( ). Inference rules are presented which define the transitions which a process may perform, which for composite programs are given in terms of the possible transitions of the constituents; whether the constituents may evolve over time without performing any transitions, given in terms of an evolves relation; and what the components may perform initially, given by a function init . Full abstraction will be established for the timed failures modelMTF, by extracting timed traces and timed refusals from the transition sequences of a program, and establishing that the pertinent information agrees with the semantics given directly by the denotational semantic function. This result is used to show that equivalence under may-testing is the same as equality in the timed failures model; it follows that the timed failures model is the weakest model that implies trace congruence (the largest congruence smaller than trace equivalence). This illustrates the fact that timed traces alone are not sucient to provide an adequate model for timed CSP, and that a model containing refusal information is required. pdf |