@inproceedings{oai:ipsj.ixsq.nii.ac.jp:00206732,
 author = {大池, 勇太郎 and 小形, 真平 and 青木, 善貴 and 中川, 博之 and 小林, 一樹 and 岡野, 浩三},
 book = {ソフトウェアエンジニアリングシンポジウム2020論文集},
 month = {Sep},
 note = {NuSMV によるモデル検査では，多数の部分式に分解できる長大な検査式に対して，大規模な反例が出力された場合，反例で満たされていない部分式（以下，不満足な部分式）を手動で識別することに時間がかかる問題がある．そこで本研究では，不満足な部分式を自動識別するための解析手法と支援ツールを提案する．提案手法では，構文解析により複雑な検査式を部分式に分解し，部分式が反例で満たされるかどうかを調べて不満足な部分式を識別する．提案手法の有効性評価のために交通制御システムのモデルに適用した結果，不満足な部分式を正しく識別できたため，提案手法は有効である見込みを得た．},
 pages = {23--31},
 publisher = {情報処理学会},
 title = {モデル検査における複雑な検査式に対する反例解析手法の提案},
 volume = {2020},
 year = {2020}
}