Knowledge Bank

Proper functionality is a necessity for systems used in safety-critical applications; consequently, software in these systems is often subject to rigorous validation and formal verification that aims at ensuring expected behavior. To aid in the design of these systems, several synchronous programming languages exist for describing deterministic system models suitable for formal verification and validation. Examples of such synchronous languages include SIGNAL, Lustre, MRICDF, and Esterel. Common application domains for synchronous programs include avionics, automotive control, process control, and defense systems. In many cases, rigorous formal verification of these systems is unfeasible because the methods, such as theorem proving and model checking, are too expensive. A theorem proving approach requires a great deal of user involvement and expertise, and a model checking approach may not be feasible on systems of substantial complexity due to computation constraints. This thesis presents the design, implementation, and evaluation of SAGA, a prototype tool for the automated validation of synchronous reactive embedded systems. SAGA shifts the testing effort associated with critical systems from creating individual test cases manually to reasoning about the safety and environment properties of a system. The approach SAGA takes is to generate relevant inputs to the system-under-test from a user-specified environment description, and to validate the resulting system behavior against user-specified safety properties. This overview of SAGA includes a thorough user's guide and important implementation details. Additionally, the validation process with SAGA is qualitatively assessed. The assessment is done through a case study involving the celebrated steam boiler control specification problem. Results from this case study reveal the utility of SAGA in exposing non-trivial system errors.