2005 Fiscal Year Annual Research Report
高信頼性Webアプリケーション構築のための振舞い検証モデル
| Project/Area Number |
16500027
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
結縁 祥治 名古屋大学, 大学院・情報科学研究科, 助教授 (70230612)
|
|---|
| Keywords | 通信プロセスモデル / Webアプリケーション / π計算 / 代数的意味論 / タイムアウト処理 |
|---|
| Research Abstract |
本年度は、通信プロセスモデルを基本とするWebアプリケーションの動作モデルに対して研究を行った。MVCアーキテクチャによるwebアプリケーションの動作をπ計算によって定式化するための検討を行った。結果として、この記述を与えるための体系の拡張についての結果が得られた。
拡張は以下の2点について検討した。
1.GUI構築において描画オブジェクトの意味論の研究
通信をGUIオブジェクトの生成・消滅、および、GUIオブジェクトにおけるイベントの受け渡しに対応させる枠組みを提案し、実現を行った。さらに基本的な意味論について検討した。
2.時間経過による意味論の拡張
遅延演算子をπ計算に導入した体系の意味論について検討を行った。時間を考慮した双模倣関係が限定された文脈において合同性が成立することを示した。
これらの拡張において、以下のような知見が得られた。
GUI意味論では実現に加えて、GUIを操作する際、GUIが正常に動作するための制約について、本枠組みを基本とした形式的な検証の枠組みが構築できることを示した。
時間を含めた意味論について、等価性に対して時間を観測できるように拡張すると意味論は大変強い意味論となった。このため、一般的な合同性を得ることはできず、限られた文脈でのみ合同性が得られた。このことは、タイムアウトなどを伴うソフトウェアコンポーネントをソフトウェア部品として使う場合には組みこむ環境に対して制限が大きいことを示している。さらに、等価性に加えて実行速度の比較を行う意味論を提案した。ここではサーバーなど時間に対して許容度が大きい環境においては合同性が得られた。
今後はwebにおけるコンポーネントソフトウェアのモデル化をさらに進め、信頼性を保証できるための条件について明らかにする研究を進める。
|
