研究課題
昨年度の成果を基礎に、クラウド環境でのトランザクション処理におけるデータ整合性評価の手法・方法論をより正確なものとするため、モデリングやシュミレーションに加え、より論理的な評価が可能な、モデル検査で使用される時相論理と時間オートマトンを組み合わせる手法の確立を行った。当初、証明支援システムを用いた論理的検証を考えていたが、対応できる範囲やモデル規模に制約があることから、より現実的なこの手法に変更した。これは昨年度に代替案として検討していたものである。モデル作成や検証にはUPPAALというツールを使用した。昨年まで使用していたカラーペトリネットに比べ、アプリケーションロジックの詳細な記述は難しいが、この部分の構造はすでに解明されたため、整合性の本質的な部分のみをモデル化することが可能となり、このツールの欠点を解消することができた。また、性能予測に関しても、前述のUPPAALに待ち行列理論を取り入れた、より現実的なモデルを作成し、これに実測データを組み合わせることで、より正確な予測を可能とした。また、UPPAALの検証機能によりSLA (Service Level Agreement)の評価も可能となった。セキュリティに関しては、クラウド単体での理論構築が難しいため、昨年に引き続き、一般化したwebフレームワークの枠組みの中で展開してゆく方法を取った。ここでは、関数型webフレームワークLiftを取り上げ、この適合性問題の一部としてセキュリティを扱った。
すべて 2016 2015
すべて 雑誌論文 (4件) (うち査読あり 3件、 謝辞記載あり 4件) 学会発表 (4件)
Proceedings of the 10th International Conference on P2P, Parallel, Grid, Cloud and Internet Computing
巻: 978-1-4673-9473-4 ページ: 134-140
Communications in Computer and Information Science
巻: 555 ページ: 251-265
10.1007/978-3-319-25579-8_15
電子情報通信学会技術研究報告
巻: 115(353) ページ: 19-24
巻: 115(486) ページ: 253-258
