@inproceedings{oai:ipsj.ixsq.nii.ac.jp:00206742,
 author = {青木, 善貴 and 小形, 真平 and 小林, 一樹 and 中川, 博之},
 book = {ソフトウェアエンジニアリングシンポジウム2020論文集},
 month = {Sep},
 note = {CPS (Cyber Physical System) では，多数の独立的に動くコンポーネントが連携し，複数の制御ループを構成してシステムを稼働している．制御ループ内のコンポーネントがうまく協調しないと，システムが想定外の振る舞いを起こし，事故につながる可能性が高い．このような事故を発見するために，先行研究において，CPS のアーキテクチャのモデリングから抽出した制御ループの安定性を，モデル検査を用いて検証する手法 [3] を提案してきた．本手法では，抽出した制御ループが停止するかどうかを検証できる時相論理式で，モデル検査を実行して得られた反例から不具合の要因を明らかにする．ただし，反例は膨大な状態遷移のトレースを出力したもので，それを解析して制御ループの振る舞いを理解する作業は煩雑であり，不具合の要因を特定するのには非常に手間がかかる．本稿では，反例を解析して理解するための煩雑な作業を軽減する目的で，制御ループの振る舞いをグラフ化する可視化手法を提案する．先行研究の事例 [3] への提案手法の適用により，同じ不具合の要因の特定ができた．},
 pages = {115--124},
 publisher = {情報処理学会},
 title = {グラフ化による制御ループに関する反例の可視化手法の提案},
 volume = {2020},
 year = {2020}
}