実践! ソフトウェアモデル検査 HOME | お問い合わせ | サイトマップ | リンク
研究会のご紹介 オンラインサービス 支援ソフトウェア 実用化の研究
■ オンラインサービス
概要 | モデル検査サービスの手順 | 検査ファイルのアップロード | 検査結果の確認 | 検査ファイルについて | 「さつき」の本格利用について
モデル検査サービスの手順
1.検査ファイルの作成
まず,検査対象となるファイル(以降,SMVファイルと呼びます)を作成します。ファイルの作成方法につきましては,こちらを参照ください。
2.検査ファイルのアップロード
SMVファイルの作成を完了しましたら,これをWebサイトにアップロードします。[検査ファイルのアップロード]のリンクをクリックし,アップロード用のページを開いてください。
アップロード用のページの入力エリアにSMVファイルのパス情報を入力してください。(もしくは,[参照]ボタンをクリックして,ファイル選択ダイアログから選択することも可能です)
SMVファイルのパス情報の入力を完了しましたら,[アップロード]ボタンをクリックしてください。
3.サービス開始の通知
アップロードされたSMVファイルに対し,適切な書式で記述されているか文法チェックを行います。チェックの結果,異常が発見されなければこれを受け付け,サービスを開始します。
SMVファイルを受け付けた場合,お客様のブラウザに「ID」と「パスワード」を出力します。アップロードしたSMVファイルの検査結果を確認するために必要となりますので,忘れずに正しく書き留めていただきますようお願いいたします。或いは,IDとパスワードの一式を記載したテキストファイルをページからダウンロード可能としておりますので,これをダウンロードし,大切に保管しておいてください。
なお,文法チェックで異常を発見した場合,その異常の内容をお客様のブラウザに出力しますので,その内容を基にSMVファイルを修正し,再度アップロードしてください。文法チェックで異常を発見した場合は,「ID」と「パスワード」は発行されませんのでご承知おきください。
また,文法チェックで異常が発見されなかった場合でも,モデル検査の実行時に異常が発生しないことを保障するわけではありませんので,ご了承ください。
4.モデル検査の実行
アップロードされたSMVファイルは,当サイトのWebサーバから,(独)産業技術総合研究所 組込みシステム技術連携研究体様が管理される連携検証施設「さつき」に転送され,そこで,64bit版モデル検査器によるモデル検査が実行されます。
5.検査結果の確認
SMVファイルの検査結果を確認するためには,[検査結果の確認]のページをクリックし,受け付け完了時に入手したIDとパスワードでログインしてください。その時点で検査が完了済みの場合,検査結果の出力ファイルをダウンロードすることができます。また,検査がまだ完了していない場合は検査結果の出力ファイルをダウンロードするためのリンクは表示されません。しばらく時間をおいて,改めてアクセスしてください。
組込みシステム産業振興機構
関西産学官連携センター 組込みシステム技術連携研究体
先進的組込みソフト産学官連携プログラム 組込み適塾
サイエンスによる知的ものづくり教育プログラム トップエスイー
形式手法実践ポータル Formal Methods User Group
Copyright(C) 2005-2011 Practical research group of Software Model checking. All Rights Reserved.