Verifying a Cruise Control System using Simulink and SpaceEx

2020/12/31 by Nikolaos Kekatos, Kekatos, Nikolaos
Computer Science · #Formal Methods in Verification #Model-Driven Software Engineering Techniques #Modeling and Simulation Systems

paper · pdf · doi:10.48550/arxiv.2101.00102

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.

Related

• A Methodology for Developing a Verifiable Aircraft Engine Controller from Formal Requirements
• A graphical environment to express the semantics of control systems
• Evaluating Model Checking Approaches to Verify Stability of Control Systems in Simulink
• Verifying the Safety of a Flight-Critical System
• Modeling, Translation, and Analysis of Different examples using Simulink, Stateflow, SpaceEx, and FlowStar