グラフデータベースを用いたモデル検査手法の提案

• Item type: SIG Technical Reports(1)
• 公開日: 2018-03-02
• タイトル: グラフデータベースを用いたモデル検査手法の提案
• タイトル / 言語: en
• タイトル: A Model Checking Approach Using Graph Database
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: モデル検査
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 茨城大学
• 著者所属: 茨城大学
• 著者所属: 茨城工業高等専門学校
• 著者所属(英): en
• 著者所属(英): Ibaraki University
• 著者所属(英): en
• 著者所属(英): Ibaraki University
• 著者所属(英): en
• 著者所属(英): Ibaraki National College of Technology
• 著者名: 久野, 和敏; 上田, 賀一; 小飼, 敬
• 著者名(英): Kazutoshi, Kuno; Yoshikazu, Ueda; Kei, Kogai
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: モデル検査において，検査対象の状態数が膨大である場合，現実的な時間で検証できないという問題があり，実用化の課題となっている．先行研究ではこの問題を軽減するため，結合度による振舞いモデルの自動分割と部分状態遷移の生成によって，検査対象の状態数の削減に取り組んだ．しかし，この手法で生成された状態遷移は情報が部分集合化されるため，既存のモデル検査器では検証できない問題が生じた．本研究では，先行研究を用いたモデル検査において，グラフデータベース Neo4j の問い合わせと最小限の状態合成によって，既存のモデル検査器が行う検証と同等な検証を行うための手順を提案する．シミュレーション実験の結果，提案手法による検証が行えることを確認した．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: In model checking, when the number of states of an object to be inspected is enormous, there is a problem that it can not be verified with realistic time, which is a problem of practical application In previous research, in order to alleviate this problem. we tried to reduce the number of states to be inspected by automatic segmentation of behavior model by degree of coupling and generation of partial state transition. However, since the information is subsetted in the state transition generated by this method, there is a problem that can not be verified by the existing model checker. In this study, we propose a procedure for verification equivalent to verification performed by an existing model checker with by inquiries of the graph database Neo4j and minimal state synthesis of model checking using previous research. As a result of simulation experiments, we confirmed that we can verify by the proposed method.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN10112981
• 書誌情報: 研究報告ソフトウェア工学（SE）; 巻 2018-SE-198, 号 9, p. 1-8, 発行日 2018-03-02
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 2188-8825
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会