【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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

具体例: 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

なぜ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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

ボタンの無効化によるロック ハンドラは 起動しない ボタンをロック (無効化) イベントハンドラが継続 フレーム開始 フレーム開始 ボ ボ 正しく無効化 したので © DeNA Co., Ltd. 42

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

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

⽬指す姿：「画⾯」を網羅したテスト ロック漏れの検出には画⾯の網羅的な探索が必要 �� �� �� �� 進⾏不能 �� �� クラッシュ © DeNA Co., Ltd. 45

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

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

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

AnjinMBT①：状態探索によるモデル⽣成 (3) 全ての遷移の網羅的探索 未知の遷移 あり？ N End Y 画⾯認識 未タップ 有？ Y 未タップ ボタンの タップ © DeNA Co., Ltd. N 未知の遷移を ⽬指すタップ 49

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

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

AnjinMBT③：状態認識器 タップ可能ボタンを判定する既存アルゴリズムを流⽤ 参考： ● SWET2G kuniwakさんの登壇スライド ● test-helper.monkey (GitHub) l © DeNA Co., Ltd. 52

• https://speakerdeck.com/orgachem/basics-of-ugui-automation
• https://github.com/nowsprinting/test-helper.monkey/blob/master/Runtime/Monkey.cs

状態機械の保存
状態機械 〈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

AnjinMBT④：状態遷移図の⽣成 この後にデモを実施します ● 状態機械から画⾯遷移図を⽣成 ○ © DeNA Co., Ltd. 仕様書-実装のトレーサビリティ確保‧QAへの活⽤へ 54

他のアプローチ：ランダムテスト Anjin (オリジナル): 画⾯内のUI要素をランダムにタップ ボタン ‧画⾯を認識していない ‧網羅性の基準がない ボタン 💎🛍⚔💰🪛 © DeNA Co., Ltd. 55

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

デモ：AnjinMBT © DeNA Co., Ltd. 57

デモ: ⾃動⽣成された画⾯遷移図 © DeNA Co., Ltd. 58

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