Verification Model Translation Method toward Behavior Model for CAST
| Autor: | Kenji Hisazumi, Michihiro Matsumoto, Akira Fukuda, Weiqiang Kong, Takahiro Ando, Yasutaka Michiura, Keita Sakemi, Bo Wang |
|---|---|
| Rok vydání: | 2018 |
| Předmět: |
Model checking
Finite-state machine Computer science Programming language Process (computing) computer.software_genre Translation (geometry) Promela Systems Modeling Language Feature (computer vision) Computer Science::Logic in Computer Science SPIN model checker computer computer.programming_language |
| Zdroj: | DSA |
| DOI: | 10.1109/dsa.2018.00032 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|