@inproceedings{oai:ipsj.ixsq.nii.ac.jp:00193866, author = {大池, 勇太郎 and 小形, 真平 and 青木, 善貴 and 中川, 博之 and 岡野, 浩三 and Yutaro, Oike and Shinpei, Ogata and Yoshitaka, Aoki and Hiroyuki, Nakagawa and Kozo, Okano}, book = {ウィンターワークショップ2019・イン・福島飯坂 論文集}, month = {Jan}, note = {モデル検査において,複雑 ・ 大規模なシステムのモデルの反例を手動で解析することは,非常に時間がかかる.NuSMV では反例情報として,状態遷移により変化した変数の値が各状態ごとに出力されるだけであるため,変数の多い大規模なモデルでは開発者による解析が困難になりやすい.本稿では NuSMV から得られた反例解析の効率を向上させるため,反例を自動で変数ごとの遷移を確認できるように, 表形式に整理し保存する.また,反例をグラフとして可視化するためのツールを試作し,セマフォのモデルに対して実行し,誤りのある箇所を絞り込むことに有効な見込みを得られた.}, pages = {13--14}, publisher = {情報処理学会}, title = {NuSMVの反例解析支援ツールの試作}, volume = {2019}, year = {2019} }