Evaluation of the Benefits and Limitations of Verification Activities in Developing a Critical System using Model-Based Development

University of Minnesota M.S.E.E. thesis. 2018. Major: Electrical Engineering. Advisors: David Lilja, Mats Heimdahl. 1 computer file (PDF); 74 pages.In developing safety-critical cyber-physical systems, model-based development (MBD) promotes design and verification activities at the model-level, which is an abstract description of the behavior of the software to be implemented. MBD tool suites such as MATLAB's Simulink and Stateflow implements the principles of MBD so that system developers can easily incorporate various verification and validation activities such as modeling, simulation, testing, and even formal verification. Among all activities involved in MBD, simulation and model-level testing are widely adopted to identify bugs in the early phase of the model development. Formal verification of the design model, on the other hand, is often considered difficult or impractical so it is less widely adopted in the practice. This report investigates the practicality, limitations, and benefits of adopting various model-based V\&V activities in developing a safety-critical cyber-physical system. We have developed a rocket-launch control system in cooperation with a local rocketry club following MBD principles. More specifically, we developed a Simulink model, performed model-level simulation, testing, and model-level property verification of three safety properties. In each phase of the development, we demonstrate that each activity can be easily incorporated into the development process. The verification result of the Simulink Design Verifier shows that our safety properties of concern hold, with which we could gain confidence in the correctness of the model. This report will help people who design a critical system using MBD to chose the verification techniques that they need