An ounce of prevention is worth a pound of cure. Towards physically-correct specifications of embedded real-time systems

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