|
本研究では，モデル検査を中心とした形式検証を，スマートコントラクト，および，その実行基盤であるブロックチェーンに適用することによって，これらの応用におけるトラスタビリティを実現することを目標とした．
最終年度である2021年度では，特に，ブロックチェーンの中心技術であるコンセンサスアルゴリズムの検証について研究を行った．具体的には，2020年度において提案した，小スコープ仮説に基づく形式検証手法について，その開発を進めた．小スコープ仮説は，不具合による異常は小さい動作範囲中でも顕在化するという考えであり，提案法ではこの考えに基づき，プロセス数が少ない場合や，少ないステップ数での動作を網羅的に探索することで，アルゴリズムの誤りの検出を行う．この方法では，分散型のアルゴリズムであるコンセンサスアルゴリズムを，1) 逐次的な動作に解釈し，2) その上で有界モデル検査というプログラムの一定の長さの動作を網羅的に探索する検証手法を適用する．本年度は，いくつかの既存のコンセンサスアルゴリズムに対し，実際に本手法を適用できることを示した．
研究当初，主たる目的としていたスマートコントラクトの検証に関しては，並行して多くの研究が発表されたため，3年間の研究を推進する過程で，スマートコントラクトの実行基盤の核となるコンセンサスアルゴリズムの検証に注力した結果，上記の新しいコンセンサスアルゴリズムの検証手法を開発することができた．
|
