2016 Fiscal Year Annual Research Report
A study on model checking of distributed algorithms whose computational targets are distributed systems
| 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 |
Maudeのメタプログラムとして分散スナップショットアルゴリズム（CLDSA）の仕様を作成した。Maudeは書換え論理に基づく計算機言語・処理系で、代数仕様言語・処理系OBJ3の流れをくむ。メタプログラムは、プログラムを入力とし、それに手を加える等のことをし、別のプログラムを結果として返す等をする。書換え論理はリフレクティブであるため、Maudeではメタプログラムを簡便に記述すための機能を提供する。CLDSA等の分散スナップショットアルゴリズムは、スナップショットを取る対象の分散システムには本質的な影響を与えることなく重ねあわされて稼働する。このため、分散スナップショットが所望の性質を満たすことのモデル検査を行う場合、対象の分散システムと重ね合わせたものを仕様として記述する必要がある。このため、分散システムごとにCLDSAも含めて毎回仕様を作成する必要があり煩雑である。CLDSAに関係する箇所は、対象である分散システムとは独立しており、分散システムごとに変更する必要はない。そこで、CLDSAの仕様をMaudeのメタプログラムとして記述することにした。対象となる分散システムの仕様をそのメタプログラムに入力として与えると、CLDSAがその分散システムに重ねあわされたシステムの仕様が自動で生成される。これにより、対象である分散システムごとに毎回CLDSAに関係する箇所を記述する手間を省くことができる。メタプログラムにより生成される仕様に対してモデル検査を行うことができる。いくつかの例題を用いたモデル検査実験の結果、メタプログラムにより生成される仕様に対してのモデル検査の処理速度は、手動でCLDSAを分散システムに重ね合わせたものの仕様に対してのモデル検査の処理速度よろ勝っていることが分かった。研究成果は、分散システムのトップ会議であるIEEE ICDCS 2017に採録された。
|
