実践! ソフトウェアモデル検査 HOME | お問い合わせ | サイトマップ | リンク
研究会のご紹介 オンラインサービス 支援ソフトウェア 実用化の研究
■ 支援ソフトウェア
モデル入力支援機能 | 検査項目入力支援機能 | 反例解析支援機能 | ダウンロード | 支援ソフトウェアに関するＱ＆Ａ
■ モデル入力支援機能
画面上でフロー図あるいは状態遷移図を入力すると、自動的にNuSMV専用言語で記述したSMVコードを作成します。煩わしいコーディングをしなくてもモデルを作成することができます。
■ 検査項目入力支援機能
モデル検査で一番難しいと言われる検査項目、すなわちCTL式の作成を支援します。実際の検査でよく使う特定の検査項目や、範囲と事象を指定する汎用的な検査項目を、日本語の意味を見ながらマウスのクリック操作だけで作成することができます。もちろんテキスト入力で自由に作成することもできます。
■ 反例解析支援機能
NuSMVから出力される反例はテキスト形式で実行列が羅列されているだけなので、このままではとても見やすいとは言えません。反例解析支援機能では、EXCELのように一覧表で表示したり、値が変化したところを色替え表示することで、反例を見やすくして解析を支援します。
■ ダウンロード
各種ツールをこのページからダウンロードできます。
■ 支援ソフトウェアに関するＱ＆Ａ
組込みシステム産業振興機構
関西産学官連携センター 組込みシステム技術連携研究体
先進的組込みソフト産学官連携プログラム 組込み適塾
サイエンスによる知的ものづくり教育プログラム トップエスイー
形式手法実践ポータル　Formal Methods User Group
Copyright(C) 2005-2011 Practical research group of Software Model checking. All Rights Reserved.