A functional model for describing and reasoning about time behaviour of computing systems (Q2265792)

We present a mathematical model of parallel and real time systems behaviour, suitable for problem specification, and for implementation description, analysis and proof. On one hand, this model allows a pure behavioural description mode, and on the other hand, it takes into account a metric, continuous notion of time: A system is considered as a history transformer, and the history of a variable consists of the sequence of values assigned to it, together with the sequence of times when these assignments take place. A set of tools is proposed, in order to describe such histories, and to perform proofs about them. The proposed approach is illustrated by the specification, the description and the proof of an asynchronous, distributed bus arbiter.