| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2019-11-08 11:30 不具合原因分析支援のためのNuSMV反例解析手法の試案 ○大池勇太郎・小形真平（信州大）・青木善貴（日本ユニシス）・中川博之（阪大）・小林一樹・岡野浩三（信州大）  KBSE2019-24 SC2019-21 |
|
| 抄録 | （和） | 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 / / / / | |
| 文献情報 | 信学技報, vol. 119, no. 274, KBSE2019-24, pp. 7-12, 2019年11月. | |
| 資料番号 | KBSE2019-24 | |
| 発行日 | 2019-11-01 (KBSE, SC) | |
| ISSN | Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | KBSE2019-24 SC2019-21 |
|
| 研究会情報 | |
| 研究会 | KBSE SC |
| 開催期間 | 2019-11-08 - 2019-11-09 |
| 開催地（和） | 信州大学 |
| 開催地（英） | Shinshu University |
| テーマ（和） | 「ソフトウェア／サービスとAI」および一般 |
| テーマ（英） | |
| 講演論文情報の詳細 | |
| 申込み研究会 | KBSE |
| 会議コード | 2019-11-KBSE-SC |
| 本文の言語 | 日本語 |
| タイトル（和） | 不具合原因分析支援のためのNuSMV反例解析手法の試案 |
| サブタイトル（和） | |
| タイトル（英） | A Method to Analyze NuSMV Counterexamples for Defect Cause Analysis |
| サブタイトル（英） | |
| キーワード(1)（和/英） | NuSMV / NuSMV |
| キーワード(2)（和/英） | モデル検査 / model checking |
| キーワード(3)（和/英） | 反例解析 / counterexample analysis |
| キーワード(4)（和/英） | 構文解析 / syntactic analysis |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第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.) |
| 講演者 | 第1著者 |
| 発表日時 | 2019-11-08 11:30:00 |
| 発表時間 | 30分 |
| 申込先研究会 | KBSE |
| 資料番号 | KBSE2019-24, SC2019-21 |
| 巻番号（vol） | vol.119 |
| 号番号（no） | no.274(KBSE), no.275(SC) |
| ページ範囲 | pp.7-12 |
| ページ数 | 6 |
| 発行日 | 2019-11-01 (KBSE, SC) |
[研究会発表申込システムのトップページに戻る]