2014 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 | モデル検査 / 分散システム / 分散アルゴリズム / 実行経路 / Maude |
|---|
| Outline of Annual Research Achievements |
ソフトウェアを含む計算機技術や理論計算機科学の発展により、これまでに多くのモデル検査器が開発され、多くの事例への適用が行われてきた。しかし、分散スナップショットアルゴリズム(DSA)への適用は活発ではないようである。DSAは、分散システムを計算の対象としており、望みの性質をLTLやCTL等ですなおに記述できないことが理由の一つとして考えられる。望みの性質は、s1、s2、s*を、それぞれ、スナップショットを取り始める状態、スナップショット、スナップショットを取り終える状態とすると、s*はs1から到達可能であるとともにs2はs*から到達可能であるというものである。この性質を分散スナップショット到達可能性(DSR)と呼ぶ。しかし、DSAは、分散システムの異常状態から正常状態への回復等において必須であり、分散システムの信頼性や復元力に大きく影響をするため、モデル検査等の形式検証の対象にすべきである。類似既存研究に、ChandyとMisraにより提案された人類初のDSAであるCLDSAがDSRを満たすことを書換え論理に基づく計算機言語Maudeシステムでモデル検査を行った事例研究がある。ただし、この事例研究では真にDSRのモデル検査を行えているかどうかの議論を行っていない。そこで、類似既存研究で用いられた方法で真にDSRをモデル検査できているのかどうかを確認するため、DSRの形式化を行った。DSRの形式化には2つの状態機械を必要とすることがわかった。計算の対象である分散システム(UDS)の状態機械とUDSにCLDSAを追加したシステムの状態機械の2つである。類似既存研究におけるモデル検査では後者の状態機械しか用いておらず、そこで用いられているDSRの記述と我々のDSRの形式化には差があることがわかった。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
類似既存研究の精査を行い、そこで用いられている方法で真にDSRのモデル検査を行えるかどうかを保証するには更なる研究を必要としていることがわかった。理由は以下のとおりである。DSRの非形式な記述を注意深く読み取ることで、DSRの形式化を行った結果、DSRの形式化には2つの状態機械を必要とすることがわかった。計算の対象である分散システム(UDS)の状態機械とUDSにCLDSAを追加したシステムの状態機械の2つである。類似既存研究におけるモデル検査では後者の状態機械しか用いておらず、そこで用いられているDSRの記述と我々のDSRの形式化には差があることがわかったからである。望みの性質を真にモデル検査できていることを保証することはとても大切である。さもなければ意図した望みの性質を満たしていないにもかかわらず満たしていると誤って結論付けてしまうかもしれない。本年度の研究実績は、類似既存研究で用いられた方法が真にDSRのモデル検査を行えることを必ずしも否定しているわけではなく、真にDSRのモデル検査を行えることを保証する第一歩にもなり得る。
|
| Strategy for Future Research Activity |
類似既存研究で用いられている方法で真にDSRのモデル検査を行えることを保証するには以下のことを示せば良い：我々のDSRの形式化と類似既存研究でのDSRの形式化が等価である。状態機械Mは、3組<S,I,T>である。Sは状態の集合で、I⊆Sは初期状態の集合で、T⊆S×Sは状態間の2項関係である。(s,s')∈Tを状態sから状態s'への遷移と呼ぶ。M |= isReachable(s2,s1)は、状態s1∈Sから状態s2∈SにMの状態遷移を0回以上適用することで到達可能であることを表すとする。M_{UDS}を計算対象であるUDSの状態機械、M_{CLDSA}をUDSにCLDSAを追加したシステムの状態機械とする。我々の形式化は以下のようになる：(∀s∈S_{CLDSA})(M_{CLDSA} |= terminates(s) ⇒ M_{UDS} |= isReachable(s*,s1) ∧ M_{UDS} |= isReachable(s2,s*))、ここで、M_{CLDSA} |= terminates(s)は状態s∈S_{CLDSA}でCLDSAが停止したことを表しており、s1、s2、s*は、sにおけるCLDSAの開始状態s1∈S_{UDS}、最終状態s2∈S_{UDS}、スナップショットs*∈S_{UDS}を表している。類似既存研究での形式化は以下のようになる：(∀s∈S_{CLDSA})(M_{CLDSA} |= terminates(s) ⇒ M_{CLDSA} |= isReachable(base-state(s*) control(...),base-state(s1) control(...)) ∧ M_{CLDSA} |= isReachable(base-state(s2) control(...),base-state(s*)))、ここで、base-state(...)やcontrol(...)は、UDSにCLDSAを追加したシステムの形式に使うものである。M_{UDS}とM_{CLDSA}の到達可能性が一致すること示すことができれば、両者の形式化は等価であることを導くことができる。このことを証明する。
|
| Causes of Carryover |
類似既存研究の精査を行い、そこで用いられている方法で真にDSRのモデル検査を行えることを保証するには更なる研究を必要としていることがわかり理論研究に時間を要したためパソコンを用いたモデル検査の実験を次年度以降に行うことにした。このため、実験用パソコンの購入を見送るとともに研究員の雇用時間を減らした。
|
| Expenditure Plan for Carryover Budget |
研究協力者への賃金：研究協力者として大学院の学生を雇用する予定である。前年度未使用額と合わせ、雇用人数を増やすか、雇用時間を増やすかすることで、本研究課題の更なる進捗を目指す。実験用パソコン：モデル検査の実験には高性能のパソコンを必要とする。このため、研究代表者及び研究協力者用の実験用パソコンの購入を予定する。調査・研究・成果発表旅費：国際会議や国内の研究会に参加し情報収集するとともに当該分野最先端の研究者と意見交換するための旅費に充てる予定である。なお、以下の国際会議への論文投稿を予定している：ICFEM 2015, Paris, 3-6 Nov, 2015。
|
Research Products
(1 results)
