形式手法はソフトウェアを数学的に厳密かつ安全に構築する、古くて新しい技術です。我々 SWET 第一グループは、DeNA のサービスやゲームタイトルの品質向上や開発生産性向上を目指し、これまでソフトウェアの「仕様」をメインターゲットとして形式手法の適用にチャレンジしてきました。仕様の品質を向上させることにより、設計・開発や QA などの工程で品質や生産性を向上させることができます。
本登壇では、DeNA の事業ドメインにおける形式手法の適用ノウハウや、形式手法のツールの選定や開発の経緯を紹介します。特に、並行分散システムの理論的モデルである CSP をベースとした独自ツールや、Alloy 等の既存ツールを用いた検証について扱います。それに加え、最近の取り組みとして、マイクロサービスにおけるモデリングや検証、上記の技術以外にチャレンジしていることについても紹介します。
2019年に DeNA に中途入社。SWET グループにて Go のプロダクトの自動テスト導入やソースコードの内部品質の改善を担当。 その後、SWET 1G にて形式手法に出会い、形式手法を用いたプロダクトの品質改善や開発の生産性向上に挑戦している。
2023年8月 DeNA 入社。形式手法によるソフトウェア開発に従事。キャリア初期から Web 開発とモバイル開発に携わるとともに、プログラミング言語研究者として活動した。現在はモバイルアプリへのモデルベーステストに興味をもち、実開発への適用を進めている。博士(情報科学)。
2023年 DeNA に新卒入社。学生時代は趣味でプログラミングをして遊びつつ、形式手法の研究室に所属していた。現在は SWET 1G に所属し、実課題への形式手法の適用を模索している。
