Modeling, Translation, and Analysis of Different examples using Simulink, Stateflow, SpaceEx, and FlowStar

要約

このレポートでは、6台の車両小隊、2つのバウンスボール、3つのタンクシステム、および連続およびハイブリッドシステムを表す4次元線形スイッチングなど、複数のベンチマークの翻訳とテストについて詳しく説明しています。
これらのベンチマークは、SpaceEx、Flow*、Hyst、Matlab-Simulink、StateFlowなどの多様な検証ツールを含む過去のインスタンスから収集されました。これらは、ハイブリッドオートマトンとしてモデル化されたさまざまなシステムをカバーし、分析と評価のための包括的なセットを提供します。
最初は、さまざまな適切なツールを使用して、4つのシステムすべてのモデルを作成しました。
その後、これらのモデルはSpaceEx形式に変換され、さまざまな検証ツールと互換性のある異なる形式に変換されました。
各システムの動的特性へのアプローチを適応させると、それぞれの検証ツールを使用して到達可能性分析を実行しました。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google