Title: Towards Physically-Correct Specifications of Embedded Real-Time Systems
Author: Azer Bestavros, Boston University
Date: May 1994

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   a  formalism that restricts
expressiveness    in  a way  that   allows the  specification  of only
reactive,  spontaneous, and  causal computation.   Unrealistic systems
(possessing  properties   such  as  clairvoyance,    caprice, infinite
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.