|
本研究では，モデル検査を中心とした検証手法を，スマートコントラクト，および，その実行基盤であるブロックチェーンに適用することによって，これらの応用におけるトラスタビリティを実現することを目標とした．研究では，特にこれらの基礎となるコンセンサスアルゴリズムに注目し，不具合を検証する新しい手法を開発した．提案手法では，通常の逐次的なプログラムによって，メッセージ遅延や故障を含めたアルゴリズムの動作を模倣し，逐次プログラムに対するモデル検査手法を適用する．実際のアルゴリズムを対象に，安全性の違反を検出できることを示すことができた．
|
