WEKO3
アイテム
グラフ化による制御ループに関する反例の可視化手法の提案
https://ipsj.ixsq.nii.ac.jp/records/206742
https://ipsj.ixsq.nii.ac.jp/records/206742ff974568-0d45-42a8-943d-469498c96e54
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-SES2020019.pdf (2.0 MB)
|
Copyright (c) 2020 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Symposium(1) | |||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 公開日 | 2020-09-03 | |||||||||||||
| タイトル | ||||||||||||||
| タイトル | グラフ化による制御ループに関する反例の可視化手法の提案 | |||||||||||||
| タイトル | ||||||||||||||
| 言語 | en | |||||||||||||
| タイトル | Proposal of Counterexample Visualization Method for Control Loop by Graphing | |||||||||||||
| 言語 | ||||||||||||||
| 言語 | jpn | |||||||||||||
| キーワード | ||||||||||||||
| 主題Scheme | Other | |||||||||||||
| 主題 | 可視化 | |||||||||||||
| 資源タイプ | ||||||||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_5794 | |||||||||||||
| 資源タイプ | conference paper | |||||||||||||
| 著者所属 | ||||||||||||||
| 日本ユニシス株式会社 | ||||||||||||||
| 著者所属 | ||||||||||||||
| 信州大学 | ||||||||||||||
| 著者所属 | ||||||||||||||
| 信州大学 | ||||||||||||||
| 著者所属 | ||||||||||||||
| 大阪大学 | ||||||||||||||
| 著者名 |
青木, 善貴
× 青木, 善貴
× 小形, 真平
× 小林, 一樹
× 中川, 博之
|
|||||||||||||
| 論文抄録 | ||||||||||||||
| 内容記述タイプ | Other | |||||||||||||
| 内容記述 | CPS (Cyber Physical System) では，多数の独立的に動くコンポーネントが連携し，複数の制御ループを構成してシステムを稼働している．制御ループ内のコンポーネントがうまく協調しないと，システムが想定外の振る舞いを起こし，事故につながる可能性が高い．このような事故を発見するために，先行研究において，CPS のアーキテクチャのモデリングから抽出した制御ループの安定性を，モデル検査を用いて検証する手法 [3] を提案してきた．本手法では，抽出した制御ループが停止するかどうかを検証できる時相論理式で，モデル検査を実行して得られた反例から不具合の要因を明らかにする．ただし，反例は膨大な状態遷移のトレースを出力したもので，それを解析して制御ループの振る舞いを理解する作業は煩雑であり，不具合の要因を特定するのには非常に手間がかかる．本稿では，反例を解析して理解するための煩雑な作業を軽減する目的で，制御ループの振る舞いをグラフ化する可視化手法を提案する．先行研究の事例 [3] への提案手法の適用により，同じ不具合の要因の特定ができた． | |||||||||||||
| 書誌情報 |
ソフトウェアエンジニアリングシンポジウム2020論文集 巻 2020, p. 115-124, 発行日 2020-09-03 |
|||||||||||||
| 出版者 | ||||||||||||||
| 言語 | ja | |||||||||||||
| 出版者 | 情報処理学会 | |||||||||||||
