Verification model translation method toward behavior model for CAST

Takahiro Ando, Bo Wang, Hisazumi Kenji, 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

Model checking
diagrams
Accidents
accidents
communication
Communication
costs
Costs
interactions

All Science Journal Classification (ASJC) codes

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

Cite this

Ando, T., Wang, B., Kenji, H., 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

Verification model translation method toward behavior model for CAST. / Ando, Takahiro; Wang, Bo; Kenji, Hisazumi; Kong, Weiqiang; Fukuda, Akira; Michiura, Yasutaka; Sakemi, Keita; Matsumoto, Michihiro.

Proceedings - 2018 5th International Conference on Dependable Systems and Their Applications, DSA 2018. Institute of Electrical and Electronics Engineers Inc., 2018. p. 142-147 8563204 (Proceedings - 2018 5th International Conference on Dependable Systems and Their Applications, DSA 2018).

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

Ando, T, Wang, B, Kenji, H, Kong, W, Fukuda, A, Michiura, Y, Sakemi, K & 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., 8563204, Proceedings - 2018 5th International Conference on Dependable Systems and Their Applications, DSA 2018, Institute of Electrical and Electronics Engineers Inc., pp. 142-147, 5th International Conference on Dependable Systems and Their Applications, DSA 2018, Dalian, China, 9/22/18. https://doi.org/10.1109/DSA.2018.00032
Ando T, Wang B, Kenji H, Kong W, Fukuda A, Michiura Y et al. Verification model translation method toward behavior model for CAST. In Proceedings - 2018 5th International Conference on Dependable Systems and Their Applications, DSA 2018. Institute of Electrical and Electronics Engineers Inc. 2018. p. 142-147. 8563204. (Proceedings - 2018 5th International Conference on Dependable Systems and Their Applications, DSA 2018). https://doi.org/10.1109/DSA.2018.00032
Ando, Takahiro ; Wang, Bo ; Kenji, Hisazumi ; Kong, Weiqiang ; Fukuda, Akira ; Michiura, Yasutaka ; Sakemi, Keita ; Matsumoto, Michihiro. / Verification model translation method toward behavior model for CAST. Proceedings - 2018 5th International Conference on Dependable Systems and Their Applications, DSA 2018. Institute of Electrical and Electronics Engineers Inc., 2018. pp. 142-147 (Proceedings - 2018 5th International Conference on Dependable Systems and Their Applications, DSA 2018).
@inproceedings{87147d28558b4a6dbb016e63a07e8ce1,
title = "Verification model translation method toward behavior model for CAST",
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.",
author = "Takahiro Ando and Bo Wang and Hisazumi Kenji and Weiqiang Kong and Akira Fukuda and Yasutaka Michiura and Keita Sakemi and Michihiro Matsumoto",
year = "2018",
month = "12",
day = "5",
doi = "10.1109/DSA.2018.00032",
language = "English",
series = "Proceedings - 2018 5th International Conference on Dependable Systems and Their Applications, DSA 2018",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "142--147",
booktitle = "Proceedings - 2018 5th International Conference on Dependable Systems and Their Applications, DSA 2018",
address = "United States",

}

TY - GEN

T1 - Verification model translation method toward behavior model for CAST

AU - Ando, Takahiro

AU - Wang, Bo

AU - Kenji, Hisazumi

AU - Kong, Weiqiang

AU - Fukuda, Akira

AU - Michiura, Yasutaka

AU - Sakemi, Keita

AU - Matsumoto, Michihiro

PY - 2018/12/5

Y1 - 2018/12/5

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85060696930&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85060696930&partnerID=8YFLogxK

U2 - 10.1109/DSA.2018.00032

DO - 10.1109/DSA.2018.00032

M3 - Conference contribution

AN - SCOPUS:85060696930

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

SP - 142

EP - 147

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

PB - Institute of Electrical and Electronics Engineers Inc.

ER -