| Item type |
Symposium(1) |
| 公開日 |
2016-08-24 |
| タイトル |
|
|
タイトル |
偽反例の出力を抑制するモデル検査支援環境 |
| タイトル |
|
|
言語 |
en |
|
タイトル |
Model Checking Assistance Environment to Prevent Spurious Counterexamples |
| 言語 |
|
|
言語 |
jpn |
| キーワード |
|
|
主題Scheme |
Other |
|
主題 |
モデル検査・テスト |
| 資源タイプ |
|
|
資源タイプ識別子 |
http://purl.org/coar/resource_type/c_5794 |
|
資源タイプ |
conference paper |
| 著者所属 |
|
|
|
株式会社日立製作所 |
| 著者所属 |
|
|
|
株式会社日立製作所 |
| 著者所属 |
|
|
|
株式会社日立製作所 |
| 著者所属 |
|
|
|
株式会社日立製作所 |
| 著者所属 |
|
|
|
株式会社日立製作所 |
| 著者所属 |
|
|
|
株式会社日立製作所 |
| 著者所属 |
|
|
|
株式会社日立製作所 |
| 著者所属 |
|
|
|
株式会社日立製作所 |
| 著者所属 |
|
|
|
株式会社日立製作所 |
| 著者所属 |
|
|
|
株式会社日立製作所 |
| 著者所属 |
|
|
|
株式会社日立製作所 |
| 著者所属 |
|
|
|
株式会社日立製作所 |
| 著者所属 |
|
|
|
株式会社日立製作所 |
| 著者所属 |
|
|
|
株式会社日立製作所 |
| 著者所属(英) |
|
|
|
en |
|
|
Hitachi, Ltd. |
| 著者所属(英) |
|
|
|
en |
|
|
Hitachi, Ltd. |
| 著者所属(英) |
|
|
|
en |
|
|
Hitachi, Ltd. |
| 著者所属(英) |
|
|
|
en |
|
|
Hitachi, Ltd. |
| 著者所属(英) |
|
|
|
en |
|
|
Hitachi, Ltd. |
| 著者所属(英) |
|
|
|
en |
|
|
Hitachi, Ltd. |
| 著者所属(英) |
|
|
|
en |
|
|
Hitachi, Ltd. |
| 著者所属(英) |
|
|
|
en |
|
|
Hitachi, Ltd. |
| 著者所属(英) |
|
|
|
en |
|
|
Hitachi, Ltd. |
| 著者所属(英) |
|
|
|
en |
|
|
Hitachi, Ltd. |
| 著者所属(英) |
|
|
|
en |
|
|
Hitachi, Ltd. |
| 著者所属(英) |
|
|
|
en |
|
|
Hitachi, Ltd. |
| 著者所属(英) |
|
|
|
en |
|
|
Hitachi, Ltd. |
| 著者所属(英) |
|
|
|
en |
|
|
Hitachi, Ltd. |
| 著者名 |
佐藤, 直人
芹沢, 一
前田, 浩光
高橋, 伸明
前川, 義之
四野見, 秀明
村尾, 直哉
大島, 豊
田代, 敦
黒川, 勇
八木沢, 育哉
高田, 豊
清永, 章彦
大橋, 正己
|
| 著者名(英) |
Naoto, Sato
Kazuyoshi, Serizawa
Hiromitsu, Maeda
Nobuaki, Takahashi
Yoshiyuki, Maekawa
Hideaki, Shinomi
Naoya, Murao
Yutaka, Ohshima
Atsushi, Tashiro
Isamu, Kurokawa
Ikuya, Yagisawa
Yutaka, Takata
Akihiko, Kiyonaga
Masami, Ohashi
|
| 論文抄録 |
|
|
内容記述タイプ |
Other |
|
内容記述 |
システムの仕様不具合を網羅的に検査する手段として，モデル検査がある．モデル検査とは，仕様を有限状態機械としてモデル記述し，その状態空間をモデル検査器と呼ばれるツールで機械的に網羅検査する技術である．検査により仕様不具合が検出された場合，モデル検査器はその不具合に至るまでの実行系列を反例として出力する．上流段階の設計では，仕様の簡略化のため，システムの振る舞いを抽象化して表現する場合がある．その場合，実際のシステムの振る舞いと一致しない反例が出力される可能性がある．これは偽反例と呼ばれ，不具合解析の障害になっている．偽反例を除去するためには，仕様が実システムの振る舞いと一致するように詳細化すればよい．しかし，上記のような目的で意図的に仕様を抽象化している場合は，その目的を達成できなくなる．そこで本稿では，仕様を詳細化せずに偽反例の出力を抑制する手法を提案する．さらに，提案手法に基づく作業を，形式言語を習得していない設計者でも実施可能にするモデル検査支援環境を提案する．本支援環境は，偽反例を入力として受け付け，その偽反例が出力されないように形式言語モデルを自動変更する．また本稿では，提案手法の実現性を確認するために行った適用実験結果も示す． |
| 書誌情報 |
ソフトウェアエンジニアリングシンポジウム2016論文集
巻 2016,
p. 211-218,
発行日 2016-08-24
|
| 出版者 |
|
|
言語 |
ja |
|
出版者 |
情報処理学会 |
IPSJ-SES2016031.pdf (637.0 kB)
