Formal Design Methodology for Hard-Real-Time Systems.
Abstract
The goal of this project is to investigate the fundamental scientific issues that will provide a foundation for a formal design methodology for hard-real-time systems. We think that it is fair to say that the progress made by this group parallels and indeed defines much of the direction and advance in real-time software research in the last 10 years. To bring a scientific discipline to real-time system design, we must develop formal techniques: (1) to specify the real-time behavior of systems (our contributions: RTL, RTCTL, and APTL); (2) to query and validate the desired behavior of a design (our contributions: RTL deductive system, RTCTL model checker, APTL tableau verifier); (3) to ensure that a design can indeed be implemented by proper resource allocation algorithms (our contributions: solutions to adaptive real-time task scheduling, a fast admissibility test for sporadic tasks, complexity results and algorithms for the pinwheel scheduling problem); (4) in addition, we need to demonstrate that our theory can be translated into design tools that form an integral part of a design methodology (our contributions: the Modechart suite of tools). We have obtained a number of basic results in all these areas and also expanded the horizon of real-time computing in the direction of: (a) rule-based systems (our contributions: the EQL, MRL real-time rule-based programming environment); and (b) semantics and concurrency control of real-time data (our contributions: the similarity relation and its use in real-time scheduling). (KAR) p. 4
Document Details
- Document Type
- Technical Report
- Publication Date
- May 31, 1994
- Accession Number
- ADA298843
Entities
People
- Aloysius K. Mok
Organizations
- University of Texas at Austin