July Tech Festa 2021 winter で使用したスライドです。 バグのない分散システムの設計は果たして可能でしょうか? この問いに対する一つの答えとして、CockroachDB では形式手法ツール TLA+ を用いて分散トランザクションの正しさを担保しています。 形式手法はシステムの挙動を数学的に解析する技法で、「ノードが特定のタイミングで故障した場合にのみ発生するバグ」といった再現困難な問題を確実に検出することができます。 本講演では、CockroachDB の事例を通して、形式手法が実世界で活用されている様子をお伝えします。 イベント概要:https://techfesta.connpass.com/event/193966/ ブログ記事:https://ccvanishing.hateblo.jp/entry/2021/01/24/185819 録画:https:/
![CockroachDB から覗く形式手法の世界 #JTF2021w / July Tech Festa 2021 winter](https://cdn-ak-scissors.b.st-hatena.com/image/square/24d7cc6d365a3dc8160100b733137c0e4fdec2c1/height=288;version=1;width=512/https%3A%2F%2Ffiles.speakerdeck.com%2Fpresentations%2F22e7d3cd87af4508b3acd05dacf7ad3b%2Fslide_0.jpg%3F17172884)