2015 Fiscal Year Research-status Report
分散システムを計算の対象とする分散アルゴリズムのモデル検査に関する研究
| Project/Area Number |
26540024
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
緒方 和博 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (30272991)
|
|---|
| Project Period (FY) |
2014-04-01 – 2017-03-31
|
| Keywords | モデル検査 / 分散スナップショット / 分散アルゴリズム / 分散システム / 状態機械 / 到達可能 |
|---|
| Outline of Annual Research Achievements |
ソフトウェアを含む計算機技術や理論計算機科学の発展により、これまでに多くのモデル検査器が開発され、多くの事例への適用が行われてきた。しかし、分散スナップショットアルゴリズム（DSA）への適用の報告は多くはない。DSAは、分散システムを計算の対象としており、望みの性質を既存のLTLやCTL等で素直に記述できないことが理由のひとつであると考えられる。望みの性質は、s1, s2, s*を、それぞれ、スナップショットを取り始める状態、スナップショットを取り終える状態、スナップショットとすると、s*はs1から到達可能であり、s2はs*から到達可能であるというものである。この性質を分散スナップショットの到達可能性（DSR）と呼ぶ。これまでの研究により、人類初のDSAであるChandyとLamportにより提案されたDSA（CLDSA）のDSRの形式化には２つの状態機械、計算の対象である分散システム（UDS）の状態機械M_UDSとUDSにCLDSAを重ね合わせることで得られるシステムの状態機械M_CLDSA、を必要とすることがわかっていた。一方、CLDSAがDSRを満たすことのモデル検査に関する既存研究では、DSRの形式化にはM_CLDSAのみが使われている。両者のDSRの形式化には見た目の差はあるが、等価であることを証明した。これにより、既存のCLDSAがDSRを満たすことのモデル検査の方法は、CLDSAが意図どおりの性質の検査を行えることの保証ができたことになる。この証明に加え、CLDSAはUDSの挙動を本質的に変更することはない、ことの証明も行った。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
これまでの研究成果は、CLDSAの自然言語によるDSRの記述に則り素直に形式化するとM_UDSとM_CLDSAの２つの状態機械を必要とする、ということである。これは、M_CLDSAのみを用いる既存研究のDSRの形式化と見かけ上異なっている。今回の研究成果である、これら２とおりの形式化は見かけ上異なるが等価であるという事実は、既存研究で提案されているCLDSAのDSRに関するモデル検査方法が、意図どおりの検査を行えていることを保証する。CLDSA等のDSAは、クラウド等の分散システムのバックアップ作成等にとって本質的に重要な技術であり、信頼性を高めることは必須である。今回の成果は、CLDSAのみならず他のDSAに対しても十分に適用可能であり、社会インフラとなったクラウド等の分散システムの信頼性向上に少なからず寄与できたということができる。
|
| Strategy for Future Research Activity |
既存研究のCLDSAのモデル検査では、具体的なUDSにCLDSAを重ね合わせることで得られるシステムの状態機械M_CLDSAのシステム仕様をMaude（代数仕様言語OBJの流れをくむ書換え論理に基づく仕様記述・プログラミング言語・処理系）で記述していた。この方法では、個々のUDSごとにシステム仕様を記述する必要がある。CLDSAは、UDSをパラメータとして取り、UDSにCLDSAを重ね合わせることで得られるシステムを生成するもの、つまり分散システムを計算の対象とする分散アリゴリズムととらえると、MaudeのメタプログラムとしてCLDSAの（メタ）システム仕様を記述することが可能になる。このようにCLDSAのメタシステム仕様を記述すると、UDSのシステム仕様を与えるだけで、UDSにCLDSAを重ね合わせることで得られるシステムの状態機械のシステム仕様を自動で得ることができ、個々のUDSごとにシステム仕様を記述する必要がなくなる。さらに、この方法では、UDSの状態機械M_UDSとUDSにCLDSAを重ね合わせることで得られるシステムの状態機械M_CLDSAの２つの状態機械を利用することができるため、２つの状態機械を用いたDSRの形式化を直接モデル検査することも可能になる。M_UDSのみを用いたDSRの形式化とM_UDSとM_CLDSAの２つの状態機械を用いたDSRの形式化の等価性については証明済みだが、どちらの形式化に対するモデル検査のほうがより効率的にモデル検査できるかは研究の対象である。このことも解明する予定である。さらに、CLDSA以外のDSAや一般の分散システムを計算の対象とする分散アルゴリズムのモデル検査には、複数の状態機械を利用できる仕組みが必要であることが予想されるため、そのような分散アルゴリズムのメタシステム仕様の作成方法ならびに複数の状態機械を利用できるモデル検査方法の解明は非常に重要である。
|
| Causes of Carryover |
計算の対象である分散システムUDSにCLDSAを重ね合わせることにより得られるシステムの状態機械M_CLDSAだけを用いるDSRの形式化とM_CLDSAに加えUDSの状態機械M_UDSも用いる、すなわちM_UDSとM_CLDSAの２つの状態機械を用いるDSRの形式化が等価であることの証明、すなわち理論研究に時間を要したため、予定していたモデル検査等の実験を先送りすることにした。このため、実験補助のための研究協力者の人件費・謝金と旅費に未使用額が生じた。
|
| Expenditure Plan for Carryover Budget |
モデル検査等の実験を補助してもらう研究協力者の人数を増やすか、雇用時間を増やすかすることで、本研究課題の更なる進捗を目指す。これまでの研究成果とあわせ次年度以降の研究成果発表のために旅費を活用するとともに実験用パソコン等の購入にあてる予定である。
|
Research Products
(3 results)
