English

Verifying a Cruise Control System using Simulink and SpaceEx

Logic in Computer Science 2021-01-05 v1 Systems and Control Systems and Control
Authors: Nikolaos Kekatos
View on arXiv ↗ PDF ↗

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.

Keywords

formal verification

Cite

@article{arxiv.2101.00102,
  title  = {Verifying a Cruise Control System using Simulink and SpaceEx},
  author = {Nikolaos Kekatos},
  journal= {arXiv preprint arXiv:2101.00102},
  year   = {2021}
}

Related papers

View all related →
Systems and Control · Computer Science
Verification of Control Systems Implemented in Simulink with Assertion Checks and Theorem Proving: A Case Study
Dejanira Araiza-Illan, Kerstin Eder, Arthur Richards
2021-04-13
Software Engineering · Computer Science
Verifying the Safety of a Flight-Critical System
Guillaume Brat, David Bushnell, Misty Davies, Dimitra Giannakopoulou +2
2015-02-10
Systems and Control · Computer Science
Formal Verification of Control Systems Properties with Theorem Proving
Dejanira Araiza-Illan, Kerstin Eder, Arthur Richards
2014-10-22
Software Engineering · Computer Science
A Methodology for Developing a Verifiable Aircraft Engine Controller from Formal Requirements
Matt Luckcuck, Marie Farrell, Oisín Sheridan, Rosemary Monahan
2021-10-19
Programming Languages · Computer Science
Formal Verification of Spacecraft Control Programs Using a Metalanguage for State Transformers
Andrey Mokhov, Georgy Lukyanov, Jakob Lechner
2018-02-07
Systems and Control · Computer Science
Evaluating Model Checking Approaches to Verify Stability of Control Systems in Simulink
Dejanira Araiza-Illan, Kerstin Eder
2015-11-03
Logic in Computer Science · Computer Science
Self-Driving Vehicle Verification Towards a Benchmark
Nima Roohi, Ramneet Kaur, James Weimer, Oleg Sokolsky +1
2018-06-26
Systems and Control · Computer Science
A graphical environment to express the semantics of control systems
Timothy Wang, Romain Jobredeaux, E. Feron
2011-08-23
Systems and Control · Electrical Eng. & Systems
Modeling Uncertainty: From Simulink to Stochastic Hybrid Automata
Pauline Blohm, Felix Schulz, Lisa Willemsen, Anne Remke +1
2025-06-18
Robotics · Computer Science
Simulation Based Control Architecture Using Webots and Simulink
Harun Kurt, Ahmet Cayir, Kadir Erkan
2025-05-06
Software Engineering · Computer Science
SCR3: towards usability of formal methods
M. Chechik
2007-05-23
Systems and Control · Electrical Eng. & Systems
Modeling, Translation, and Analysis of Different examples using Simulink, Stateflow, SpaceEx, and FlowStar
Yogesh Gajula, Ravi Varma Lingala
2025-04-10
Software Engineering · Computer Science
Formal Verification Of A Shopping Basket Application Model Using PRISM
Patrick Mukala
2023-08-02
Logic in Computer Science · Computer Science
On the Verification of a WiMax Design Using Symbolic Simulation
Salim Ismail Al-Akhras, Sofiène Tahar, Gabriela Nicolescu, Michel Langevin +1
2013-08-02
Systems and Control · Electrical Eng. & Systems
Safety-Critical Controller Verification via Sim2Real Gap Quantification
Prithvi Akella, Wyatt Ubellacker, Aaron D. Ames
2022-09-21
Systems and Control · Electrical Eng. & Systems
A Barrier-Based Scenario Approach to Verify Safety-Critical Systems
Prithvi Akella, Aaron D. Ames
2022-02-24
Artificial Intelligence · Computer Science
Learning a Safety Verifiable Adaptive Cruise Controller from Human Driving Data
Qin Lin, Sicco Verwer, John Dolan
2019-10-31
Software Engineering · Computer Science
A Formal Approach to System Integration Testing
Susanne Kandl, Martin Elshuber
2014-04-29
Logic in Computer Science · Computer Science
From Zonotopes to Proof Certificates: A Formal Pipeline for Safe Control Envelopes
Jonathan Hellwig, Lukas Schäfer, Long Qian, André Platzer +1
2026-01-28
Artificial Intelligence · Computer Science
Safety Verification of Neural Network Controlled Systems
Arthur Clavière, Eric Asselin, Christophe Garion, Claire Pagetti
2020-11-11
Logic in Computer Science · Computer Science
A Scalable Approach for Hardware Semiformal Verification
Tomas Grimm, Djones Lettnin, Michael Hübner
2018-02-12
Software Engineering · Computer Science
Framework and Methodology for Verification of a Complex Scientific Simulation Software, Flash-X
Akash Dhruv, Rajeev Jain, Jared O'Neal, Klaus Weide +1
2024-05-20
Logic in Computer Science · Computer Science
Using Formal Models, Safety Shields and Certified Control to Validate AI-Based Train Systems
Jan Gruteser, Jan Roßbach, Fabian Vu, Michael Leuschel
2024-11-22
Software Engineering · Computer Science
Evaluating Model Testing and Model Checking for Finding Requirements Violations in Simulink Models
Shiva Nejati, Khouloud Gaaloul, Claudio Menghi, Lionel C. Briand +2
2019-05-10
Optimization and Control · Mathematics
How to Evolve Safe Control Strategies
G. W. Greenwood, X. Song
2007-05-23
R2 v1 2026-06-23T21:40:29.200Z