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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish
Title of host publicationProceedings - 2018 5th International Conference on Dependable Systems and Their Applications, DSA 2018
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages142-147
Number of pages6
ISBN (Electronic)9781538692660
DOIs
Publication statusPublished - Dec 5 2018
Event5th International Conference on Dependable Systems and Their Applications, DSA 2018 - Dalian, China
Duration: Sep 22 2018Sep 23 2018

Publication series

NameProceedings - 2018 5th International Conference on Dependable Systems and Their Applications, DSA 2018

Other

Other5th International Conference on Dependable Systems and Their Applications, DSA 2018
CountryChina
CityDalian
Period9/22/189/23/18

    Fingerprint

All Science Journal Classification (ASJC) codes

  • Computer Science Applications
  • Safety, Risk, Reliability and Quality
  • Instrumentation

Cite this

Ando, T., Wang, B., Hisazumi, K., Kong, W., Fukuda, A., Michiura, Y., ... Matsumoto, M. (2018). Verification model translation method toward behavior model for CAST. In Proceedings - 2018 5th International Conference on Dependable Systems and Their Applications, DSA 2018 (pp. 142-147). [8563204] (Proceedings - 2018 5th International Conference on Dependable Systems and Their Applications, DSA 2018). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/DSA.2018.00032