eSparkはTLA+で3つのルールすべてを満たす設計が存在しないことを証明し、その後1つを手放した

小学校向けの教育テクノロジー提供企業であるeSpark Learningは、顧客ごとに手作業で不定期の設定プロセスを運用しており、それが複数のサードパーティ製システムを連携させ、顧客のITネットワークを直接変更していた。ユーザー基盤が拡大するにつれ、その作業負荷は持続不可能になった。サポートチームは、維持するだけで毎年新たに正社員を1人採用する必要があることに気づいた。経営陣はこれまで、このプロセスの自動化は危険すぎると判断していた。ミスが顧客のネットワークに影響を及ぼし、契約を失う可能性があったからだ。

エンジニアのHillel Wayneは最近、バッチアップローダーのプロジェクトで（TLA+流の）形式仕様を用い、コードを書く前にアーキテクチャのバグを発見することで納品期間を1週間短縮していた。プロジェクトマネージャーは、自動化された代替システムが安全であるために保証すべき3つの性質を定義していた。Wayneは仕様言語でシステムをモデル化し、モデルチェッカーにかけた。モデルチェッカーは仕様が許すあらゆるシナリオを網羅的にシミュレーションし、ルールを破るシナリオを見つけると具体的なトレースを返す。

2日間のモデル化の後、どの設計も即座に破綻するか、あるいは本番環境で数か月間気づかれずに潜んだ後に崩壊しうる微妙な欠陥を含んでいた。3つの必須性質のうち2つを満たす設計はあったが、3つすべてを満たすものはなかった。Wayneはいずれかを選んで願望に賭けるのではなく、プロジェクトマネージャーをモデル化の成果物に招き入れ、各設計がどのように失敗するかを具体的に示し、ビジネスがどの性質ならなくても済むかを尋ねた。

社内の設計専門家は、ある性質は常にではなく通常のみ成り立てばよいと判断した。その1つのトレードオフを絞り込むと、モデルチェッカーは複数の設計が今度は機能することを確認し、チームはそのうちの1つを構築した。自動設定サービスはその後何年も問題なく稼働し、それを構築したエンジニアたちの在職期間よりも長く続いた。

モデルチェッカーは3つのルールすべてを満たす設計が存在しないことを証明した。交渉する

仕様言語でのモデル化は捨てるのが安価である。ほとんど構築済みのコードベースはそうではない。そのため、実装前にあらゆる設計案を検証することで、無駄なエンジニアリング時間を避けられた。

モデルチェッカーは具体的な失敗トレースを返すため、抽象的なリスク警告よりも非エンジニアのステークホルダーにとって説得力がある。

コードを書く前に「これらの設計はいずれも3つの要件すべてを満たさない」ことを明らかにすることで、暗黙的で未検討だった前提が、プロジェクトマネージャーが実際に下せる明示的な決定に変わった。

試すどの設計も失敗するように見えるときは、まず設計空間を形式的にモデル化せよ。モデルチェッカーは漠然としたリスク感を、コードを書く前に提起できる具体的で交渉可能なトレードオフに変える。

自動設定管理サービスは何年にもわたり効率的に稼働し、それを構築したエンジニアたちの在職期間をはるかに超えて続いた。Wayneはその後、形式仕様のコンサルタントとしてフルタイムで働き、この実践について執筆した。その中には同主題の書籍や、Alloy仕様言語のドキュメント作成業務も含まれる。