CSP + T(ID:6812/csp008)CSP with complex event timingsfor CSP + Time "Adds expressive power to some of the sequential aspects of CSP and allows the description of complex event timings from within a single sequential process" Related languages
References: 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. |