Deriving real-time action systems with multiple time bands using algebraic reasoning

• An interval-based logic for deriving action systems via algebraic reasoning is developed.
• Temporal operators are given an algebraic semantics, avoiding the need for a separate temporal logic semantic layer.
• True concurrency between an action system and its environment is addressed.
• Compositional methods for reasoning over multiple time bands and sampling is developed.
• A controller for a two-pump, two-tank system, taking into account various real-world timing constraints is derived.

The verify-while-develop paradigm allows one to incrementally develop programs from their specifications using a series of calculations against the remaining proof obligations. This paper presents a derivation method for real-time systems with realistic constraints on their behaviour. We develop a high-level interval-based logic that provides flexibility in an implementation, yet allows algebraic reasoning over multiple granularities and sampling multiple sensors with delay. The semantics of an action system is given in terms of interval predicates and algebraic operators to unify the logics for an action system and its properties, which in turn simplifies the calculations and derivations.