タグ

tlaに関するteppeisのブックマーク (2)

  • 実践TLA+ | 翔泳社

    設計だってテストしたい! 【書の内容】 書は Hillel Wayne, "Practical TLA+", Apress, 2018 の邦訳版です。 複雑精緻なシステムを構築する際に、設計そのもの、仕様そのものにバグがないかをテストできたら、もう少し幸せな開発人生を送れそうな気がします。 書は送金システムの小規模な仕様からTLA+を使ってヤバいバグを発見するところから始まります。この小さなサンプルをもとに、より良いアプリケーションの設計・テスト・構築に、どのようにTLA+を使えばよいかを理解し、実際のプロジェクトに援用できるよう、TLA+の演算子、論理、関数、PlusCal、モデル、および同時実行の基礎を学びます。 設計図の整理の仕方、分散システムや最終的な整合性の指定の仕方を学んだら、アルゴリズムのパフォーマンスやデータ構造、ビジネスコードやMapReduceなど、さまざまな実用

    実践TLA+ | 翔泳社
    teppeis
    teppeis 2021/07/26
    9月15日発売
  • CockroachDB から覗く形式手法の世界 #JTF2021w / July Tech Festa 2021 winter

    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
    teppeis
    teppeis 2021/01/25
    TLA+を使った形式手法の利用例
  • 1