| 研究概要 |
本研究は,利用者のオペレーティング・システムやネットワーク接続環境,更に個々の形式手法や検証ツールに依存しない情報システム仕様記述・検証のための総合環境を構築することを目指している。今年度は主に以下のような研究成果を上げた。
1.本研究で提案するシステムと,その基盤となる分散協調的作業を実現するフレームワークの設計を行った。本システムでは,形式手法に関する既存のツールや記法のためのファイルをサーバ上にアップロードし,これらに異なるオペレーティング・システムやネットワーク接続環境からアクセスしてWebブラウザ上で仕様の記述や検証が行えるようにする。その他,利用者ごとの形式手法に関する専門知識の格差を補うためのチュートリアル機能を設計した。
2.設計したフレームワークを,Reverse Ajax技術を用いて構築した。このフレームワークを用いると,分散されたネットワーク接続環境下でWebブラウザを介して複数人による協調作業を行えるアプリケーションを実装可能である。
3.上記のフレームワークを利用して,まずはZ記法という形式手法の既存の検証ツールをサーバにアップロードでき,更にインターネットを介して複数人で仕様の記述・検証ができる環境を実装した。
4.同様に,既存のモデル検査ツール3種(SPIN,SMV,UPPAAL)をサーバ上にアップロードし,システムの記述・検証ができるWebアプリケーションを実装した。
|
