| 講演名 | 2019-11-08 不具合原因分析支援のためのNuSMV反例解析手法の試案 大池 勇太郎(信州大), 小形 真平(信州大), 青木 善貴(日本ユニシス), 中川 博之(阪大), 小林 一樹(信州大), 岡野 浩三(信州大), |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | CPS(Cyber-Physical System)のように複数のモジュールが相互作用する大規模複雑なシステムを対象としたモデル検査では，モデルに定義される多数の状態変数が一つの検査式に条件式として登場しうる．そのような検査式により長大な反例が生じたとき，どの条件式を満たさなかったのかを手動で調査することは時間がかかる問題がある．そこで本研究では，大規模複雑なモデル・検査式に対する不具合原因分析の支援を目的として，モデル検査ツールNuSMVを対象に，長大な検査式に対して反例の出力原因となった条件式を自動で解析する反例解析手法と支援ツールを提案する．本稿では，提案手法の有効性評価のために，交通管理における信号制御システムのモデルに提案手法を適用した結果を報告する． |
| 抄録(英) | Many state variables that are defined in a model may appear as conditional expressions in one specification on model checking for a large complex system like CPS(Cyber-Physical System) in which multiple modules interact with each other.When a long counterexample was generated from such a complex specification, the task to manually check which conditional expression was not satisfied takes a lot of time.Therefore, in this study, we propose a counterexample analysis method and a support tool that automatically identify the conditional expressions that are causes of NuSMV counterexamples for defect cause analysis of a large specification and models.This paper describes the results of applying the proposed method to a traffic light control system model for traffic management in order to evaluate the effectiveness of the proposed method. |
| キーワード(和) | NuSMV / モデル検査 / 反例解析 / 構文解析 |
| キーワード(英) | NuSMV / model checking / counterexample analysis / syntactic analysis |
| 資料番号 | KBSE2019-24,SC2019-21 |
| 発行日 | 2019-11-01 (KBSE, SC) |
| 研究会情報 | |
| 研究会 | KBSE / SC |
|---|---|
| 開催期間 | 2019/11/8(から2日開催) |
| 開催地（和） | 信州大学 |
| 開催地（英） | Shinshu University |
| テーマ（和） | 「ソフトウェア／サービスとAI」および一般 |
| テーマ（英） | |
| 委員長氏名（和） | 粂野 文洋(日本工大) / 中村 匡秀(神戸大) |
| 委員長氏名（英） | Fumihiro Kumeno(Nippon Inst. of Tech.) / Masahide Nakamura(Kobe Univ.) |
| 副委員長氏名（和） | 中川 博之(阪大) / 菊地 伸治(物質・材料研究機構) / 山登 庸次(NTT) |
| 副委員長氏名（英） | Hiroyuki Nakagawa(Osaka Univ.) / Shinji Kikuchi(NIMS) / Yoji Yamato(NTT) |
| 幹事氏名（和） | 高橋 竜一(茨城大) / 田辺 良則(鶴見大) / 細野 繁(東京工科大) / 木村 功作(富士通研) |
| 幹事氏名（英） | Ryuichi Takahashi(Ibaraki Univ.) / Yoshinori Tanabe(Tsurumi Univ.) / Shigeru Hosono(Tokyo Univ. of Tech.) / Kosaku Kimura(Fujitsu Lab.) |
| 幹事補佐氏名（和） | 菊地 奈穂美(OKI) / 金子 朋子(NII) |
| 幹事補佐氏名（英） | Nahomi Kikuchi(OKi) / Tomoko Kaneko(NII) |
| 講演論文情報詳細 | |
| 申込み研究会 | Technical Committee on Knowledge-Based Software Engineering / Technical Committee on Service Computing |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 不具合原因分析支援のためのNuSMV反例解析手法の試案 |
| サブタイトル（和） | |
| タイトル（英） | A Method to Analyze NuSMV Counterexamples for Defect Cause Analysis |
| サブタイトル（和） | |
| キーワード(1)（和/英） | NuSMV / NuSMV |
| キーワード(2)（和/英） | モデル検査 / model checking |
| キーワード(3)（和/英） | 反例解析 / counterexample analysis |
| キーワード(4)（和/英） | 構文解析 / syntactic analysis |
| 第 1 著者 氏名（和/英） | 大池 勇太郎 / Yutaro Ohike |
| 第 1 著者 所属（和/英） | 信州大学(略称：信州大) Shinshu University(略称：Shinshu Univ.) |
| 第 2 著者 氏名（和/英） | 小形 真平 / Shinpei Ogata |
| 第 2 著者 所属（和/英） | 信州大学(略称：信州大) Shinshu University(略称：Shinshu Univ.) |
| 第 3 著者 氏名（和/英） | 青木 善貴 / Yoshitaka Aoki |
| 第 3 著者 所属（和/英） | 日本ユニシス株式会社(略称：日本ユニシス) Nihon Unisys, Ltd.(略称：Nihon Unisys, Ltd.) |
| 第 4 著者 氏名（和/英） | 中川 博之 / Hiroyuki Nakagawa |
| 第 4 著者 所属（和/英） | 大阪大学(略称：阪大) Osaka University(略称：Osaka Univ.) |
| 第 5 著者 氏名（和/英） | 小林 一樹 / Kazuki Kobayashi |
| 第 5 著者 所属（和/英） | 信州大学(略称：信州大) Shinshu University(略称：Shinshu Univ.) |
| 第 6 著者 氏名（和/英） | 岡野 浩三 / Kozo Okano |
| 第 6 著者 所属（和/英） | 信州大学(略称：信州大) Shinshu University(略称：Shinshu Univ.) |
| 発表年月日 | 2019-11-08 |
| 資料番号 | KBSE2019-24,SC2019-21 |
| 巻番号（vol） | vol.119 |
| 号番号（no） | KBSE-274,SC-275 |
| ページ範囲 | pp.7-12(KBSE), pp.7-12(SC), |
| ページ数 | 6 |
| 発行日 | 2019-11-01 (KBSE, SC) |