Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2504.04638 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917981103063040 |
|---|---|
| author | Gajula, Yogesh Lingala, Ravi Varma |
| author_facet | Gajula, Yogesh Lingala, Ravi Varma |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_04638 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Modeling, Translation, and Analysis of Different examples using Simulink, Stateflow, SpaceEx, and FlowStar Gajula, Yogesh Lingala, Ravi Varma Systems and Control Robotics 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. |
| title | Modeling, Translation, and Analysis of Different examples using Simulink, Stateflow, SpaceEx, and FlowStar |
| topic | Systems and Control Robotics |
| url | https://arxiv.org/abs/2504.04638 |