Logical layers in specifications with distributed objects and real time

A practical theory for incremental specification of reactive systems is des cribed, where reasoning on temporal properties is possible already at high levels of abstraction, and rigorous refinement towards implementation is su pported. The paper discusses how the underlying logic, execution model, and refinement methods fit together, how logical layering is imposed on specif ications, and how object-oriented concepts, distribution, and real time are supported. A generic pattern for periodic and aperiodic real-time events i s given in terms of abstract classes, and the approach is illustrated by a simple example of mobile robot control software.