実践! ソフトウェアモデル検査 HOME | お問い合わせ | サイトマップ | リンク
研究会のご紹介 オンラインサービス 支援ソフトウェア 実用化の研究
■ オンラインサービス
概要 | モデル検査サービスの手順 | 検査ファイルのアップロード | 検査結果の確認 | 検査ファイルについて | 「さつき」の本格利用について
検査ファイルについて
検査ファイルの構文は，モデル検査器NuSMVの検査ファイルの構文のサブセットです。
検査ファイルについてはこちらをご参照ください。
事前知識として必要なNuSMVの構文については下記の書籍で詳しく説明されています。
モデル検査［初級編］ ← クリックすると産業技術総合研究所　組込みシステム技術連携研究体の書籍紹介のページを表示します。
上記の書籍で紹介されているサンプルのうち，本サービス用の検査ファイルに書き換えたファイルをダウンロードできます。
- Alpha.smv　（例題「システムα」）
- lamp.smv　（例題「ランプ点灯？」）
- semaphore.smv　（例題「並行システムと排他制御」）
- counter.smv　（例題「３進カウンタ」）
- Ctest.smv　（例題「プログラム（C言語）の試験」）
組込みシステム産業振興機構
関西産学官連携センター 組込みシステム技術連携研究体
先進的組込みソフト産学官連携プログラム 組込み適塾
サイエンスによる知的ものづくり教育プログラム トップエスイー
形式手法実践ポータル　Formal Methods User Group
Copyright(C) 2005-2011 Practical research group of Software Model checking. All Rights Reserved.