Executing State-Based Specifications in a Heterogeneous Environment

Date of Submission: 
May 1, 1998
Report Number: 
Assurance that a formal software specification possesses desired properties can be achieved through manual inspections, formal verification, or simulation and testing of the specification. To achieve the high level of confidence in the correctness required in many of today's critical embedded systems, all three approaches must be used in concert. In addition, to rigorously validate an embedded software system it is necessary to carefully consider its intended operating environment; the correctness of the proposed software system cannot be determined in isolation. This paper introduces a specification environment that supports the execution and simulation of formal state-based specifications for embedded systems. The environment allows us to easily execute and dynamically evaluate a high-level specification in a heterogeneous environment. The specification can be evaluated while it interacts with (1) high-level models of the assumed environment, (2) software simulations of the environment, or (3) the sensors and actuators in the physical environment itself.