Real time in a TLA-based theory of reactive systems

Abstract

A practical theory for operational specification of reactive systems is described. Reasoning on temporal properties is made possible by it already at high levels of abstraction, and rigorous refinement towards implementation is supported. The paper discusses how the underlying logic, execution model, and refinement methods fit together, and how object-orientation, distribution, and real time are supported. A closer look is taken on the specification of real-time properties by illustrating the approach by a logically layered specification of simple mobile robot control software.