実践！ソフトウェアモデル検査

■ 支援ソフトウェア

反例解析支援機能

NuSMVから出力される反例はテキスト形式で実行列が羅列されているだけなので、このままではとても見やすいとは言えません。反例解析支援機能では、EXCELのように一覧表で表示したり、値が変化したところを色替え表示することで、反例を見やすくして解析を支援します。

さらに、「ステップ実行モード」を使うと、フローチャートと状態遷移図の上で反例の経路を確認することができます。反例の実行列がフローチャート上で次々と色替え表示されるので、どのように処理が流れて、どこで不具合が発生しているのかが一目瞭然でわかります。

オンラインサービス

Copyright(C) 2005-2011 Practical research group of Software Model checking. All Rights Reserved.