WEKO3
アイテム
NuSMVの反例解析支援ツールの試作
https://ipsj.ixsq.nii.ac.jp/records/193866
https://ipsj.ixsq.nii.ac.jp/records/193866fd49bbcd-9111-4aec-b52d-eeed95e62335
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-WWS2019007.pdf (306.2 kB)
|
Copyright (c) 2019 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Symposium(1) | |||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 公開日 | 2019-01-17 | |||||||||||||||
| タイトル | ||||||||||||||||
| タイトル | NuSMVの反例解析支援ツールの試作 | |||||||||||||||
| タイトル | ||||||||||||||||
| 言語 | en | |||||||||||||||
| タイトル | A Prototype Tool to Aid Analysis of Counterexamples Produced by NuSMV | |||||||||||||||
| 言語 | ||||||||||||||||
| 言語 | 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 | ||||||||||||||||
| 著者名 |
大池, 勇太郎
× 大池, 勇太郎
× 小形, 真平
× 青木, 善貴
× 中川, 博之
× 岡野, 浩三
|
|||||||||||||||
| 著者名(英) |
Yutaro, Oike
× Yutaro, Oike
× Shinpei, Ogata
× Yoshitaka, Aoki
× Hiroyuki, Nakagawa
× Kozo, Okano
|
|||||||||||||||
| 論文抄録 | ||||||||||||||||
| 内容記述タイプ | Other | |||||||||||||||
| 内容記述 | モデル検査において，複雑 ・ 大規模なシステムのモデルの反例を手動で解析することは，非常に時間がかかる．NuSMV では反例情報として，状態遷移により変化した変数の値が各状態ごとに出力されるだけであるため，変数の多い大規模なモデルでは開発者による解析が困難になりやすい．本稿では NuSMV から得られた反例解析の効率を向上させるため，反例を自動で変数ごとの遷移を確認できるように, 表形式に整理し保存する．また，反例をグラフとして可視化するためのツールを試作し，セマフォのモデルに対して実行し，誤りのある箇所を絞り込むことに有効な見込みを得られた． | |||||||||||||||
| 書誌情報 |
ウィンターワークショップ2019・イン・福島飯坂 論文集 巻 2019, p. 13-14, 発行日 2019-01-17 |
|||||||||||||||
| 出版者 | ||||||||||||||||
| 言語 | ja | |||||||||||||||
| 出版者 | 情報処理学会 | |||||||||||||||
