Automated Validation for Synchronous Reactive Embedded Systems
Creators:Rajabian Schwart, Vahid
Synchronous Programming Languages
SIGNAL Programming Language
Reactive Embedded Systems
MetadataShow full item record
Publisher:The Ohio State University
Series/Report no.:The Ohio State University. Department of Electrical and Computer Engineering Honors Theses; 2012
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.
College of Engineering Undergraduate Research Scholarship
Items in Knowledge Bank are protected by copyright, with all rights reserved, unless otherwise indicated.