Verification model translation method toward behavior model for CAST

Takahiro Ando, Bo Wang, Kenji Hisazumi, Weiqiang Kong, Akira Fukuda, Yasutaka Michiura, Keita Sakemi, Michihiro Matsumoto

研究成果: Conference contribution

抄録

In this study, we think the feature of exhaustively verifying the process model of model checking is effective for Causal Analysis based on Systems-Theoretic Accident Model and Process (CAST), and discuss the introduction of the model checking technology in CAST. In particular, we propose a verification model translation method for behavior models which are created in the CAST process. Because the interaction between multiple components is important in CAST, our translation method translates plural related SysML state machine diagrams describing the components behavior to one verification model. The verification model is described in Promela language for SPIN model checker. In order to suppress the cost of the model checking, our translation method has the feature that the verification model to be generated is simple. Furthermore, it has the feature that the correspondence between the related behavior models and the verification model is understandable, and the efficiency of the confirmation of verification result can be improved. In addition, since it has the feature that the communication situation between each state machine is easy to check, it is expected to be utilized for CAST. In this paper, we describe the rules to translate the related SysML state machine diagrams to a simple verification model in Promela.

本文言語English
ホスト出版物のタイトルProceedings - 2018 5th International Conference on Dependable Systems and Their Applications, DSA 2018
出版社Institute of Electrical and Electronics Engineers Inc.
ページ142-147
ページ数6
ISBN(電子版)9781538692660
DOI
出版ステータスPublished - 2018 12 5
外部発表はい
イベント5th International Conference on Dependable Systems and Their Applications, DSA 2018 - Dalian, China
継続期間: 2018 9 222018 9 23

出版物シリーズ

名前Proceedings - 2018 5th International Conference on Dependable Systems and Their Applications, DSA 2018

Conference

Conference5th International Conference on Dependable Systems and Their Applications, DSA 2018
国/地域China
CityDalian
Period18/9/2218/9/23

ASJC Scopus subject areas

  • コンピュータ サイエンスの応用
  • 安全性、リスク、信頼性、品質管理
  • 器械工学

フィンガープリント

「Verification model translation method toward behavior model for CAST」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル