Multi-Level Specification and Verification of Real-Time Software
Abstract
A state based approach is presented 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 Multi-State (HMS) machine. With the higher levels defining requirements and the lower levels indicating methods of achieving the requirements. This leads to a considerable simplification of the specification process, can lead to reusability of specifications and is fundamentally different from the refinement approach to specification. A restricted method of verifying the consistency of multi-level 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 be derived. (KR)
Document Details
- Document Type
- Technical Report
- Publication Date
- Jul 01, 1989
- Accession Number
- ADA213227
Entities
People
- Armen Gabrielian
- Matthew K. Franklin