Simulink・Stateflow・SpaceEx・FlowStarを用いた複数ベンチマークのモデリング・変換・解析
Modeling, Translation, and Analysis of Different examples using Simulink, Stateflow, SpaceEx, and FlowStar
6台車両プラトーンや2つの跳ねる球などの連続・ハイブリッドシステムのベンチマークを各種ツールでモデル化し、SpaceEx形式を介して変換して到達可能性解析を行った。
著者: Yogesh Gajula, Ravi Varma Lingala
分類: eess.SY, cs.RO, cs.SY
原文アブストラクト
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.