形式手法はソフトウェアを数学的に厳密かつ安全に構築する、古くて新しい技術です。我々 SWET 第一グループは、DeNA のサービスやゲームタイトルの品質向上や開発生産性向上を目指し、これまでソフトウェアの「仕様」をメインターゲットとして形式手法の適用にチャレンジしてきました。仕様の品質を向上させることにより、設計・開発や QA などの工程で品質や生産性を向上させることができます。

本登壇では、DeNA の事業ドメインにおける形式手法の適用ノウハウや、形式手法のツールの選定や開発の経緯を紹介します。特に、並行分散システムの理論的モデルである CSP をベースとした独自ツールや、Alloy 等の既存ツールを用いた検証について扱います。それに加え、最近の取り組みとして、マイクロサービスにおけるモデリングや検証、上記の技術以外にチャレンジしていることについても紹介します。