【DeNATechCon2024】SWET流！形式手法によるDeNAプロダクト品質改善の秘訣

SWET 流！形式⼿法による DeNA プロダクト品質改善の秘訣品質本部品質管理部SWET第⼀グループ Akito Ito / Keigo Imai / Junya Shijubo © DeNA Co., Ltd.

全体のアウトライン ● 前半 ○ SWET1Gの紹介 ○ CSPベースの形式仕様記述の紹介 ○ まとめとそこから得られた知⾒ ● 後半 ○ 形式⼿法アプローチによるUnityゲーム⾃動テストの事例 © DeNA Co., Ltd. 2

⾃⼰紹介伊藤瑛 Akito Ito 2019年に中途⼊社、SWETに配属。当初はGoのプロダクトの品質改善を担当。 2021年ごろから形式⼿法を学び始める。以降、複数のプロダクトへ、形式⼿法の適⽤を通じた品質改善を⾏っている。 2023年よりSWET 1G グループリーダー © DeNA Co., Ltd. 3

4.

SWET1Gの紹介 ● ソフトウェア開発における仕様起因の問題を技術で解決することで開発⽣産性向上を達成することがミッション © DeNA Co., Ltd. 4

5.

SWET1Gの紹介 ● ソフトウェア開発における仕様起因の問題を技術で解決することで開発⽣産性向上を達成することがミッション仕様起因の問題とは？ DeNAのシステムは仕様を正しく書き切ることが難しい。運⽤が重なるにつれ、仕様不備が⽋陥の⽀配的な要因になる。詳しくは過去のTechConを参照 https://www.slideshare.net/dena_tech/dena-techcon-2020-230 372486 © DeNA Co., Ltd. 5

https://www.slideshare.net/dena_tech/dena-techcon-2020-230372486

6.

SWET1Gの紹介 ● ソフトウェア開発における仕様起因の問題を技術で解決することで開発⽣産性向上を達成することがミッション技術とは？形式⼿法、特に形式仕様記述を使う © DeNA Co., Ltd. 6

7.

形式仕様記述の紹介 ● システムの仕様を形式⾔語で記述する ○ 形式⾔語 = 数理論理学に基づく明確で厳密な意味をもつ特定の形式、構⽂のこと ● 形式が決まっているため、⾃然⾔語や⾃由な図形で仕様を書く場合に⽐べ、記述漏れや曖昧さを排除できる ● ⼀部のツールを⽤いることにより、記述した仕様に対して検査が可能になる © DeNA Co., Ltd. 7

8.

SWET1Gの紹介 ● ソフトウェア開発における仕様起因の問題を技術で解決することで開発⽣産性向上を達成することがミッション仕様起因の問題とは？技術で解決とは？ DeNAのシステムは仕様を正しく書き切ることが難しい。運⽤が重なるにつれ、仕様不備が⽋陥の⽀配的な要因になる。形式仕様記述を使う。 © DeNA Co., Ltd. 8

9.

SWET1Gで⾏っている施策の⼀部の紹介 ● 分散システムにおけるCSPを⽤いた形式仕様記述の紹介を⾏います。 ● どういうことをやっているのかを⼩さい例をもとに紹介します。 ● この事例の説明を通じ、CSPや形式仕様記述の効果について認識していただくことを⽬的としています。 © DeNA Co., Ltd. 9

10.

CSPをベースにした形式仕様記述 ● CSPとは ○ Communicating Sequential Processは並⾏システムを厳密に記述するため理論 ○ 1978年にC.A.R.Hoareが考案したプロセス理論 ● システムの振る舞いを「相互作⽤」に注⽬することにより形式化する © DeNA Co., Ltd. 10

11.

なぜ分散システムで形式⼿法を使うのか ● 分散システム ○ 複数のシステムが相互に通信を⾏い機能を提供するシステム ○ 複数のシステムがそれぞれの独⽴した状態を持つシステム ● それぞれのサブシステムの状態や通信の順番により、組み合わせが莫⼤な数になり、仕様を書き切るのが難しい © DeNA Co., Ltd. 11

12.

なぜ分散システムで形式⼿法を使うのか ● A, B, C相互に通信を⾏うようなシステム ● parで囲われている通信は並列で発⽣する ● 例えば ③ -> ④ -> ⑤ -> ⑥ -> ⑦ -> ⑧ ③ -> ⑦ -> ④ -> ⑧ -> ⑤ -> ⑥ ● 通信の順番が⼊れ替わったときの仕様の組み合わせは膨⼤な数になる © DeNA Co., Ltd. 12

13.

なぜ分散システムで形式⼿法を使うのか ● A, B, C相互に通信を⾏うようなシステム ● parで囲われている通信は並列で発⽣する ● 例えば 1 2 ③ -> ④ -> ⑤ -> ⑥ -> ⑦ -> ⑧ 3 ③ -> ⑦ -> ④ -> ⑧ -> ⑤ -> ⑥ ● 4 通信の順番が⼊れ替わったときの仕様の 5 組み合わせは膨⼤な数になる © DeNA Co., Ltd. 6 13

14.

なぜ分散システムで形式⼿法を使うのか ● A, B, C相互に通信を⾏うようなシステム ● parで囲われている通信は並列で発⽣する ● 例えば 1 3 ③ -> ④ -> ⑤ -> ⑥ -> ⑦ -> ⑧ 5 ③ -> ⑦ -> ④ -> ⑧ -> ⑤ -> ⑥ ● 6 通信の順番が⼊れ替わったときの仕様の 2 組み合わせは膨⼤な数になる © DeNA Co., Ltd. 4 14

15.

具体例 ● オーソリトランザクション機能 ● 銀⾏やクレジットカードなどの決済を⾏うときに、対象のユーザが⽀払い能⼒があるかどうかを確かめ、残⾼を確保する。確保した残⾼に対して実際の引き落としを⾏う機能。 © DeNA Co., Ltd. 15

16.

シナリオの解説 ● スマホアプリ内から商品を購⼊する状況 item service bank service ● 商品を管理するitem serviceとアプリ内通貨を管理するbank serviceが別個に存在 ● アプリから商品を購⼊する際は、 client item service経由でbank service に問い合わせる © DeNA Co., Ltd. 16

17.

SWET1GにおけるCSPでの形式仕様記述化の⼯程 1. システムの構成要素を考える (今回は割愛) 2. システムの構成要素同⼠がどう通信をしたらよいかを考える 3. それぞれのサブシステムが通信に対してどう振る舞うかを考える 4. それぞれのサブシステムの仕様を別個にコード化し、合成してシステム全体の仕様をシミュレーション‧検査する © DeNA Co., Ltd. 17

18.

SWET1GにおけるCSPでの形式仕様記述化の⼯程 1. システムの構成要素を考える (今回は割愛) 2. システムの構成要素同⼠がどう通信をしたらよいかを考える 3. それぞれのサブシステムが通信に対してどう振る舞うかを考える 4. それぞれのサブシステムの仕様を別個にコード化し、合成してシステム全体の仕様をシミュレーション‧検査する © DeNA Co., Ltd. 18

19.

具体例: シーケンス図 ● シーケンス図を考えてシステム同⼠の通信がどう⾏われたら良いのかを考える ● 通信の名前と通信によって何を送受信するのかも考え、ラフにシーケンス図に書いておく © DeNA Co., Ltd. 19

20.

SWET1GにおけるCSPでの形式仕様記述化の⼯程 1. システムの構成要素を考える (今回は割愛) 2. システムの構成要素同⼠がどう通信をしたらよいかを考える 3. それぞれのサブシステムが通信に対してどう振る舞うかを考える 4. それぞれのサブシステムの仕様を別個にコード化し、合成してシステム全体の仕様をシミュレーション‧検査する © DeNA Co., Ltd. 20

21.

具体例: 状態遷移図 ● 通信に注⽬して状態を切り出す ● 通信によって状態遷移が発⽣すると考える ● シーケンス図のメッセージの送信‧受信で状態が区切られると考える © DeNA Co., Ltd. 21

22.

具体例: 状態遷移図 ● item serviceを状態遷移図にすると以下のようになる ● この状態遷移図を全てのコンポーネントについて記述する © DeNA Co., Ltd. 22

23.

状態遷移図の書き⽅ ● incrementというイベントでcounterが1増える状態遷移図は以下のようになるイベント名 (シーケンス図より) 状態変数の定義 © DeNA Co., Ltd. 状態変数の変化 23

24.

SWET1GにおけるCSPでの形式仕様記述化の⼯程 1. システムの構成要素を考える (今回は割愛) 2. システムの構成要素同⼠がどう通信をしたらよいかを考える 3. それぞれのサブシステムが通信に対してどう振る舞うかを考える 4. それぞれのサブシステムの仕様を別個にコード化し、合成してシステム全体の仕様をシミュレーション‧検査する © DeNA Co., Ltd. 24

25.

CSPによるモデル化 ● CSP専⽤⾔語は(まだ)⽤いていない参考: CSPだと前述のserverはこう書くことができる SERVER = purchase?amount -> authorize!amount -> authorizeOk?txid -> commit!txid -> …. ● 独⾃ツールを実装し、OCaml上でCSPのモデルが記述できるように環境を整備している ● CSPのモデルはそれぞれのサブシステムごとに実装し、合成を⾏う © DeNA Co., Ltd. 25

26.

[beta]

具体例: OCamlのモデル (遷移関数)
●

状態遷移図を遷移関数に書き写していく

●

遷移関数とは、現在の状態を引数に発⽣しうる遷移を計算する関数

let server_transf (state : server_state) =
match state with
……
| S4 { items; txId } ->
[
Recv
( CH_CommitOK txId,
guard_true,
fun _ (CommitOK { txId }) ->
S5 { txId; items = newItem () :: items }
);
]
| S5 { items } -> [ Ev (PurchaseOK, S0 { items }) ]
© DeNA Co., Ltd.

26

27.

なぜOCamlなのか ● CSPを直接記述できるツールはあるが⾃作している ● OCamlはSWET1Gで利⽤してきた実績があり、既存の資産があるので採⽤している ● OCamlのCSPのモデルについてより詳しく知りたい⽅は https://swet.dena.com/entry/2022/04/04/135152 を参照してください © DeNA Co., Ltd. 27

https://swet.dena.com/entry/2022/04/04/135152

28.

モデルの合成 ● それぞれのサブシステムの遷移関数 item service を合成して、システム全体の遷移関数を計算できる (=並⾏合成) ● 複数のモデルを同時に遷移させる bank service ような仕組み © DeNA Co., Ltd. 28

29.

合成したモデルのシミュレーションそれぞれの通信が発⽣した直後の各サブシステムの状態を観察できる © DeNA Co., Ltd. 29

30.

モデル検査‧リファインメント検査 ● 実装したモデルを使って、網羅的な探索ができる ○ ○ モデル検査 ■ システムのとりうる状態を全て探索し、許容されない状態がないかを検査する ■ e.g. 決済は実⾏されたがアイテムが付与されていない状態はないかの検査リファインメント検査 ■ © DeNA Co., Ltd. モデル同⼠が同じ振る舞いをするかを検査できる 30

31.

CSPにおける形式仕様化の効果と考察 ● それぞれのサブシステムの状態や通信の順番により、組み合わせが莫⼤な数になり、仕様を書き切るのが難しい => それぞれのサブシステムの遷移を定義し、合成することによりシステム全体の振る舞いを調べることが可能に ● 状態遷移図の効果 => それぞれのサブシステムがどのタイミングでどの通信を⾏いどのデータを更新するのかが明確になる © DeNA Co., Ltd. 31

32.

まとめ ● SWET 1Gの紹介 SWET1Gは仕様に関する問題を形式⼿法を使って解決するグループ ● CSPの施策の紹介分散システムにおける難しさ、CSPのモデル化のプロセス、 CSPのモデル化の効果 © DeNA Co., Ltd. 32

33.

後半の話題：モデルベーステストによるアウトゲームテスト⾃動化形式仕様に基づいたUnityゲームGUIの網羅的テスト © DeNA Co., Ltd. 33

34.

⾃⼰紹介今井敬吾 Keigo Imai 四⼗坊純也 Junya Shijubo © DeNA Co., Ltd. 2023年8⽉ DeNA ⼊社。形式⼿法によるソフトウェア開発に従事。キャリア初期から Web 開発とモバイル開発に携わるとともに、プログラミング⾔語研究者として活動した。現在はモバイルアプリへのモデルベーステストに興味をもち、実開発への適⽤を進めている。博⼠(情報科学) 2023年 DeNA に新卒⼊社。学⽣時代は趣味でプログラミングをしつつ、形式⼿法分野の研究室に所属していた。現在は SWET 1G に所属し、実課題への形式⼿法の適⽤を模索している。 34

35.

モバイル(2D)ゲームの構成：インゲームとアウトゲームインゲーム (GUI) アウトゲーム (GUI) ゲームの「ガワ」パズルゲームのパズル部分インゲーム (ロジック) アウトゲーム (ロジック) アイテム、ソーシャル、課⾦などモバイルゲーム全体の構成 © DeNA Co., Ltd. 35

36.

モバイル(2D)ゲームの構成：インゲームとアウトゲーム今回のターゲットインゲーム (GUI) パズルゲームのパズル部分インゲーム (ロジック) アウトゲーム GUI アウトゲーム (ロジック) ゲームの「ガワ」アイテム、ソーシャル、課⾦などモバイルゲーム全体の構成 © DeNA Co., Ltd. 36

37.

アウトゲームGUIの特徴アウトゲームGUI 並⾏性をもつ簡単な操作(タップ) 演出効果ウィンドウ、ボタン、スクロールバーサウンド＆ビジュアル、1フレーム毎の制御エンバグの可能性がある多数の（変更されやすい）画⾯キャラ編成、アイテム購⼊、ショップ、ソーシャルなどの作り込み © DeNA Co., Ltd. 37

38.

アウトゲームGUIと並⾏性：あるべき姿ボタン等のUIはタップ直後にロックする。さもなくば… 無効化する ⏳ ボタンタップ © DeNA Co., Ltd. （タップに反応しない）ボタン 1F(フレーム)後 38

39.

アウトゲームGUIにおけるバグの例：ロック漏れ⽛をむく並⾏性：連続タップで容易にクラッシュしてしまう無効化されていないボタンタップクラッシュボタン 1F タップ 1F 1F(フレーム)後再タップできてしまうと © DeNA Co., Ltd. 39

40.

なぜクラッシュするか：ロックしなくてよいケースイベントハンドラが1フレームで完了する場合は、連続タップしても問題ないイベントハンドラ実⾏フレーム開始フレーム開始ボ © DeNA Co., Ltd. ボ 40

41.

なぜクラッシュするか：ロック漏れでクラッシュするケースハンドラのasync/awaitでクラッシュの余地が⽣まれる 2回目のハンドラが並列に起動 await UniTask.Delay() async/awaitでハンドラが継続フレーム開始フレーム開始ボボ（async/awaitの場合、厳密には同時に実⾏されることはないが、想定外の結果を⽣むことが多い） © DeNA Co., Ltd. 41

42.

43.

他の例：タッチガードによるGUIロック半透明なオブジェクトでタッチ不可領域を覆う⼿法他の部分はロックタップさせない ‹ホーム画⾯› ‹ホーム画⾯› タップを誘導 💎🛍⚔💰🪛 元の画⾯ © DeNA Co., Ltd. タッチガード 💎🛍⚔💰🪛 (タップを吸収する図形) 43

44.

タッチガードの「遅れ」による進⾏不能バグ例：ゲームの「ホーム画⾯」におけるメニュータップタップさせない ‹バトル画面› 消えない ‹バトル画面› タッチガードが遅れて出現 ⚔ 意図せず有効なボタン ⚔ 進⾏不能 💎🛍⚔💰🪛 タッチガードが間に合っていない © DeNA Co., Ltd. 意図しない画⾯遷移 44

45.

46.

あんじんえむびーてぃ AnjinMBT：SWET製 Unityモデルベーステストツール ● モデルベーステスト (Model Based Testing; MBT)：状態遷移モデルに基づくテスト* ● Unity アウトゲームGUI の網羅的実⾏を中⼼とした、様々な機能をもつ AnjinMBT 実⾏の概略モデルに基づく網羅的テスト状態機械 (≒画⾯遷移図) に基づく実⾏モデル⾃動テストアウトゲームGUI ⾃動⽣成状態探索によるモデル⽣成(保存) © DeNA Co., Ltd. アウトゲームGUIのモデル *世の中には他のモデルに基づくMBTもある。 46

47.

AnjinMBT①：状態探索によるモデル⽣成 (1) Unityゲームの⾃動実⾏により状態機械を構築未知の遷移先* (例) ‹ショップ画面› ボタン等のUI = 遷移買いにきた買いにきたショップ画⾯売りにきた売りにきた画⾯ = 状態 * 遷移先が未知である場合は空の状態集合∅を割り当てる：δ(ショップ画⾯,買いにきた)=∅ © DeNA Co., Ltd. 47

48.

AnjinMBT①：状態探索によるモデル⽣成 (2) テスト実⾏中の状態機械更新例：「買いにきた」ボタンを(⾃動)タップ新しく発⾒した状態ひのきのぼう ‹アイテム購⼊画⾯› ‹ショップ画⾯› アイテム購⼊タップ買いにきた売りにきた買いにきたひのきのぼう時間経過どうのつるぎどうのつるぎショップ画⾯売りにきた新しい画⾯を発⾒ © DeNA Co., Ltd. 48

49.

50.

AnjinMBT②：状態遷移に基づく実⾏モデル ● 画⾯遷移を状態機械 〈S, s0, A, δ〉 とみなしてモデル化例: ログインダイアログの状態機械 δ0 = { (s0,input, {s0}), (s0,login, {s1}), (s1,logout, {s0}), (s1,conﬁrm, {s2}) ここで状態(画⾯)の集合 S アクション集合 A 〈{s0, s1, s2}, s0, {input,login,logout,conﬁrm}, δ0〉 遷移関係 δ : S x A x P(S) 初期状態 s0∈S login input グラフィカルな表現 s0 s1 logout © DeNA Co., Ltd. } confirm s2 50

51.

AnjinMBT③：状態認識器 Unityのシーン階層から操作可能なボタンを列挙ウィンドウ名= 状態名* GameObject名 =アクション名 Tap, ok_btn.MyWindow.Canvas.SampleScene MyWindow Tap, cancel_btn.MyWindow.Canvas.SampleScene l ボタンを⼀意に特定するパスを付与** *社内FWの慣習を採⽤。他のポリシーも可能(アクション集合など) © DeNA Co., Ltd. **UI要素を⼀意に特定できる⽂字列であればよい 51

52.

53.

[beta]

状態機械の保存
状態機械 〈S, s0, A, δ〉をJSONフォーマットで保存
{

© DeNA Co., Ltd.

初期状態 (s0): 特別な状態 <init> とした
"initial": "<init>",
"states": [
"<init>",
状態集合 S
"MyWindow"
],
遷移関係 δ
"transitions": [
{
"src": "<init>",
"step": "<no_event>,<initial_action>",
"dest": [
"MyWindow"
]
},
遷移前画面
{
タップしたボタン
"src": "MyWindow",
"step": "Tap,ok_btn.MyWindow.Canvas.SampleScene",
"dest": [ "NextWindow" ]
遷移後画面

53

54.

55.

56.

他のアプローチ：モデル検査 ● 例：書籍「SPINモデル検査」 (中島震, 近代科学社, 2008) ● Javaプログラムを SPIN (Promela⾔語) でモデル化いつまで経っても検査が完了しない検証 (モデル検査) フィードバック‧修正 ‧モデル化のコストモデル (Promela) コード (Java) ‧追従のコスト ‧状態数爆発モデル化頻繁に変更がある © DeNA Co., Ltd. モデル化が⼤変 56

57.

58.

59.

まとめ ● アウトゲームGUIにおける並⾏バグ ○ 教科書的な形式⼿法の適⽤が難しい領域 ● AnjinMBT によるモデルベーステスト © DeNA Co., Ltd. ○ 画⾯を認識して、UI操作を⾃動実⾏ ○ 画⾯遷移からモデル（状態機械）を⾃動⽣成 ○ モデルに基づいた網羅的‧探索的なテスト 59

【DeNATechCon2024】SWET流！形式手法によるDeNAプロダクト品質改善の秘訣

DeNA_Tech

関連スライド

ディメンショナルモデルの実導入と実装について

GraphQLやるならDataloaderを使おう

【DeNATechCon2024】新卒がソロでatmaCup 優勝&Kaggle 金メダル獲得した時の取り組み

【DeNATechCon2024】未来医療の革新 AIを活用した医療情報の効率的構造化

テクノロジーレポート AI / データ活用編

【DeNATechCon2024】CI/CD の課題解消！ GitHub Actions への移行で可能になったこと

各ページのテキスト