用多种工具建模并验证四类混合系统，提升系统安全性分析效率。
Modeling, Translation, and Analysis of Different examples using Simulink, Stateflow, SpaceEx, and FlowStar
- 基于不同工具构建四类混合系统模型，涵盖车辆队列与液位控制等场景。
- 将模型统一转换为SpaceEx格式，实现跨工具可达性分析。
- 适合系统验证、自动控制与形式化方法研究者参考使用。
本报告详细描述了多个基准测试的建模、转换与验证过程，包括六车车队、两球弹跳、三罐液位系统及四维线性切换系统，这些系统代表了连续与混合动态行为。数据源自过往使用SpaceEx、Flow*、HyST、MATLAB-Simulink、Stateflow等工具的案例，涵盖多种以混合自动机建模的系统，构成全面的分析与评估基准。我们首先利用适配工具为四类系统建立模型，随后将模型转换为SpaceEx格式，并进一步转译为兼容各类验证工具的格式。根据各系统动态特性调整方法，采用相应工具完成可达性分析。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。