| 研究概要 |
本研究は, 利用者のオペレーティング・システムやネットワーク接続環境, 更に個々の形式手法や検証ツールに依存しない情報システム仕様記述・検証のための総合環境を構築することを目指している。前年度の成果を踏まえ, 今年度は主に以下のような研究成果を上げた.
1. 前年度に開発したシステムと, その基盤となる分散協調的作業を実現するフレームワークの改良を行った. 本システムでは, 形式手法に関する既存のツールや記法のためのファイルをサーバ上にアップロードし, これらに異なるオペレーティング・システムやネットワーク接続環境からアクセスしてWebブラウザ上で仕様の記述や検証が行えるようにする. その他, 利用者ごとの形式手法に関する専門知識の格差を補うためのチュートリアル機能の充実を図った。特に, データベースを用いた仕様記述の再利用機能と, これらを用いた入力補完機能を強化した.
2. 開発したフレームワークを, 様々な検証へ応用できることを示した. このフレームワークを用いると, 分散されたネットワーク接続環境下でWebブラウザを介して複数人による協調作業を行えるアプリケーションを実装可能である。
3. 開発したフレームワークを利用して, isabelle, Coq, PVS, SPIN, SMVとった検証ツールを用いてインターネットを介して複数人で仕様の記述・検証ができることを確認した. また性能評価も行った.
4. 前年度と今年度の研究成果やその応用を国内のシンポジウムや国際会議において発表した. 更に, 雑誌論文にも公表した。
|
