A timed failures model for extended communicating processes: extended abstract

We develop a model for the real-time behaviour of an extension of communicating sequential processes, ECP: the timed failures model. ECP includes a time-out mechanism for actions that synchronize and a broadcast construct. The model maximalizes local activity in processes and allows the delay of enabled synchronization actions to be a-priori bounded. It is a direct generalization of the (non-timed) failures model: traces are generalized to time-action relations, associating actions to the times at which they occur, and failure-sets to time-failure relations, associating actions to the times at which they are refused. In addition to a-priori bounded delay of actions, the model supports nondiscrete time and concurrency of actions; it makes the semantic operators continuous and is fully abstract when actions and the times at which they take place are made observable.