Multi-level specification and verification of real-time software

The authors present a state-based approach for specification of real-time software at multiple levels of abstraction. In this approach, specification at each level is performed in terms of a hierarchical multistate (HMS) machine, with the higher levels defining requirements and the lower levels indicating methods of achieving the requirements. This approach leads to a considerable simplification of the specification process; it can lead to reusability of specifications and is fundamentally different from the refinement approach. A restricted method of verifying the consistency of multilevel specifications is also presented. By the use of this method, necessary scheduling of concurrent tasks to satisfy a complex set of logical and temporal constraints can often be derived