2025/04/06 by Yogesh Gajula, Gajula, Yogesh, Ravi Varma Lingala +1
Computer Science · #FOS: Computer and information sciences #FOS: Electrical engineering #Formal Methods in Verification #Modeling and Simulation Systems #Real-Time Systems Scheduling #Robotics (cs.RO) #Systems and Control (eess.SY) #electronic engineering #information engineering
paper · pdf · doi:10.48550/arxiv.2504.04638
openalex publication_date 2025/04/06 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
This report details the translation and testing of multiple benchmarks, including the Six Vehicle Platoon, Two Bouncing Ball, Three Tank System, and Four-Dimensional Linear Switching, which represent continuous and hybrid systems. These benchmarks were gathered from past instances involving diverse verification tools such as SpaceEx, Flow*, HyST, MATLAB-Simulink, Stateflow, etc. They cover a range of systems modeled as hybrid automata, providing a comprehensive set for analysis and evaluation. Initially, we created models for all four systems using various suitable tools. Subsequently, these models were converted to the SpaceEx format and then translated into different formats compatible with various verification tools. Adapting our approach to the dynamic characteristics of each system, we performed reachability analysis using the respective verification tools.