| 概要 |
| ■ 背景 |
| 当サイトでもモデル検査器としてNuSMVをはじめとした各種のモデル検査器を紹介しておりますが，モデル検査によるソフトウェアの検証の実用化にあたっては幾つかの課題があります。 |
|
| 課題の一つとして「状態爆発の問題」があります。実際のシステム内容をそのままモデル化すると，検査を実施しても早々に利用可能なメモリの上限に達してしまい結果を出力するところまで辿り着けないため，その結果，システムの事実性を損なわずに抽象化を図るといった難しい作業が必要となってしまいます。この課題を解決する一つの手段として，当研究会では64bit版モデル検査器に着目し，これの開発を行いました。 |
|
| 課題のもう一つとして，「モデル検査の実行環境の問題」があります。昨今，情報セキュリティの重要性が強く認識されており，その結果，モデル検査器自体を各企業で使用しているPCにダウンロードして試すといった使い方は難しくなった，或いはできなくなったとの話もお聞きしています。この課題の解決策の一つとして，当研究会ではインターネットを介しての「Webシステムによるモデル検査サービス」を考案しました。 |
|
| 当研究会が目指しております「モデル検査技術の実用化」に向けては，企業が安心して使用でき，かつ高性能なモデル検査サービスの実現が必要不可欠と考えており，そのサービスの施行として当サイトでの「モデル検査サービス」を開始した次第です。 |
|
＜モデル検査サービスの利用期間について＞
本サービスの試行期間は2011年2月末まで 2012年3月末までを予定しておりますが，予告なしに中断，或いは終了する場合があります。なお，本サービスの中断，或いは終了によって生じるいかなる損害についても本研究会は一切責任を負いません。本サービスを利用される方は，この点を同意いただけているものとみなします。ご了承ください。
|
|
|
| ■ システム構成 |
| このモデル検査サービスを構成する要素は，以下の3つとなります。 |
| (a) 依頼者のPC |
| (b) Webサーバ |
| (c) 連携検証施設「さつき」 |
| 依頼者は，(a)自身のPCからInternetExploler等のブラウザを介して(b)のWebサーバにモデル検査対象のファイルをアップロードします。次に，アップロードされたファイルを(b)のWebサーバから(c)の連携検証施設「さつき」に転送し，(c)のさつきにてモデル検査を実行します。モデル検査を完了しましたら，その検査結果のファイルを(c)のさつきから(b)のWebサーバに転送し，その内容を(a)の依頼者のPCでお使いのブラウザを介して依頼者にお届けします。 |
|
|
| ■ セキュリティについて |
| 本サービスで使用するWebサーバは，セコムトラストシステムズ社よりSSLサーバ証明書を発行していただいております（詳細は，ページ右下のバナーをクリックください）。依頼者のPCとWebサーバとの間でのデータのやり取りはSSLで暗号化されていますので，盗聴や改ざんの心配はありません。 |
|
| 同様に，Webサーバとさつきとの間のデータ転送においても，SSLで暗号化された中での通信となります。 |
|
＜SSLサーバ証明書について＞
SSLサーバ証明書は「www.modelcheck.jp」のURLに対して発行されたものです。「modelcheck.jp」等の異なるURLで当サイトにアクセスしてバナーをクリックした場合は「リンク元が証明書と一致しません。サイトを確認して下さい」とのメッセージがページに出力されます。お手数ですが，「www.modelcheck.jp」のURLでアクセスした上でSSLサーバ証明書の再確認をお願いいたします。 |
|
|
| ■ 関連データの運用について |
アップロードしていただいたSMVファイルや検査結果のファイルは，その計算機上で不要になった後すぐに削除し，計算機上で残り続けることはありません。例えば，WebサーバにアップロードされたSMVファイルは，さつきへの転送完了後はWebサーバから削除します。同様に，さつき内でのSMVファイルは，モデル検査の完了後に削除します。
ただし，Webサーバ上の検査結果ファイルのみは，依頼者が結果をダウンロードするための猶予期間を1週間設けているため，Webサーバに検査結果が転送されてから1週間後に削除する仕様としております。 |
|
|
|
