2006 Fiscal Year Annual Research Report
高信頼性Webアプリケーション構築のための振舞い検証モデル
| Project/Area Number |
16500027
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
結縁 祥治 名古屋大学, 大学院情報科学研究科, 助教授 (70230612)
|
|---|
| Keywords | Webアプリケーション / 通信ブロセスモデル / 形式意味論 / プログラム検証 / インターネット高度化 |
|---|
| Research Abstract |
本年度は、通信プロセスモデルをWebアプリケーションの振舞いに応用する技術の開発を目標に研究を進めた。しかし、Webアプリケーションの振舞いを十分な精度で記述する手法とその基礎的な実現手法についてのみ研究成果が得られた。
以下に、本年度得られた研究結果を示す。
1.Webアプリケーションのような通信を含む振舞いを抽象的に表す技法として、関数型言語Haskellに通信プロセスモデルにおける通信の機能を導入したPi-Monadの提案と実装を行った。この実現によって、Haskell言語の持つ型による厳密性を保ちながら、通信の振舞いを記述できるようになった。
2.コレオグラフィ記述言語について研究を行った。主にWebサービスのような粒度の大きな分散サービスに用いられているコレオグラフィー記述を細かい粒度の並行分散ソフトウェアに適用する枠組みについて研究した。簡単な分散アプリケーションとして、家電機器の連携動作についてのモデル化を行った。Webアプリケーションはこの発展形として捉えることができる。
3.Webアプリケーションの一連の動作をまとめるセッションの概念をできるだけ構文として与える形式的体系についての検討を行った。
セッション記述をPi-Monad上で記述する手法についても検討し、Webアプリケーションの高信頼の基盤となる枠組みが確立された。
|
