研究課題
挑戦的萌芽研究
分散スナップショットアルゴリズム（DSA）を書換え論理に基づく計算機言語Maudeのメタプログラム（MP）として記述する方法と分散スナップショット到達可能性（DSR）を直接モデル検査する方法を考案し、実験により有効性を確認した。従来法では、分散システム（DS）ごとにDSAも含め毎回記述する必要があったのに対し、提案方法では、MPを１回記述しさえすれば、DSのみの記述で十分であるという利点がある。また、DSRを直接モデル検査可能になったため、より高速にモデル検査可能になり、性質を満たさない場合反例を提示できるようにもなった。提案方法は、DSを計算の対象とする分散アルゴリズムに適用可能である。
すべて 2017 2015 その他
すべて 国際共同研究 (1件) 雑誌論文 (5件) (うち国際共著 3件、 査読あり 4件、 オープンアクセス 4件、 謝辞記載あり 3件)
Proc. of IEEE ICDCS 2017
巻: NA
Proceedings of 6th International Workshop on SOFL + MSVL (SOFL+MSVL 2016), Springer
巻: LNCS 10189 ページ: 201-219
10.1007/978-3-319-57708-1_12
Proc. of 2015 Second International Symposium on Dependable Computing and Internet of Things
巻: - ページ: 30-39
10.1109/dcit.2015.13
巻: - ページ: 1-10
10.1109/dcit.2015.23
信学技報
巻: 114 ページ: 49-54
110010001774
