July Tech Festa 2018 で分散システムの検証について話してきました / #JTF2018 - チェシャ猫の消滅定理

先日行われた July Tech Festa 2018 で、モデル検査を使った分散アルゴリズムの検証について発表してきました。 前半はオートマトンによるシステムの記述と検査の基礎について、後半は三種類のツール SPIN、TLA+、P による記述方法の紹介、といった内容です。 後半のソースコード紹介が散文的な感じになってしまって、いまいちメリットが伝わらない感じだったので、次回があればもっとエモいスライドにしようと思います。 分散アルゴリズムの形式化 定理証明による検証 今回の話の流れとして「分散システムにはモデル検査が有効」と述べていますが、必ずしも定理証明が分散システムの検証に向かないという趣旨ではありません。 例えば、定理証明器 Coq によって分散システムを証明するためのフレームワークとして Verdi が開発されています。 github.com さらに、Coq は実行可能なコードも

[Nyoho]

形式手法

[igrep]

“個人的には本当の初心者にまず薦めたいモデル検査ツールは Alloy なんですよね。近々 Alloy の初心者向けハンズオンを開催しようという腹案も”