Properties as Processes: their Specification and Verification

This paper presents a novel application of an untimed process algebra formalism to a class of timing-critical verification problems usually modelled with either timed automata or timed process algebra. We show that a formalism based on interacting automata can model system components, behavioural constraints and properties requiring proof without elaborating the underlying process-algebraic formalism to include explicit timing constructs; and that properties can be verified without introducing temporal logic, model-checking, or renement relation checking. We demonstrate this technique in detail by application to the Fischer mutual-exclusion protocol, an archetypal example of a system that depends of timing constraints to operate correctly