@inproceedings{oai:ipsj.ixsq.nii.ac.jp:00174376,
 author = {佐藤, 直人 and 芹沢, 一 and 前田, 浩光 and 高橋, 伸明 and 前川, 義之 and 四野見, 秀明 and 村尾, 直哉 and 大島, 豊 and 田代, 敦 and 黒川, 勇 and 八木沢, 育哉 and 高田, 豊 and 清永, 章彦 and 大橋, 正己 and Naoto, Sato and Kazuyoshi, Serizawa and Hiromitsu, Maeda and Nobuaki, Takahashi and Yoshiyuki, Maekawa and Hideaki, Shinomi and Naoya, Murao and Yutaka, Ohshima and Atsushi, Tashiro and Isamu, Kurokawa and Ikuya, Yagisawa and Yutaka, Takata and Akihiko, Kiyonaga and Masami, Ohashi},
 book = {ソフトウェアエンジニアリングシンポジウム2016論文集},
 month = {Aug},
 note = {システムの仕様不具合を網羅的に検査する手段として，モデル検査がある．モデル検査とは，仕様を有限状態機械としてモデル記述し，その状態空間をモデル検査器と呼ばれるツールで機械的に網羅検査する技術である．検査により仕様不具合が検出された場合，モデル検査器はその不具合に至るまでの実行系列を反例として出力する．上流段階の設計では，仕様の簡略化のため，システムの振る舞いを抽象化して表現する場合がある．その場合，実際のシステムの振る舞いと一致しない反例が出力される可能性がある．これは偽反例と呼ばれ，不具合解析の障害になっている．偽反例を除去するためには，仕様が実システムの振る舞いと一致するように詳細化すればよい．しかし，上記のような目的で意図的に仕様を抽象化している場合は，その目的を達成できなくなる．そこで本稿では，仕様を詳細化せずに偽反例の出力を抑制する手法を提案する．さらに，提案手法に基づく作業を，形式言語を習得していない設計者でも実施可能にするモデル検査支援環境を提案する．本支援環境は，偽反例を入力として受け付け，その偽反例が出力されないように形式言語モデルを自動変更する．また本稿では，提案手法の実現性を確認するために行った適用実験結果も示す．},
 pages = {211--218},
 publisher = {情報処理学会},
 title = {偽反例の出力を抑制するモデル検査支援環境},
 volume = {2016},
 year = {2016}
}