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