CLEOPATRA: Building Responsive Systems from Physically-Correct Specifications
Abstract
Predictability- the ability to foretell that an implementation will not violate a set of specified reliability and timeliness requirements is a crucial, highly desirable property of responsive embedded systems. This paper overviews a development methodology for responsive systems, which enhances predictability by eliminating potential hazards resulting from physically-unsound specifications. The backbone of our methodology is the Time-constrained Reactive Automaton (TRA) formalism, which adopts a fundamental notion of space and time that restricts expressiveness in a way that allows the specification of only reactive, spontaneous, and causal computation. Using the TRA model, unrealistic systems possessing properties such as clairvoyance, caprice, in nite capacity, or perfect timing cannot even be specified. We argue that this "ounce of prevention" at the specification level is likely to spare a lot of time and energy in the development cycle of responsive systems, not to mention the elimination of potential hazards that would have gone, otherwise, unnoticed.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 01, 1993
- Accession Number
- ADA444368
Entities
People
- Azer Bestavros
Organizations
- Boston University