@techreport{oai:ipsj.ixsq.nii.ac.jp:00094188,
 author = {後藤亮馬 and 和崎克己},
 issue = {8},
 month = {Jul},
 note = {合意問題は分散システムの研究分野において重要な問題の一つであり，非同期分散アルゴリズムにおいては，合意問題が解決されているかを確認することが困難である．本研究では，非同期分散アルゴリズムの正当性を，モデル検査によって検証することを目的として，モデル検査器 SPIN を用いて，非同期分散合意アルゴリズムである Chandra-Toueg アルゴリズムの正当性を検証する．SPIN とは通信プロトコルの検証を目的として提案されたモデル検査ツールであり，使用記述言語 PROMELA で記述された振る舞いを，網羅探査により検査することができる．モデルの作成を行う際には，PROMELA 本来の記述方法では困難であった表現を行うために，グローバルタイムアウト機構などのいくつかの工夫を行った．Chandra-Toueg アルゴリズムで使用されている巡回調停者方式では，調停者が健全か否かを考慮しない．また，実際には調停者変更を行った後，ノード間でのリセット動作などの同期を取るべきである．以上二つの理由から，調停者変更時に健全性の判定機能を追加し，調停者変更後に同期をとる選出方法に変更した．作成した通常モデルと拡張モデルを使用してデットロック検査を行い，正当性を検証した．},
 title = {調停者の選出方法を考慮した分散合意アルゴリズムのPROMELAモデルと検証},
 year = {2013}
}