スライド - アーキテクチャ指向形式手法に基づく高品質ソフトウェア開発法

「形式手法とテスト」
宮崎大学 工学教育研究部
⽚⼭徹郎
<[email protected]>
Part 1
2015/02/20
JaSST東京2015＃D2
2
テストに必要な情報って？
• 「仕様が曖昧だからテストが大変！」
– 仕様に何を求めてますか？
つまり
• テスト技術者にとって、どういう仕様が望まし
いのか？
それを考える前に
• テストに必要な情報って？
– テストベース
2015/02/20
JaSST東京2015＃D2
3
テストベース
• テストに必要な情報をテスト技法で考える
同値分割法
ソフトウェアやシステムへの入力を、同じ処理をする
グループに分割するための情報
境界値分析
さまざまな境界となる値
デシジョンテーブルテスト
条件、条件の組み合わせ、動作(結果)
状態遷移テスト
状態、状態の前後の条件、状態間の遷移、イベント
(入力)
ユースケーステスト
アクター(ユーザ、システム)、アクターとシステムとの
相互作用(シナリオ)、事前条件、事後条件
制御パステスト
ソースコード (テスト結果の判定の際に仕様)
オールペアテスト
(ペアワイズテスト)
因子、水準、禁則
エラー推定
過去のバグ情報
2015/02/20
JaSST東京2015＃D2
4
テストベース
• テストに必要な情報をテストレベルで考える
コンポーネントテスト
コンポーネント要件、詳細設計、ソースコード (スタブ、ド
ライバ、シミュレータ)
統合テスト
ソフトウェア設計もしくはシステム設計、アーキテクチャ、
ワークフロー、ユースケース
システムテスト
システム要求仕様もしくはソフトウェア要求仕様、ユース
ケース、機能仕様 (リスク分析レポート)
受け入れテスト
ユーザ要件、システム要件、ユースケース、ビジネスプロ
セス、リスク分析レポート
2015/02/20
JaSST東京2015＃D2
5
テストと仕様の関係
• テストに必要な情報は、実施するテストによっ
て、さまざま
つまり
• テストに必要な情報を、すべて仕様から取れ
るわけではない。
一方で
• 仕様から取れる情報が多いのは事実
– 曖昧でない仕様であれば、テストに必要な情報を
短時間で多く取れるかも？
2015/02/20
JaSST東京2015＃D2
6
Part 2
2015/02/20
JaSST東京2015＃D2
7
理想の仕様を考えてみよう！
• 「Myersの三角形判定問題」の仕様を考えてみる
– 資料を配布します
– この資料は、セッション終了後に回収します。
• テスト技術者が考える仕様のあり方について、今後の検
討材料とさせていただきます。ご協力をお願いします。
2015/02/20
JaSST東京2015＃D2
8
「Myersの三角形判定問題」
• 問題
(「ソフトウェア・テストの技法 第２版」Glenford J.Myers, Tom Badgett, Todd M.Thomas,
Corey Sandler著, 長尾真監訳, 松尾正信訳, 近代科学社, ISBN4-7649-0329-6より)
– 以下のプログラムをテストするのに充分と思われる
一連のテストケースを書いてください。
「このプログラムでは、ユーザが3つの整数を入力します。
この3つの値は、それぞれ三角形の3辺の長さを表すものと
します。プログラムは、三角形が、不等辺三角形、二等辺三
角形、正三角形のうちのどれであるかを決めるメッセージを
出力します。」
2015/02/20
JaSST東京2015＃D2
9
「Myersの三角形判定問題」
• 解答
1.
2.
3.
4.
5.
6.
7.
有効な不等辺三角形
有効な正三角形
有効な二等辺三角形
3.の順列組み合わせ
1つが0
1つが負
2つの和がそれ以外の1つ
と等しい
8.
9.
10.
11.
12.
13.
7.の順列組み合わせ
2つの和がそれ以外の1つより
小さい
9.の順列組み合わせ
すべて0
整数ではない値
数値の個数が間違っている
14. 上記それぞれについて、予想
される出力を示したか
※ただし、この解答は、Myersの著書における解答
2015/02/20
JaSST東京2015＃D2
10
理想の仕様を考えてみよう！
– 以上が、Myersの三角形判定問題で、仕様からテス
トケースを作成する難しさが理解できる問題になって
います。
• でもこの問題は、仕様の書き方にも問題があると思いま
せんか？
1. あなたは、この14個の解答を得るための仕様はど
のように書いてあったらいいと思いますか？
2. あなたが、仕様に求める情報や条件は何ですか？
2015/02/20
JaSST東京2015＃D2
11
Part 3
2015/02/20
JaSST東京2015＃D2
12
VDM++仕様を用いた
デシジョンテーブル自動生成ツールVDTableの開発
• 目的
– デシジョンテーブルの作成には、手間と時間がかかる
• 仕様の記述内容の理解(論理関係の把握)
• 条件と動作の抽出
– 形式手法を用いたテスト設計時の作業効率化
VDM + Decision Table
VDM++
仕様
2015/02/20
JaSST東京2015＃D2
デシジョン
テーブル
13
VDTableの流れ
VDM++
仕様
Parser
VDMJ
Converter
DTGenerator
デシジョン
テーブル
解析用内部表現データ
条件
構文解析
データ
事前条件
事後条件
モジュール
2015/02/20
JaSST東京2015＃D2
動作
真理値
14
構文解析データ
• 抽象構文木をもとに出力したデータ
#access
private
#location
in '/Users/katlab/Documents/workspace/VDMDT/data/Sample.vdmpp' at line 4:3
#name
revBin2dec
#type
(seq of (nat) -> nat)
#kind
explicit function
#body
private revBin2dec: (seq of (nat) -> nat)
revBin2dec(s) ==
(if (s = [])
then 0
elseif (s = [0])
then 0
#access
アクセス修飾子の種類
#location
ユーザが指定した
VDM++仕様のパスと定
義の開始位置
#name
定義名
#type
引数の型
#kind
定義ブロックの種類
#body
定義本体
elseif (s = [1])
then 1
else ((hd s) + (2 * revBin2dec((tl s)))))
2015/02/20
JaSST東京2015＃D2
15
解析用内部表現データ
• 構文解析データを解析に適した情報(モジュー
ルの分割、if elseの対応など)に変換したデータ
…
#kind
explicit function
#body
private revBin2dec: (seq of (nat) -> nat)
revBin2dec(s) ==
(if (s = [])
then 0
elseif (s = [0])
then 0
elseif (s = [1])
then 1
else ((hd s) + (2 * revBin2dec((tl s)))))
2015/02/20
JaSST東京2015＃D2
if1
(s = [])
then
0
elseif
(s = [0])
then
0
elseif
(s = [1])
then
1
else1
((hd s) + (2 * revBin2dec((tl s))))
16
抽出規則
• 以下の抽出規則に従い、解析用内部表現データ
から条件と動作を抽出しString型の配列に格納
条件抽出処理パターン
動作抽出処理パターン
if “条件’’ then
elseif “条件” then
then “動作’’ if
then “動作’’ elseif
then “動作’’ else
else “動作’’ if
else “動作’’ elseif
else “動作’’ else
else “動作’’ EOF
cases “条件’’ ->
-> “動作’’ cases
others “動作’’ EOF
pre “条件’’ post
pre “条件’’ EOF
post “条件’’ EOF
2015/02/20
JaSST東京2015＃D2
※EOF(End Of File)
17
条件配列
条件配列
解析用内部表現データ
if1
(s = [])
then
0
elseif
(s = [0])
then
0
elseif
(s = [1])
then
1
else1
((hd s) + (2 * revBin2dec((tl s))))
2015/02/20
インデックス
ス
条件
0
(s = [])
1
(s = [0])
2
(s = [1])
抽出規則
条件抽出処理パターン
動作抽出処理パターン
if “条件’’ then
elseif “条件” then
then “動作’’ if
then “動作’’ elseif
then “動作’’ else
else “動作’’ else
else “動作’’ elseif
else “動作’’ else
else “動作’’ EOF
-> “動作’’ cases
others “動作’’ EOF
cases “条件’’ ->
pre “条件’’ post
pre “条件’’ EOF
post “条件’’ EOF
JaSST東京2015＃D2
※EOF(End Of File)
18
動作配列
動作配列
解析用内部表現データ
if1
(s = [])
then
0
elseif
(s = [0])
then
0
elseif
(s = [1])
then
1
else1
((hd s) + (2 * revBin2dec((tl s))))
2015/02/20
インデックス
動作
0
0
1
1
2
((hd s) + (2 * revBin2dec(( tl s ))))
抽出規則
条件抽出処理パターン
動作抽出処理パターン
if “条件’’ then
elseif “条件” then
then “動作’’ if
then “動作’’ elseif
then “動作’’ else
else “動作’’ else
else “動作’’ elseif
else “動作’’ else
else “動作’’ EOF
-> “動作’’ cases
others “動作’’ EOF
cases “条件’’ ->
pre “条件’’ post
pre “条件’’ EOF
post “条件’’ EOF
JaSST東京2015＃D2
※EOF(End Of File)
19
CA-Table
解析用内部表現データ
if1
(s = [])
then
0
elseif
(s = [0])
then
0
elseif
(s = [1])
then
1
else1
((hd s) + (2 * revBin2dec((tl s))))
2015/02/20
条件配列
インデックス
条件
0
(s = [])
1
(s = [0])
2
(s = [1])
CA-Table
条件
インデックス
トークン
動作
インデックス
0
if1
0
1
elseif
0
2
elseif
1
0
else1
2
動作配列
JaSST東京2015＃D2
インデックス
動作
0
0
1
1
2
((hd s) + (2 * revBin2dec(( tl s ))))
20
真理値の生成手順
1.
2.
3.
4.
真理値の値を格納する配列を作成
配列の1列目を選択
CA-Tableの1行を選択
トークンを比較し、配列に真理値の値を格納
a.
“if”, “elseif”, “cases”のいずれかに一致した場合
i.
ii.
b.
条件インデックス先の行に対し、選択した列へ“Y”を、次の列から列の終了
まで“N”を格納
選択した列の動作インデックス先へ“X”を格納
“else”, “others”に一致した場合
i.
ii.
条件インデックス先の行に対し、選択した列へ“N”を、次の列から列の終了
まで“-”を格納
選択した列の動作インデックス先へ“X”を格納
5. 選択していない行がある場合、配列の次の列を選択し3.に戻
る。ない場合は真理値が完成
2015/02/20
JaSST東京2015＃D2
21
真理値の生成1
1.
2.
3.
真理値の値を格納する配列を作成
配列の1列目を選択
CA-Tableの1行を選択
String型二次元配列
条件数 ＋ 偽(else, others)の数
0
if1
0
1
elseif
0
2
elseif
1
0
else1
2
2015/02/20
動作
インデックス
動作数
トークン
条件数
条件
インデックス
JaSST東京2015＃D2
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
22
真理値の生成2
4.
トークンを比較し、配列に真理値の値を格納
a.
“if”, “elseif”, “cases”のいずれかに一致した場合
i.
ii.
条件インデックス先の行に対し、選択した列へ“Y”を、次の列から列の終
了まで“N”を格納
選択した列の動作インデックス先へ“X”を格納
Y
N
N
N
1
-
-
-
-
2
-
-
-
-
条件
インデックス
トークン
0
if1
0
1
elseif
0
0
X
-
-
-
2
elseif
1
1
-
-
-
-
0
else1
2
2
-
-
-
-
2015/02/20
動作
インデックス
0
JaSST東京2015＃D2
23
真理値の生成3
5.
選択していない行がある場合、配列の次の列を選択し3.に戻
る
Y
N
N
N
1
-
-
-
-
2
-
-
-
-
条件
インデックス
トークン
0
if1
0
1
elseif
0
0
X
-
-
-
2
elseif
1
1
-
-
-
-
0
else1
2
2
-
-
-
-
2015/02/20
動作
インデックス
0
JaSST東京2015＃D2
24
真理値の生成4
4.
トークンを比較し、配列に真理値の値を格納
a.
“if”, “elseif”, “cases”のいずれかに一致した場合
i.
ii.
条件インデックス先の行に対し、選択した列へ“Y”を、次の列から列の終
了まで“N”を格納
選択した列の動作インデックス先へ“X”を格納
Y
N
N
N
1
-
Y
N
N
2
-
-
-
-
条件
インデックス
トークン
0
if1
0
1
elseif
0
0
X
X
-
-
2
elseif
1
1
-
-
-
-
0
else1
2
2
-
-
-
-
2015/02/20
動作
インデックス
0
JaSST東京2015＃D2
25
真理値の生成5
4.
トークンを比較し、配列に真理値の値を格納
a.
“if”, “elseif”, “cases”のいずれかに一致した場合
i.
ii.
条件インデックス先の行に対し、選択した列へ“Y”を、次の列から列の終
了まで“N”を格納
選択した列の動作インデックス先へ“X”を格納
Y
N
N
N
1
-
Y
N
N
2
-
-
Y
N
条件
インデックス
トークン
0
if1
0
1
elseif
0
0
X
X
-
-
2
elseif
1
1
-
-
X
-
0
else1
2
2
-
-
-
-
2015/02/20
動作
インデックス
0
JaSST東京2015＃D2
26
真理値の生成6
4.
トークンを比較し、配列に真理値の値を格納
b.
“else”, “others”に一致した場合
i.
ii.
条件インデックス先の行に対し、選択した列へ“N”を、次の列から列の終
了まで“-”を格納
選択した列の動作インデックス先へ“X”を格納
Y
N
N
N
1
-
Y
N
N
2
-
-
Y
N
条件
インデックス
トークン
0
if1
0
1
elseif
0
0
X
X
-
-
2
elseif
1
1
-
-
X
-
0
else1
2
2
-
-
-
X
2015/02/20
動作
インデックス
0
JaSST東京2015＃D2
27
真理値の生成7
5.
CA-Tableの全ての行を選択し終えた場合、真理値の生成手
順を終了し、真理値が完成
Y
N
N
N
1
-
Y
N
N
2
-
-
Y
N
条件
インデックス
トークン
0
if1
0
1
elseif
0
0
X
X
-
-
2
elseif
1
1
-
-
X
-
0
else1
2
2
-
-
-
X
2015/02/20
動作
インデックス
0
JaSST東京2015＃D2
28
デシジョンテーブルの生成
Rule
#1
#2
#3
#4
(s = [])
Y
N
N
N
(s = [0])
-
Y
N
N
(s = [1])
-
-
Y
N
0
X
X
-
-
1
-
-
X
-
((hd s) + (2 * revBin2dec((tl s))))
-
-
-
X
Condition
Action
2015/02/20
JaSST東京2015＃D2
29
VDTableの外観
VS-Screen
D-Tree
DT-Panel
2015/02/20
JaSST東京2015＃D2
30
DT-Panel
A：モジュールタブ
{Q}：事後条件タブ
{P}：事前条件タブ
2015/02/20
JaSST東京2015＃D2
31
D-Tree
描画
任意の定義をクリック
再描画
2015/02/20
JaSST東京2015＃D2
32
真理値の生成手順
1.
2.
3.
4.
再掲
真理値の値を格納する配列を作成
配列の1列目を選択
CA-Tableの1行を選択
トークンを比較し、配列に真理値の値を格納
a.
“if”, “elseif”, “cases”のいずれかに一致した場合
i.
ii.
b.
条件インデックス先の行に対し、選択した列へ“Y”を、次の列から列の終了
まで“N”を格納
選択した列の動作インデックス先へ“X”を格納
“else”, “others”に一致した場合
i.
ii.
条件インデックス先の行に対し、選択した列へ“N”を、次の列から列の終了
まで“-”を格納
選択した列の動作インデックス先へ“X”を格納
5. 選択していない行がある場合、配列の次の列を選択し3.に戻
る。ない場合は真理値が完成
2015/02/20
JaSST東京2015＃D2
33
テストベース
再掲
• テストに必要な情報をテスト技法で考える
同値分割法
ソフトウェアやシステムへの入力を、同じ処理をする
グループに分割するための情報
境界値分析
さまざまな境界となる値
デシジョンテーブルテスト
条件、条件の組み合わせ、動作(結果)
状態遷移テスト
状態、状態の前後の条件、状態間の遷移、イベント
(入力)
ユースケーステスト
アクター(ユーザ、システム)、アクターとシステムとの
相互作用(シナリオ)、事前条件、事後条件
制御パステスト
ソースコード (テスト結果の判定の際に仕様)
オールペアテスト
(ペアワイズテスト)
因子、水準、禁則
エラー推定
過去のバグ情報
2015/02/20
JaSST東京2015＃D2
34