Simulink Stateflowにおけるモデル検査手法の一考察

カテゴリ: 研究会(論文単位)

論文No: IIS15077

グループ名: 【D】産業応用部門 次世代産業システム研究会

発行日: 2015/09/17

タイトル(英語): Model Checking for Simulink Stateflow Models

著者名: 山田 親稔(沖縄工業高等専門学校),ミラー マイケル(ビクトリア大学)

著者名(英語): Yamada Yamada(National Institute of Technology, Okinawa College),Michael Miller(University of Victoria)

キーワード: モデル検査|ＳＰＩＮ|Ｓｉｍｕｌｉｎｋ　Ｓｔａｔｅｆｌｏｗ|非決定性動作|Model checking|SPIN|Simulink Stateflow|nondeterministic behaviors

要約(日本語): 本稿では，Simulink Stateflowモデルで記述されたシステムに，ツール連携手法を適用し，SPINモデル検査ツールを使用して検証する方法を提案する。提案手法を適用することで，Simulink Stateflowモデルでは検査することが不可能な非決定性動作モデルを，SPINツールを使用して検査することが可能である。

要約(英語): In this paper, we consider two tool chains that support using SPIN to model check systems specified as Simulink Stateflow models. We present algorithms for doing the necessary translations and present empirical results. We also show that these tools allow SPIN to be used for model checking nondeterministic Stateflow models in addition to deterministic ones.

原稿種別: 日本語

PDFファイルサイズ: 1,036 Kバイト