July Tech Festa 2018 で使用したスライドです。二相コミットを例として、分散アルゴリズムの検証にモデル検査を使用する手法について解説しています。また、代表的なモデル検査ツールである SPIN、TLA+、P について、同じシステムを各ツールで記述してみることでその特定の違いについて学びます。 イベント概要:https://2018.techfesta.jp/speakers#C40 ブログ記事:http://ccvanishing.hateblo.jp/entry/2018/08/01/055608
![分散システム、本当に「正しく」開発できますか? #JTF2018 / July Tech Festa 2018](https://cdn-ak-scissors.b.st-hatena.com/image/square/85c87588131bea566afe930f99bfb67975edfc95/height=288;version=1;width=512/https%3A%2F%2Ffiles.speakerdeck.com%2Fpresentations%2F3a93278b01104211ad3f73c1aee0e7c3%2Fslide_0.jpg%3F10492427)