2013 Fiscal Year Research-status Report
クラウドトランザクションモデルの構築とクラウド適合アダプタ開発
| Project/Area Number |
25330094
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Research Institution | Ryukoku University |
|---|
Principal Investigator |
新川 芳行 龍谷大学, 理工学部, 教授 (70351343)
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Keywords | クラウドコンピューティング / トランザクション処理 / データ整合性 |
|---|
| Research Abstract |
初年度において、クラウドトランザクション処理の基本となるBASEトランザクションの形式化とモデル化を、カラーペトリネット(Colored Petri Net - CPN)と述語論理により行うための研究を行った。CPNによるモデル化では、モデルの拡張性と再利用性を向上させるため、モジュール化を徹底し、さらにモデルの機能記述となるCPN MLコードも機能階層化による汎用性を向上させた。一方、データ整合性制約を記述する述語論理を直接記述することは非現実的であるため、仕様記述言語のVDM++を用いた。これにより、データ構造とデータ処理およびデータ整合性制約が単一の記述体系に集約可能となった。この、クラウドトランザクションにおける機能面での特性の形式化・モデル化に加え、非機能面の要件の一つである、パフォーマンス評価に関するモデル化にCPNを使用するための方法論の基礎も確立した。ただしCPN自体には、時間概念を扱う機能がないため、拡張版である時間付CPNを用いている。時間付CPNは時間の確率統計的性質を、CPN Toolsの用意する分布関数により柔軟に表現できるが、時相論理・時間論理に基づく論理的性質の分析に弱いという欠点を持つ。この部分を補完するため、時間オートマトンと分岐時相論理に基づくモデル検査ツールのUPPAALによるモデル化も合わせて研究した。パフォーマンスモデルは、抽象モデルによる分析・評価には限界があるため、実環境としてGoogle App Engine (GAE)を選択し、構築モデルを適用するとともに、実測用プログラムによるパフォーマンス測定も行い、モデル精度の検証も行った。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
平成25年度の主要到達目標は一般化したクラウドトランザクション処理特性のBASEにつき、1).データ整合性の論理的記述と検証方法 2). クラウドトランザクション処理におけるパフォーマンス評価モデルの確立 3). クラウドセキュリティの形式化・モデル化 4).前記三項目のシミュレーション基盤の構築、の四項目であった。このうち1).と2).については完了しており、3).については研究が進行中となっている。また、4).については1).、2).に関する部分は完了し、3).に関する部分を残すのみとなっている。この点で 多少の遅れが発生しているが、パフォーマンスについては、実環境における実測との比較や、時間論理・時相論理の適用など、今後必要となる作業を前倒しにしており、総合的に判断して、おおむね順調との判断を行った。
|
| Strategy for Future Research Activity |
昨年度に引き続き、クラウドトランザクション処理におけるセキュリティ要件の形式化・モデル化の研究を継続するとともに、申請書の研究実施計画に基づいて、証明論的方法によりモデルの完全性を補完する。このために証明支援ツールIsabelleを用いることでこのデータの一般化を行い、すべてのデータベース・インスタンスに対し適合性とギャップの評価が行える仕組みを構築する。CPNがプロセス系のモデリングに適しているのに対しIsabelleがデータ制約や整合性の一般化に適しており、補完的に用いることで精度の高いフィットギャップ分析が可能となる。ここで、構築したモデルをIsabelle処理可能にするためのワークロードが高くなりすぎると判断した場合、CPN MLコードによる高階関数を用いる方法に切り替える準備を並行して行う。
|
| Expenditure Plans for the Next FY Research Funding |
購入予定の機器の価格改定などにより、予定金額より支払額が減ったため次年度使用額が生じた。
消費税の変更による価格改定等で相殺される。
|
