電子情報通信学会 研究会発表申込システム
講演論文 詳細
技報閲覧サービス
技報オンライン
‥‥ (ESS/通ソ/エレソ/ISS)
技報アーカイブ
‥‥ (エレソ/通ソ)
 トップに戻る 前のページに戻る   [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 Print edition: ISSN 0913-5685  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.)
第7著者 氏名(和/英/ヨミ) / /
第7著者 所属(和/英) (略称: )
(略称: )
第8著者 氏名(和/英/ヨミ) / /
第8著者 所属(和/英) (略称: )
(略称: )
第9著者 氏名(和/英/ヨミ) / /
第9著者 所属(和/英) (略称: )
(略称: )
第10著者 氏名(和/英/ヨミ) / /
第10著者 所属(和/英) (略称: )
(略称: )
第11著者 氏名(和/英/ヨミ) / /
第11著者 所属(和/英) (略称: )
(略称: )
第12著者 氏名(和/英/ヨミ) / /
第12著者 所属(和/英) (略称: )
(略称: )
第13著者 氏名(和/英/ヨミ) / /
第13著者 所属(和/英) (略称: )
(略称: )
第14著者 氏名(和/英/ヨミ) / /
第14著者 所属(和/英) (略称: )
(略称: )
第15著者 氏名(和/英/ヨミ) / /
第15著者 所属(和/英) (略称: )
(略称: )
第16著者 氏名(和/英/ヨミ) / /
第16著者 所属(和/英) (略称: )
(略称: )
第17著者 氏名(和/英/ヨミ) / /
第17著者 所属(和/英) (略称: )
(略称: )
第18著者 氏名(和/英/ヨミ) / /
第18著者 所属(和/英) (略称: )
(略称: )
第19著者 氏名(和/英/ヨミ) / /
第19著者 所属(和/英) (略称: )
(略称: )
第20著者 氏名(和/英/ヨミ) / /
第20著者 所属(和/英) (略称: )
(略称: )
講演者
発表日時 2019-11-08 11:30:00 
発表時間 30 
申込先研究会 KBSE 
資料番号 IEICE-KBSE2019-24,IEICE-SC2019-21 
巻番号(vol) IEICE-119 
号番号(no) no.274(KBSE), no.275(SC) 
ページ範囲 pp.7-12 
ページ数 IEICE-6 
発行日 IEICE-KBSE-2019-11-01,IEICE-SC-2019-11-01 


[研究会発表申込システムのトップページに戻る]

[電子情報通信学会ホームページ]


IEICE / 電子情報通信学会