WEKO3
アイテム
モデル検査における複雑な検査式に対する反例解析手法の提案
https://ipsj.ixsq.nii.ac.jp/records/206732
https://ipsj.ixsq.nii.ac.jp/records/206732418b9a8e-d80f-4c56-bb9b-dc9e2757a195
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-SES2020009.pdf (2.2 MB)
|
Copyright (c) 2020 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Symposium(1) | |||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 公開日 | 2020-09-03 | |||||||||||||||||
| タイトル | ||||||||||||||||||
| タイトル | モデル検査における複雑な検査式に対する反例解析手法の提案 | |||||||||||||||||
| タイトル | ||||||||||||||||||
| 言語 | en | |||||||||||||||||
| タイトル | A Method to Analyze Counterexample for Complex Specification in Model Checking | |||||||||||||||||
| 言語 | ||||||||||||||||||
| 言語 | jpn | |||||||||||||||||
| キーワード | ||||||||||||||||||
| 主題Scheme | Other | |||||||||||||||||
| 主題 | モデル検査 | |||||||||||||||||
| 資源タイプ | ||||||||||||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_5794 | |||||||||||||||||
| 資源タイプ | conference paper | |||||||||||||||||
| 著者所属 | ||||||||||||||||||
| 信州大学 | ||||||||||||||||||
| 著者所属 | ||||||||||||||||||
| 信州大学 | ||||||||||||||||||
| 著者所属 | ||||||||||||||||||
| 日本ユニシス株式会社 | ||||||||||||||||||
| 著者所属 | ||||||||||||||||||
| 大阪大学 | ||||||||||||||||||
| 著者所属 | ||||||||||||||||||
| 信州大学 | ||||||||||||||||||
| 著者所属 | ||||||||||||||||||
| 信州大学 | ||||||||||||||||||
| 著者所属(英) | ||||||||||||||||||
| en | ||||||||||||||||||
| Shinshu University | ||||||||||||||||||
| 著者所属(英) | ||||||||||||||||||
| en | ||||||||||||||||||
| Shinshu University | ||||||||||||||||||
| 著者所属(英) | ||||||||||||||||||
| en | ||||||||||||||||||
| Nihon Unisys, Ltd. | ||||||||||||||||||
| 著者所属(英) | ||||||||||||||||||
| en | ||||||||||||||||||
| Osaka University | ||||||||||||||||||
| 著者所属(英) | ||||||||||||||||||
| en | ||||||||||||||||||
| Shinshu University | ||||||||||||||||||
| 著者所属(英) | ||||||||||||||||||
| en | ||||||||||||||||||
| Shinshu University | ||||||||||||||||||
| 著者名 |
大池, 勇太郎
× 大池, 勇太郎
× 小形, 真平
× 青木, 善貴
× 中川, 博之
× 小林, 一樹
× 岡野, 浩三
|
|||||||||||||||||
| 論文抄録 | ||||||||||||||||||
| 内容記述タイプ | Other | |||||||||||||||||
| 内容記述 | NuSMV によるモデル検査では，多数の部分式に分解できる長大な検査式に対して，大規模な反例が出力された場合，反例で満たされていない部分式（以下，不満足な部分式）を手動で識別することに時間がかかる問題がある．そこで本研究では，不満足な部分式を自動識別するための解析手法と支援ツールを提案する．提案手法では，構文解析により複雑な検査式を部分式に分解し，部分式が反例で満たされるかどうかを調べて不満足な部分式を識別する．提案手法の有効性評価のために交通制御システムのモデルに適用した結果，不満足な部分式を正しく識別できたため，提案手法は有効である見込みを得た． | |||||||||||||||||
| 書誌情報 |
ソフトウェアエンジニアリングシンポジウム2020論文集 巻 2020, p. 23-31, 発行日 2020-09-03 |
|||||||||||||||||
| 出版者 | ||||||||||||||||||
| 言語 | ja | |||||||||||||||||
| 出版者 | 情報処理学会 | |||||||||||||||||
