[TLA+] 分散システムを設計する際に形式仕様を導入してみた
こんにちは、トレタの鄧(でん)です。
今回はトレタ社内でシステムを設計する際に導入した形式仕様(formal specification)、あるいは形式手法(formal method)についてお話したいと思います。
なぜ形式仕様が必要なのか?モバイルアプリや Web アプリ、またはマイクロサービスなどの普及により基本分散型のサービスが主流になりつつあると思いますが、その分散型のシステムを設計する際に複数のシステムの状態推移や整合性を担保するシステム設計はそのシステムの複