使用 Simulink、Stateflow、SpaceEx 与 FlowStar 对不同示例进行建模、翻译与分析

Yogesh Gajula; Ravi Varma Lingala

使用 Simulink、Stateflow、SpaceEx 与 FlowStar 对不同示例进行建模、翻译与分析

系统与控制 2025-04-10 v1 机器人学系统与控制

作者: Yogesh Gajula , Ravi Varma Lingala

摘要

本报告详细记录了多组基准测试的翻译与测试过程，包括六辆车队、两颗弹跳球、三储罐系统以及四维线性切换系统，这些系统分别代表连续系统和混合系统。这些基准测试来自过去涉及多种验证工具（如 SpaceEx、Flow*、HyST、MATLAB-Simulink、Stateflow 等）的实例，涵盖了由混合自动机建模的系统，提供了一套完整的分析与评估集合。首先，我们使用各自适合的工具为所有四个系统创建模型。随后，将这些模型转换为 SpaceEx 格式，再翻译为与各类验证工具兼容的不同格式。根据每个系统的动态特性，我们分别使用相应的验证工具进行可达性分析。

关键词

Simulink Stateflow SpaceEx FlowStar 混合系统可达性分析验证工具基准测试

引用

@article{arxiv.2504.04638,
  title  = {Modeling, Translation, and Analysis of Different examples using Simulink, Stateflow, SpaceEx, and FlowStar},
  author = {Yogesh Gajula and Ravi Varma Lingala},
  journal= {arXiv preprint arXiv:2504.04638},
  year   = {2025}
}

备注

6 pages, 18 Figures

使用 Simulink、Stateflow、SpaceEx 与 FlowStar 对不同示例进行建模、翻译与分析

摘要

关键词

引用

备注

相关论文