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 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. This model is illustrated by the specification, the description and the proof of a distributed bus arbiter.