@techreport{oai:ipsj.ixsq.nii.ac.jp:00186599,
 author = {久野, 和敏 and 上田, 賀一 and 小飼, 敬 and Kazutoshi, Kuno and Yoshikazu, Ueda and Kei, Kogai},
 issue = {9},
 month = {Mar},
 note = {モデル検査において，検査対象の状態数が膨大である場合，現実的な時間で検証できないという問題があり，実用化の課題となっている．先行研究ではこの問題を軽減するため，結合度による振舞いモデルの自動分割と部分状態遷移の生成によって，検査対象の状態数の削減に取り組んだ．しかし，この手法で生成された状態遷移は情報が部分集合化されるため，既存のモデル検査器では検証できない問題が生じた．本研究では，先行研究を用いたモデル検査において，グラフデータベース Neo4j の問い合わせと最小限の状態合成によって，既存のモデル検査器が行う検証と同等な検証を行うための手順を提案する．シミュレーション実験の結果，提案手法による検証が行えることを確認した．, 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.},
 title = {グラフデータベースを用いたモデル検査手法の提案},
 year = {2018}
}