Interval-based data refinement: A uniform approach to true concurrency in discrete and real-time systems
A method for data refinement over intervals is developed, together with a sound forward simulation rule. The framework enables reasoning about true concurrency between parallel processes. Methods for decomposing forward simulation proofs are developed. The framework may be specialised to reason about both discrete and realtime systems. Examples include a concurrent algorithm and a complex real-time pump system.
refinement true concurrency real-time systems interval-based reasoning discrete time systems