Timed acceptances: An algebra of time dependent computing

A process whose correctness depends on its adherence to explicit timing constraints is a time dependent process. Applications requiring such processes are found in automated manufacturing and control systems, computer networks and aeronautic systems. Unfortunately, there has been little theoretical interest in the issues that arise when the explicit temporal performance of a process is considered part of its behavior. Timed Acceptances provides a framework in which time dependent processes can be formally described and analysed. The timed acceptances model supports an explicit representation of time, accounts for nondeterminism, is expressive and forms the basis of a proof system for reasoning about time dependent processes. It consists of a partially ordered domain of time dependent processes and a set of operators. A time dependent process is characterized by its possible execution sequences. An execution sequence consists of a timed trace and the nondeterministic choices the process may make after executing the trace. The temporal behavior of the process is represented by associating an occurrence time with each event it executes. The partial ordering, process containment, represents the notion of one process being less deterministic than another. It can be used to show that a process satisfies its specification. The operators of the algebra are like the CSP operators and are defined with respect to time. As we show, they form a natural and expressive syntax for representing time dependent processes. Using these operators, one can express delays, bounded timing constraints, timeouts, periodic processes, decisions made on the occurrence time of an event and process interaction. The operators enjoy a variety of mathematical properties. Together with process containment, these properties form a powerful proof system for analyzing time dependent processes. We have shown the use of Timed Acceptances in modelling and analyzing various time dependent processes. In particular, it has been applied to the analysis of a timed communication protocol, Bit Oriented Signalling, currently being used at AT&T\u27s Digital Multiplexed Interface