状態機械をとおして
複雑な分散システムの核心に迫る！

緒方研究室　OGATA Laboratory
教授：緒方 和博（OGATA Kazuhiro）

E-mail：
［研究分野］
計算機科学、ソフトウェア工学、形式手法
［キーワード］
分散システム、状態機械、定理証明、モデル検査

研究を始めるのに必要な知識・能力

初歩的な論理学や集合論などについて知っていたり、プログラミング（特にスレッドを用いた並行プログラムの作成）の経験もあったりしたほうが良いですが、配属後に学修を開始したとしても研究を始めるのに支障はないです。もっとも大切なことは研究テーマへの高い関心と学修・研究意欲の継続です。

この研究で身につく能力

主に抽象化能力と論理的思考力を身に付けることができます。抽象化能力と論理的思考力を身に付けると、複雑な事象を平易なことばで筋道を立てて簡潔に説明できるようになります。

【就職先企業・職種】 情報・通信業、電機機器など

研究内容

　状態機械は、初期状態を含む状態の集合と状態間の2項関係から構成されます。状態間の2項関係を状態遷移と呼びます。このため、状態機械は状態遷移機械とも呼ばれます。通信プロトコル、電子商取引プロトコル、相互排除プロトコル、スナップショットプロトコル、意思決定プとコルなどの分散システムは、状態機械として記述することができます。
　ノードやネットワークの局所状態から構成される大域状態を状態とし、メッセージの送受信などのノードやネットワークの局所状態の変化を状態遷移とすることで、分散システムを状態機械として記述できます。そうすると、分散システムの満たすべき要件は状態機械の不変性等の性質として表現でき、分散システムが要件を満たすことの確認は、状態機械が性質を満たすことを検証することで行うことができるようになります。本研究室では、分散システムの状態機械による記述方法、満たすべき要件の性質としての表現方法、それに状態機械が性質を満たすことの検証方法についての研究を行っています。

1．機械学習を用いた補題発見に関する研究：

通信信頼性、支払合意性、相互排除性などの分散システムの満たすべき要件は状態機械の不変性と呼ばれる性質で表すことができます。不変性とはすべての到達可能状態で真になる状態述語のことです。不変性の証明は、状態の到達可能性を決定できる状態述語isReachableを構成できれば十分です。つまり、isReachableを構成できさえすれば状態機械、ひいては分散システムの核心に迫ることができることになります。しかし、isReachableを構成できるアルゴリズムは存在しないことがわかっています。そこで、機械学習を用いてisReachableを構成することを試みています。機械学習は学習用データに基づく訓練の後、これらのデータのみならず新規のデータに対しても正しい判断を下せるようにするための技術です。本研究では、状態機械から生成できる到達可能状態を学習用データとして用い、あらゆる状態に対し到達可能であるかどうかの判断を下せるようになること、すなわち、isReachableの構成を試みます。

2．分散システムを計算の対象とする分散アルゴリズムのモデル検査に関する研究：

分散スナップショットアルゴリズム等の分散システムを計算の対象とする分散アルゴリズムの満たすべき性質の素直な記述には実行系列（ある条件を満たす状態の列）を通常の値として扱える必要があります。しかし、Spin等の既存のモデル検査器では実行系列を通常の値として扱えません。このため、そのような分散アルゴリズムの満たすべき性質を素直に記述できません。そこで、分散アルゴリズムならびに性質を素直に記述できるとともに効率良くモデル検査できることを目指し、実行経路を通常の値として扱えるモデル検査法を考案し、それに基づくモデル検査器を設計・実装し、分散スナップショットアルゴリズム等の事例に適用することでそれらの有効性を確認することを行っています。

主な研究業績

1. Kazuhiro Ogata and Kokichi Futatsugi: Modeling and verification of real-time systems based on equations, Science of Computer Programming, 66（2）: 162-180, Elsevier, 2007.
2. Kazuhiro Ogata and Kokichi Futatsugi: Proof Score Approach to Analysis of Electronic Commerce Protocols, International Journal of Software Engineering and Knowledge Engineering, 20（2）: 253-287, World Scientific, 2010.
3. Kazuhiro Ogata, Kokichi Futatsugi: Compositionally Writing Proof Scores of Invariants in the OTS/CafeOBJ Method, The Journal of Universal Computer Science （J. UCS）, 19（6）: 771-804, J.UCS consortium, 2013.

使用装置

代数仕様言語CafeOBJ（本学で開発された数少ない日本初の計算機言語のひとつ）
代数仕様言語Maude（CafeOBJの姉妹言語）