VDM++ 仕様を対象としたテストケース自動生成ツールBWDMの適用範囲拡大による実用性の向上

2023.3.9
宮崎大学大学院 工学研究科 工学専攻
武藤崇史

片山徹郎

目次
• 背景と目的• 拡張( i )背景と目的，手段，適用例• 拡張( ii )背景と目的，手段，適用例• 拡張( iii )背景と目的，手段，適用例

• 考察
• まとめ
• 今後の課題2

背景と目的
ソフトウェアにバグが混入する原因の一つとして，上流工程の設計段階で自然言語を一般に用いていることが挙げられる
自然言語の持つ曖昧さにより，仕様書が本来意図していない意味で捉えられてしまう

厳密な仕様を作成するために，形式手法が用いられる

3

背景と目的VDM++• 形式手法の一つにVDM(Vienna Development Method)がある• 1996年に，VDM-SLが仕様記述言語として世界初のISO標準化• VDM++はVDM-SLをオブジェクト指向拡張を施した形式仕様記述言語

本研究ではVDM++仕様記述を対象とする

4背景と目的

自然言語，あるいは形式手法を用いた設計のいずれにおいても，実装後にソフトウェアテストを行う必要がある
しかし，人手によるテストケースの設計は手間と時間がかかる

5

背景と目的テストケース自動生成ツールBWDM• 立山氏が開発したBWDM(Boundary Value/ViennaDevelopment Method)を平木場氏が拡張• VDM++仕様記述を対象に，テストケースを自動で生成する
CLIツール• Java，Kotlinで記述

6

背景と目的テストケース自動生成ツールBWDM• VDM支援ツールVDMJの字句解析機能と構文解析機能を利用する• 境界値分析，記号実行，ドメイン分析によるテストケースを生成

7

背景と目的BWDMの入出力例

入力エラーの場合は”Undefined Action”と出力する

8

背景と目的BWDMの問題点• 型定義ブロックに対応していない• 不変条件と事前条件と事後条件に対応していない• オブジェクトの状態を変更する操作定義のテストケースを 生成できない• 入れ子構造にある関数定義及び操作定義に対応していない

9

背景と目的BWDMの実用性の向上を目的に，既存のBWDMが持つ4つの問題点を解決して，BWDMの適用範囲を拡大する

10拡張
4つの問題点に対応する4つの拡張( i ) 不変条件と事前条件と事後条件の解析及び評価→不変条件と事前条件と事後条件に対応していない問題点を解決( ii ) 型定義ブロックへの対応→型定義ブロックに対応していない問題点を解決( iii )オブジェクトの状態に対するテストケース生成機能の追加→オブジェクトの状態を変更する操作定義のテストケースを生成できない問題点を解決( iv )入れ子構造にある関数定義及び操作定義への対応→入れ子構造にある関数定義及び操作定義に対応していない問題点を解決

11

拡張
4つの問題点に対応する3つの拡張( i ) 不変条件と事前条件と事後条件の解析及び評価→不変条件と事前条件と事後条件に対応していない問題点を解決→オブジェクトの状態を変更する操作定義のテストケースを生成できない問題点を解決( ii ) 型定義ブロックへの対応→型定義ブロックに対応していない問題点を解決( iii )入れ子構造にある関数定義及び操作定義への対応→入れ子構造にある関数定義及び操作定義に対応していない問題点を解決

12

拡張
拡張後のBWDMの構造

13

拡張( i )4つの問題点に対応する3つの拡張( i ) 不変条件と事前条件と事後条件の解析及び評価→不変条件と事前条件と事後条件に対応していない問題点を解決→オブジェクトの状態を変更する操作定義のテストケースを生成できない
問題点を解決14拡張( i ):背景と目的
不変条件と事前条件と事後条件に対応していない
問題点
➢不変条件
• 型定義ブロックとインスタンス変数定義ブロックに記述される• オブジェクトが存在している間，常に真となる条件式• inv (条件式) で記述される➢事前条件• 操作定義ブロックと定数定義ブロックに記述される• 操作または関数が実行される前に真となる条件式• pre (条件式) で記述される➢事後条件• 操作定義ブロックと関数定義ブロックに記述される• 操作または関数を実行した後に真となる条件式• post (条件式) で記述される15拡張( i ):背景と目的不変条件と事前条件と事後条件に対応していない問題点

事前条件を認識していないため，間違った期待出力を生成している16

拡張( i ):背景と目的オブジェクトの状態を変更する操作定義のテストケースを生成できない問題点• if-then-else式がない定義に対しては入力データを取得できず，テストケースを生成できない→分岐がなくてもオブジェクトの状態が変更する場合，テストすべき項目がある• 操作実行後のオブジェクトの状態を考慮せずにテストケースを生成している→操作の処理内容によっては，実行後のオブジェクトが不正な状態になる場合がある

17

拡張( i ):背景と目的オブジェクトの状態を変更する操作定義のテストケースを生成できない問題点• if-then-else式がない定義に対しては入力データを取得できず，テストケースを生成できない→分岐がなくてもテストすべき場合がある• 操作実行後のオブジェクトの状態を考慮せずにテストケースを生成している→操作の処理内容によっては，実行後のオブジェクトが不正な状態になる場合がある操作後に検証すべき条件式がある

18

拡張( i ):手段
不変条件と事前条件と事後条件の解析及び評価• VDM++仕様では，不変条件と事前条件と事後条件の3種類の条件式を設定できる• 操作実行後のオブジェクトの状態を算出し，3種類の条件式に適用した際の真偽値を求めて，表示する期待出力を決定する
表示する期待出力該当する条件return文の結果

3種類の条件式を全て充足し，正常に出力できる

Input Error

事前条件もしくは引数の制約条件を充足しない

Failureー

事後条件か，インスタンス変数の制約条件か，戻り値の制約条件のいずれかを充足しない
3種類の条件式を全て充足するが，出力がない

19

拡張( i ):手段
不変条件と事前条件と事後条件の解析及び評価
引数「金額」が1000の時• カード利用額 = 1000 (0 + 1000)• 保有ポイント = 710 (700 + 1000 div 100)0 <= 710 <= 4294967294

0 <= 1000 <= 4294967294
1000 <= 100000
1000 >= 1000

3種類の条件式を全て充足するが，出力がないため，期待出力は「ー」となる

20

拡張( i ):手段
不変条件と事前条件と事後条件の解析及び評価
操作後に検証すべき条件式の境界値を取るための入力値を算出する• 操作後に検証すべき条件式中のインスタンス変数を，操作の式に置換して境界値を求める
0 + 金額 <= 100000
操作前のカード利用額 カード利用限度額→金額の入力値(100000と100001)を取得※入力値は記号実行を用いて取得する

21

拡張( i ):適用例
VDM++仕様

拡張後のBWDMに適用した際の出力22拡張( i ):適用例
VDM++仕様

拡張後のBWDMに適用した際の出力

操作前・操作後ともに正常であるため，期待出力を「ー」としている（return文がある場合は，その結果を期待出力とする）

23

拡張( i ):適用例
VDM++仕様

拡張後のBWDMに適用した際の出力

事前条件か引数の制約条件を充足しないため，期待出力を「Input Error」としている

24

拡張( i ):適用例
VDM++仕様

拡張後のBWDMに適用した際の出力不変条件を充足しないため，期待出力を「Failure」としている

25

拡張( ii )4つの問題点に対応する3つの拡張( ii ) 型定義ブロックへの対応→型定義ブロックに対応していない問題点を解決

26

拡張( ii ):背景と目的型定義ブロックに対応していない問題点「月」型は1~12の自然数• 型定義ブロック(types)で定義されている型が，どのような型であるか特定できない• 型の境界値を入力とするテストケースを生成できない「月」型の境界値➢nat1型における境界値 :0, 1, 4294967295, 4294967296➢不変条件における境界値 :12, 1327

拡張( ii ):背景と目的型定義ブロックに対応していない問題点
型を特定できていない

既存のBWDMに適用した際の出力28拡張( ii ):手段

既存の構文解析部の抽象構文木解析• 関数定義を表すクラスには定数定義リストをメンバに持たせる

構文解析処理により定義の抽象構文木を抽出
抽象構文木が定数定義であれば• 操作定義を表すクラスには定数定義リストとインスタンス変数定義リストをメンバに持たせる
定数定義
リストに格納抽象構文木がインスタンス変数定義であればインスタンス変数定義
リストに格納抽象構文木が関数定義であれば抽象構文木が操作定義であればテストケース生成対象となる関数定義を表すクラスのインスタンスを生成

関数定義
リストに格納テストケース生成対象となる操作定義を表すクラスのインスタンスを生成

操作定義
リストに格納29

拡張( ii ):手段

既存の構文解析部の抽象構文木解析• 型定義リストをメンバに持たせる

構文解析処理により定義の抽象構文木を抽出• 型定義ブロック以外では型定義を識別できないため，型定義リストを基に実際の型に書き換える
抽象構文木が定数定義であれば定数定義
リストに格納抽象構文木がインスタンス変数定義であればインスタンス変数定義
リストに格納抽象構文木が関数定義であれば抽象構文木が操作定義であればテストケース生成対象となる関数定義を表すクラスのインスタンスを生成

関数定義
リストに格納テストケース生成対象となる操作定義を表すクラスのインスタンスを生成

操作定義
リストに格納抽象構文木が型定義であれば型定義
リストに格納30

拡張( ii ):手段

型定義の不変条件に対する境界値生成
引数型に「月」型を使用している場合，この式の境界値も生成する• BWDMはif-then-else式の条件式を境界値分析部に渡して，入力データとなる境界値を生成する• 引数型に不変条件がある場合，if-then-else式の条件式と同様に不変条件の条件式も境界値分析部に渡す31

拡張( ii ):適用例
拡張後のBWDMに適用した際の出力の一部

VDM++仕様32

拡張( ii ):適用例
拡張後のBWDMに適用した際の出力の一部

VDM++仕様「年」型と「月」型がそれぞれnat型，nat1型だと特定できている33

拡張( ii ):適用例
拡張後のBWDMに適用した際の出力の一部

VDM++仕様に対応したテストケースを生成している34

拡張( iii )4つの問題点に対応する3つの拡張( iii )入れ子構造にある関数定義及び操作定義への対応→入れ子構造にある関数定義及び操作定義に対応していない問題点を解決

35

拡張( iii ):背景と目的入れ子構造にある関数定義及び操作定義に対応していない問題点• 定義の中で別の関数定義や操作定義を呼び出す場合がある• if-then-else式の中で関数定義や操作定義を呼び出していると，入力値の取得や期待出力の導出ができない

36

拡張( iii ):背景と目的入れ子構造にある関数定義及び操作定義に対応していない問題点• 定義の中で別の関数定義や操作定義を呼び出す場合がある• if-then-else式の中で関数定義や操作定義を呼び出していると，入力値の取得や期待出力の導出ができない37

拡張( iii ):背景と目的
入れ子構造にある関数定義及び操作定義に対応していない問題点• return文で関数定義や操作定義を呼び出していると，return文の処理をそのまま期待出力として表示してしまう

38

拡張( iii ):手段
入れ子構造にある関数定義及び操作定義への対応
入れ子構造にある条件式から境界値（入力値）を取得する
1. 対象とする条件式に到達するための条件式を全て抽出する
2. 呼び出している定義の結果を求める条件式を生成する
3. 1.と2.の条件式を前提条件として，対象とする条件式の境界値を求める

39

拡張( iii ):手段
入れ子構造にある関数定義及び操作定義への対応
入れ子構造にある条件式から境界値（入力値）を取得する
1. 対象とする条件式に到達するための条件式を全て抽出する
引数の制約条件と事前条件を抽出する• テスト点 >= 0
• テスト点 <= 4294967294• テスト点 <= 10040

拡張( iii ):手段
入れ子構造にある関数定義及び操作定義への対応
入れ子構造にある条件式から境界値（入力値）を取得する
2. 呼び出している定義の結果を求める条件式を生成する
呼び出している定義の結果と，そこに到達するための条件式を結合する• ボーダーラインを取得() = 70 and 70 < 60

• ボーダーラインを取得() = 60 and 70 >= 60
平均点

複数ある場合は，orで結合する(ボーダーラインを取得() = 70 and 70 < 60) or(ボーダーラインを取得() = 60 and 70 >= 60)

41

拡張( iii ):手段
入れ子構造にある関数定義及び操作定義への対応
入れ子構造にある条件式から境界値（入力値）を取得する
3. 1.と2.の条件式を前提条件として，対象とする条件式の境界値を求める
1.と2.で取得した前提条件• テスト点 <= 100• テスト点 >= 0
• テスト点 <= 4294967294• (ボーダーラインを取得() = 70 and 70 < 60) or(ボーダーラインを取得() = 60 and 70 >= 60)

前提条件よりボーダーラインを取得()の結果が60となるため，テスト点の境界値59と60が求められる

42

拡張( iii ):手段
入れ子構造にある関数定義及び操作定義への対応
入れ子構造にある定義の期待出力を決定する
if-then-else式中に関数定義や操作定義が呼び出されている場合，その定義の木構造に入力値を適用して，実行フローを特定する
特定した実行フローのreturn文で関数定義もし
くは操作定義が呼び出されている場合，その定義の木構造を基に，期待出力を決定する

43

拡張( iii ):適用例
VDM++仕様

拡張後のBWDMに適用した際の出力44拡張( iii ):適用例
VDM++仕様

拡張後のBWDMに適用した際の出力入れ子構造にある条件式から境界値（入力値）を取得している

45

拡張( iii ):適用例
VDM++仕様

拡張後のBWDMに適用した際の出力

呼び出し先の操作定義の出力を期待出力としている

46

考察:人手によるテストケース作成との比較
入れ子構造にある定義を含む
VDM++仕様書
人手による作成

テストケース

拡張後のBWDMによる生成

テストケース

拡張後のBWDMに新たに適用可能となったVDM++仕様から
人手によってテストケースを作成する時間と拡張後のBWDMに適用してテストケースを生成する時間を比較する

47

考察:人手によるテストケース作成との比較

実験結果
人手によるテストケース作成時間
被験者

作成時間

被験者A

12m 38s

人手とBWDMの比較

被験者B

10m 54s

時間

被験者C

8m 33s

被験者8人の平均

被験者D7m 04s

BWDM

被験者E

8m 50s

被験者F

8m 02s

被験者G

7m 43s

被験者H

9m 59s

9m 12s1.3s

人手によるテストケース作成の平均時間に比べて，拡張後のBWDMを使用した場合は，9分程度（約99.76%）の時間短縮が確認できた
また，人手による作成ではヒューマンエラーも見られた

48

考察:関連研究との比較
Aamer Nadeem 氏らの研究*• VDM++仕様を対象にしたテストケース自動生成手法の提案• 不変条件と事前条件を同値分割して，有効な入力空間からランダムに決定した代表値を入力データとする• メソッド呼び出しの有効な手順を記述した仕様を用意して，テストシーケンスを生成する
BWDMはVDM++仕様のみを用意すればテストケースを生成できる．また，
BWDMで生成するテストケースは，境界値テスト，ドメイン分析テストで使用でき，記号実行により境界値分析ではカバーできない実行フローに対するテストも期待できる．さらにオブジェクトに影響を及ぼすメソッドに対して，オブジェクトの状態のテストを実施できる．
*Aamer Nadeem, Muhammad Jaffar-Ur-Rehman. Automated Test Case Generation from IFAD VDM++ Specifications.
SEPADS 05: 4th WSEAS International Conference on Software Engineering, Parallel & Distributed Systems, No.28, pp.1-7, 2005.

49

まとめ
◼ 目的
BWDMの実用性の向上◼ 手段• 不変条件と事前条件と事後条件の解析及び評価• 型定義ブロックへの対応• 入れ子構造にある関数定義及び操作定義への対応◼ 結論
BWDMに3つの拡張を施したことにより，既存の4つの問題点を解決し，適用範囲が拡大した
また，BWDMに新たに適用可能となったVDM++仕様においても，テストケース生成に要する時間を9分程度（約99.76%）短縮でき，ヒューマンエラーを除去できることを確認できた

したがって，拡張後のBWDMの実用性が向上し，BWDMを使用した場合のテスト工程の作業効率が向上した

50

今後の課題• 整数型以外の型への対応
拡張後のBWDMでは，int型とnat型とnat1型のみに対応可能であり，それ以外のreal型やrat型などの型に対応していないため，対応が必要である• 再帰構造にある関数定義及び操作定義への対応
拡張後のBWDMでは，操作及び関数呼び出しが含まれる定義のテストケースを生成する際に，呼び出し先の定義の抽象構文木解析処理を終えていない場合，テストケースを生成できず，再帰構造にある関数及び操作定義のテストケースを生成できため，対応が必要である• 操作後の値を参照する条件式への対応
拡張後のBWDMでは，操作後の値を参照する条件式に対する境界値を取得することができないため，対応する必要がある☝現在は拡張( i )のオブジェクトの状態に対応したテストケース生成により対応済み

51