Evaluation of the Benefits and Limitations of Verification Activities in Developing a Critical System using Model-Based Development
2018-09
Loading...
View/Download File
Persistent link to this item
Statistics
View StatisticsJournal Title
Journal ISSN
Volume Title
Title
Evaluation of the Benefits and Limitations of Verification Activities in Developing a Critical System using Model-Based Development
Authors
Published Date
2018-09
Publisher
Type
Thesis or Dissertation
Abstract
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.
Description
University of Minnesota M.S.E.E. thesis. 2018. Major: Electrical Engineering. Advisors: David Lilja, Mats Heimdahl. 1 computer file (PDF); 74 pages.
Related to
Replaces
License
Series/Report Number
Funding information
Isbn identifier
Doi identifier
Previously Published Citation
Suggested citation
Lee, Young Sub. (2018). Evaluation of the Benefits and Limitations of Verification Activities in Developing a Critical System using Model-Based Development. Retrieved from the University Digital Conservancy, https://hdl.handle.net/11299/200995.
Content distributed via the University Digital Conservancy may be subject to additional license and use restrictions applied by the depositor. By using these files, users agree to the Terms of Use. Materials in the UDC may contain content that is disturbing and/or harmful. For more information, please see our statement on harmful content in digital repositories.