Verifying a Cruise Control System using Simulink and SpaceEx
Nikolaos Kekatos
TL;DR
This paper demonstrates a methodology for verifying a cruise control system by combining simulation in Simulink with formal reachability analysis using SpaceEx, illustrating a practical approach to control system verification.
Contribution
It presents a step-by-step process integrating simulation and formal verification tools for control system validation.
Findings
Successful verification of the cruise control system
Integration of Simulink with SpaceEx for combined analysis
Guidelines for applying formal methods to control systems
Abstract
This article aims to provide a simple step-by-step guide highlighting the steps needed to verify a control system with formal verification tools. Starting from a description of the physical system and a control objective in natural language, we design the plant and the controller, we use Simulink for simulation and we employ a reachability analysis tool, SpaceEx, for formal verification.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Model-Driven Software Engineering Techniques · Modeling and Simulation Systems