2026-03-13T20:33:34Z https://ipsj.ixsq.nii.ac.jp/oai

oai:ipsj.ixsq.nii.ac.jp:00174376 2025-01-20T06:53:37Z 6164:6165:6522:8893

偽反例の出力を抑制するモデル検査支援環境 Model Checking Assistance Environment to Prevent Spurious Counterexamples 佐藤, 直人 芹沢, 一 前田, 浩光 高橋, 伸明 前川, 義之 四野見, 秀明 村尾, 直哉 大島, 豊 田代, 敦 黒川, 勇 八木沢, 育哉 高田, 豊 清永, 章彦 大橋, 正己 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 モデル検査・テスト システムの仕様不具合を網羅的に検査する手段として，モデル検査がある．モデル検査とは，仕様を有限状態機械としてモデル記述し，その状態空間をモデル検査器と呼ばれるツールで機械的に網羅検査する技術である．検査により仕様不具合が検出された場合，モデル検査器はその不具合に至るまでの実行系列を反例として出力する．上流段階の設計では，仕様の簡略化のため，システムの振る舞いを抽象化して表現する場合がある．その場合，実際のシステムの振る舞いと一致しない反例が出力される可能性がある．これは偽反例と呼ばれ，不具合解析の障害になっている．偽反例を除去するためには，仕様が実システムの振る舞いと一致するように詳細化すればよい．しかし，上記のような目的で意図的に仕様を抽象化している場合は，その目的を達成できなくなる．そこで本稿では，仕様を詳細化せずに偽反例の出力を抑制する手法を提案する．さらに，提案手法に基づく作業を，形式言語を習得していない設計者でも実施可能にするモデル検査支援環境を提案する．本支援環境は，偽反例を入力として受け付け，その偽反例が出力されないように形式言語モデルを自動変更する．また本稿では，提案手法の実現性を確認するために行った適用実験結果も示す． 情報処理学会 2016-08-24 jpn conference paper https://ipsj.ixsq.nii.ac.jp/records/174376 ソフトウェアエンジニアリングシンポジウム2016論文集 2016 211 218 https://ipsj.ixsq.nii.ac.jp/record/174376/files/IPSJ-SES2016031.pdf application/pdf 637.0 kB 2018-08-24