lecture at Univ.Paderborn

ソフトウェア工学/
検証指向開発VODの巻
九州産業大学情報科学部
松本正雄 2009
Prof. Dr. Masao J. Matsumoto
2009
1
Verification-oriented
Development (VOD)
Prof. Dr. Masao J. Matsumoto
University of Dortmund,
University of Tsukuba,GSSM
Kyushu Sangyo University
2009
2
検証指向のソフトウエア開発
 検証とは?
 正しいか否か調べて証拠付で結論付け
ること
 検証は必要か?
 検証指向の開発(VOD)を行うのは何故
か?
 そうしないと検証不可能に陥ってしま
うから
2009
3
VOD講義内容
 テスト技法
 検証指向の開発手順
 状態遷移を含むソフトウエアの検証法
2009
4
VOD:Verification-oriented
Development
Competitive Software Technology
2009
5

信
頼
を
得
る
秘
訣
2009
エ検
ア証
開指
発向
技の
法ソ
フ
ト
ウ
6
検証は重要
設計
Relation
各種仕様
設計の検証
2009
Fig.6.9 検証作業
被検証物
比較
正当
比較:
本来設計結果が満たすべき条件
を予測正解値として求め、その
条件と実際に行われた設計を
比較
7
Verification is Crucial
Design
Relation
Specification
Testee
Compare
Correct
Verification Design
2009
Fig.6.9 Verification Activities
8
Mathematical Review
被検証物
設計
証明
証明責任
不一致
Relation
Specification
証明妥当性の確認
2009
Fig.6.15 Review by Mathematical Approach
9
Mathematical Review
Testee
Design
Proof
Fulfil Proof Responsibility
Unmatch
Relation
Specification
Check the Proof Feasibility
2009
Fig.6.15 Review by Mathematical Approach
10
Technical Review
被検証物
設計
レビュー者の能力
仕様
レビュー
レビュー視点
Fig.6.16 Review by Technical Approach
2009
11
Technical Review
Design
Testee
Reviewers'
Expertise&Ability
Specification
Review
Review Viewpoints
Fig.6.16 Review by Technical Approach
2009
12
Managerial Review
Specification
仕様
設計
作業記録
確認
成果
納期やUI
レビュー者の
能力
標準
開発管理
2009
Fig.6.17 Review by Managerial Approach
13
Managerial Review
Specification
Specification
Design
Activity Records
Confirmation
Products
Looks and Delivery Date
Reviewers'
Expertise&Ability
Standards
Development Management
2009
Fig.6.17 Review by Managerial Approach
14
ライフサイクルにおける検証
1
12
2
3
11
4
5
10
1 分析Analysis
6
3 概要設計
5 詳細設計
7 実装
12 運用
7
9
8
11 システムテスト
10 複合テスト
2,4,6,8 レビュー
2009
9 単体テスト
15
Fig 6.11 Verification throughout Life Cycle
Verification in Life Cycle
1
12
2
3
11
4
1 Analysis
2 Gross
5Design
Detail Design
7 Implement'n
5
6
10
12 Operations
7
9
8
11 System Test
10 Compound Test
2,4,6,8 Reviews
2009
9 Unit Test
16
Fig 6.11 Verification throughout Life Cycle
Intermediate Products in
Life Cycle
1
12
2
3
1Analysis 4
5
3 Gross Design
5 Detail Design
6
7
9
7 Implement'n
2 Functn'l Specificat'n
8
4 Block Specificat'ns
6 Module Specificat'ns 8 Code Modules
2009
12'
11
11'
10
9'
12 Operations
10'
12'Evaluat'n
11 System Test
11' System
10 Compound Test
10' C.Tested Block
9 Unit Test
9' C.TestedModule
17
テスト
 最小の労力で最大のテスト効果を狙う
 背景


2009
・検証に多大な労力時間を要す
・テスト網羅率を向上させたい
18
テスト技法の種類
 テスト
 静的:実行しないでテスト
 動的:実行してテスト
 網羅テスト
 制御フロー
 機能データフロー
2009
19
同値
入力データを個々に識別するかわりに、同じ
特性を有する部分集合を捉え、その部分集合
に対して1つのテストを行う。
 部分集合を同値クラス(または単に同値と呼
ぶ)を使って、テストを行う。
 仕様合致:有効同値。
 仕様不一致:無効同値。


2009
Xyz、456、b2y7、@hks
20
同値を使用したテストの例題


仕様書:
データを読み、それが
–
–


8桁以内の英数字(半角小文字)なら“正しい
(または1)“そうでなければ“誤り(または
0)”と表示する。
先頭の1バイトが*であるなら、終了する。
例題:
上記のプログラムをテストする場合、用意
すべきテストデータと実施すべきテスト
ケースは何通りか?
2009
21
同値を使用したテストの例題


仕様書:
データを読み、それが
–
–



8バイト以内の英数字(半角小文字と限らない)
なら“1”そうでなければ“0”と表示する。
先頭の1バイトが*であるなら、終了する。
例題:
上記のプログラムをテストする場合、用意
すべきテストデータと実施すべきテスト
ケースは何通りか?
回答用紙に学籍番号、氏名:ファイル名は
英数字で学籍番号.doc
6.12(金)13:00
2009
22
採点基準
 論理を示していて、しかもその論理が
正しい。100点
 論理を示しているが、その論理が間
違っている。間違い1件ごとに10点
減。
 論理を示さず、思いつきを幾つか並べ
た。高々50点
 未提出。0点
2009
23
多い間違い
1.論理を示していない(ただ場合を幾つか
列挙しただけ)。
 2.網羅的でない。
 3.テストデータの通りを示さずテストケー
スのみ。
 4.U-(A or B)から選ばず。
 5.正しいデータ(有効同値)の場合、処理
結果が正しいと応答したか」が脱落してい
る。

2009
24
正解
 前提:データは読めた。大文字小文字
は問わない。
 停止性のテスト:
 1.*がきたら停止した。
 2.*がきたが停止しなかった。¥
 3.*以外がきたら停止した。¥
 4.*以外がきたら停止しなかった。
2009
25
正解(続)
 データごとの処理妥当性→30通り
– 入力データを全角とみなす場合5x3=15通り
 有効同値データがきたら1とした。
 有効同値データがきたら0とした。
 有効同値データがきたら0,1以外とした。
 無効同値データ4通りに対して上記3通り。
– 入力データを半角とみなす場合5x3=15通
り
2009
26
全体で34通り
 停止性→4通り
 妥当性→30通り
2009
27
システムとしては、さらに多い
 ファームウエアのテスト
 DOSレベルのテスト
 OSレベルのテスト
 ミドゥルウエアレベルのテスト
 アプリケーションレベルのテスト
2009
28
過誤の2種類
 第一種の過誤:間違いを正しいとする
 第二種の過誤:正しいを間違いとする
2009
29
回答
 このプログラムのテストケースは以下
の□通りです:
 1. *を使って結果がプログラム停止
 2.tdを使って結果が1であるか
 3.tdを使って結果が1であるか
 続く
 (td:具体的にテストデータを書く)
2009
30
1 0
2 0
3 0
4 4
5 0
6 4
7 1
 8以上

2009
0
31
同値の例題
入力データについて、その長さが8文字以内
で、しかも英数字だけから構成されているか
否かを調べ、もしそうなら「1」、そうでな
ければ「0」を表示するプログラムをテスト
するときに必要なデータは何通りか?*で停
止。半角小文字。データ5、Tケース10通り
 正常データ使用して結果が0か
 正常データ使用して結果が1か
 異常データ使用して結果が0か
 異常データ使用して結果が1か

2009
32
ある方法
 前記例題を網羅的にテストするための
 データ入力の数は?
 n個の文字種のなかから1文字選び、r
桁の文字列を作ること
 n=36、0=<r<=8
 何通りになるか?
2009
33
C=Σnr
r=1から8
 n=36
 異常な場合がさらに加算されなければ
ならない!
2009
34
Equivalent Value
a
c
b
u
a: Subspace of which elements are those string of which size is 8 character-long or less
b: Subspace of which elements are strings which are composed only by alphanumeric
c= a AND b
u: all possible combinations of remaining inputs
2009
Fig 6.20 Subspaces and equivalent values
35
Equivalent Value ベン図
a
u
c
b
a: Subspace of which elements are those string of which size is 8 character-long or less
b: Subspace of which elements are strings which are composed only by alphanumeric
c= a AND b
u: all possible combinations of remaining inputs
2009
Fig 6.20 Subspaces and equivalent values
36
回答










2009
有効同値使用して結果が1か
上記で結果が0か
無効同値(英数以外で8桁)使用して結果が0か
上記で結果が1か
無効同値(英数で8桁超え)使用して結果が0か
上記で結果が1か
無効同値(英数以外で8桁超え)使用して結果が0か
上記で結果が1か
*が来て停止するか
上記で停止しないか
37
Input Grouping by
Functional Decomposition
Input
Blackbox
Input Group 1
F1
Input Group 2
F2
Input Group 3
F3
Functionalities
Fig 6.22 Input Grouping by Functional Division
2009
38
同値分割法
 仕様に基づき、「有効な部分集合」
「無効な部分集合」に集約すること。
 例題では「桁数チェック」と「文字種
チェック」の2つの処理があるので、
その2つに分割して、同値を求める:
2009
39
同値
 ①有効同値:桁数8以下で英数字だけか
らなる文字列 部分集合c
 ②無効同値1:非英数字を含む8桁以下
の文字列 部分集合(a-c)
 ③無効同値2:8桁超えていて英数文字
列 部分集合(b-c)
 ④無効同値3:8桁超えていて非英数字
を含む文字列 u-(a or b)
2009
40
Relationship among Input
Equivalent Values
Equivalent value group 1
11
Equivalent value
12
1m
Equivalent value group 2
21
22
2m
Equivalent value group n
n1
Combination
Output 1
Logic
n2
nm
2009
Fig 6.23 Equivalent values Relationship
41
限界値分割
 本質的に同値と同概念。得られた同値
分割から実テストデータ作成時境界を
重視する。
 例:8文字と9文字の文字列
 内部コードA(Z)の1つ前(後)の文
字
2009
42
テスト効果の優れたテストと
は?
 網羅率が良いこと(最大のテスト効
果)
 効率的であること(最小のテスト工
数)
2009
43
例題1
ファイルの内容を表示するShowMeFileコマン
ドの機能をテストする場合を考えよう
 ShowMeFileコマンドの仕様
 指定されたファイルの内容を表示する。もし
パラメタが*なら、すべてのファイルの内容
を、特定のファイル名ならそのファイルの内
容を表示する。
 パラメータENDが来たら停止する。
課題
・使用テストデータは何か?
・テストケースは?

2009
44
上記コマンドのテスト設計
 行うべき
– テストデータ
– テストケース
 を言え。
2009
45
前記のテストを行わねばならない
君なら、どう行うか?
 何通りのテストを行えば済むと思うか?
 答1 2通り
 答2 3通り
 答3 4通り
 答4 5通り
 答5 6通り
 答6 7通り以上

2009
46
レポート回答結果

7通り、根拠不正:松井、山田
6通り、根拠論理性有るが場合2つ見逃しと数え方誤り:△田中宏
異常の場合の挙げ方が不完全(ENDの場合見逃し):▽小田
根拠不正解:藤本
、TD無回答:梅野:
5通り、根拠不正:菅原
4通り、根拠正解だが、場合の数え方誤り:◎麻生、◎安東、◎田中賢
根拠論理性有るが場合1つ見逃し:○中村,○坂原,○古田,○廣松
C,E部分回答:白川
Cだけ:林田、廣松、中園
C/根拠不正:廣田、野見山、倉本
3通り、根拠論理性有るがENDと不正パラメタの場合を見逃し:○西丸
根拠不正:下田、緒方
2通り、根拠不正:宮川、松下
回答誤りか未了:梶山、川添、貫

未提出:吉村(晴剛、奨太)、伊東、弓崎、増永、豊住、淵脇














2009
47
テストの肝要事項
 最も少ない工数で最大の網羅を確実にす
ること。
 その目的を達成することが品質信頼性の
高い製品を作成するための1つの必要条
件である。
 目的達成に役立つ方法を駆使するのが優
秀な技術者。
2009
48
テスト方法の例
 同値データ方法
 限界値データ方法
 原因結果グラフ(CED)方法
 ケースフロー図(CFD)方法
2009
49
CED(Cause-Effects Diagram)方法
 同値法は必要十分なテストデータを設
計するには便利
 テストケース設計には使用テストデー
タと期待値と実行結果の組を捉える必
要がある。
 ①テストデータ、②その実行結果、③
期待値の組が与えられれば正常か異常
かの判定が可能。→①②③を見て。
2009
50
CED法の手順
 1)原因(テストデータ)と結果(期
待値)を各々列挙する
 2) 原因と結果の関係を見極める→図
式化する
 3)上記に基づいて、テストケースを
作る(ディシジョンテーブルを作成)
2009
51
CED方法の手順
 1)原因結果グラフを作成して最も網
羅的でしかも効率的なテストを行う
 2)原因結果グラフとは原因と結果の
関係を同定して図示。
– 入力データとなる同値を原因、出力を結果
と呼ぶ。
 3)原因を列挙する。有効と無効同値
4)結果を列挙する。
5)原因と結果の関係からテストケー
スを設計する。
2009
52
前記プログラムのCEDを書け
 原因には何があるか?
 結果には何があるか?
 原因と結果の関係は何か?
2009
53
ShowMeFileコマンドのCED

3)原因は次の3つ。
①*が指定された
②なんらかのファイル名が指定された
③指定されたファイルは存在している
4)結果は次の3つ。
(70)指定されたファイルの内容を出力する
(71)パラメータ不正のエラー表示をする
(72)指定されたファイルが存在しない旨エラー
表示する。
2009
54
最小の回数で網羅的なテスト効果を
行なうには、いかなるテストを行え
ば良いか(何通りのテスト)?
ヒント
 1.左側に入力同値(原因)を書き、右側に
結果を書く。
 2.原因から結果に向け、因果関係を結線
し、結果が成立する条件を加味してCED(原
因結果グラフ)を作成する。
 3.それを基にデシジョンテーブルを作成す
る。

2009
55
例題に対する原因結果グラフ
原因
1
結果
71
not
or
11
2
and
and
3
not
70
72
Fig 6.25 Cause-Effect Graph
2009
56
Cause-Effect Graph:Example
Causes
1
Effects
71
not
or
11
2
and
and
3
not
70
72
Fig 6.25 Cause-Effect Graph
2009
57
デシジョンテーブル例1
Table 6.2 Decision Table for Example
テスト項目
1 2 3 4 5
原因
(1)
(2)
(3)
結果
(70)
(71)
(72)
2009
1 0 0 0
0 1 0 1
1 1 - 0
1 1
1
1
上段
1:真
0:偽
ー:不問
下段
1: 成立する
空白:成立せず
58
デシジョンテーブル例2
追加 原因 (4)END
結果(73)プログラム停止
Table 6.2 Decision Table for Example
テスト項目
1 2 3 4 5
原因
(1)
(2)
(3)
(4)
結果
(70)
(71)
(72)
(73)
2009
1 0 0
0 1 0
1 1 0 0 0
0 -
1 -
0 -
0 1
上段
1:真
0:偽
ー:不問
下段
1: 成立する
空白:成立せず
1 1
1
1
1
59
Decision Table:Example
Table 6.2 Decision Table for Example
Test Items
1 2 3 4 5
Causes
(1)
(2)
(3)
1
0
1
0 0 0
1 0 1
1 - 0
Effects
(70)
(71)
(72)
1
1
2009
1
1
60
CFD(Case-Flow Diagram)技法
 CED技法よりテスト項目数を減らせる
 同値分割と同値間関係をベン図で表現
2009
61
Equivalent Value Subspace
by CFD without Common
U
a
Space
U
a
Subspace
U - (a or b)
b
Subspace
b
U:Large Island for Equivalent value, a,b : Small Island for Equivalent value
2009
Fig 6.27 Equivalent value subspacing by CFD
62
同値集合(共通部分無しの場合)
ベン図
CFD
U
a
母集合
U
a
部分集合
U - (a or b)
b
部分集合
b
U:Large Island for Equivalent value, a,b : Small Island for Equivalent value
2009
Fig 6.27 Equivalent value subspacing by CFD
63
同値集合(共通部分有りの場合)
ベン図
CFD
U
U
a
a
c
c
c=a^ b
b
b
U-(a or b)
2009
Fig 6.28 Equivalent value subspacing by CFD
64
Equivalent Value Subspace
by CFD with Common
U
U
a
a
c
c
c=a^ b
b
b
U-(a or b)
2009
Fig 6.28 Equivalent value subspacing by CFD
65
例題2 LHA高圧縮書庫管理プロ
グラム
LHA 命令、オプション、その他パラメタ
 命令 英字1文字(aumfdpexlvst)xor 省略
 a:ファイル追加、u:新ファイル追加、m:新ファイ
ル移動、f:ファイル更新、d:ファイル削除、p:
ファイル閲覧、e:ファイル復元、x:デイレクト
リ付でファイル復元、l:書庫一覧表示、v:同
左d付、s:自己解凍書庫作成、t:書庫のテス
ト

2009
66
続
オプション –rwxmpcazthonisl 複数指定可
 -が指定されていれば、オプション有り、
 -が指定されていないなら、オプション無し
 r:サブデイレクトリも検索、w:ワークデ
イレクトリ指定、x:デイレクトリ名を有効
に、m:問い合わせしない、p:名前の比較
を厳密に行う、c:日時参照を行わない、a:
全属性を凍結対象とする、z:無圧縮格納、
t:書庫の時刻を最新ファイルに、h:ヘッ
ダ形式

2009
67
続
 その他パラメタ
– LZH ? [DIR ?][FILES ?]
– ?は各名称指定または省略
 LHAコマンド全体の形式
– LHA [命令][オプション][LZH ?[DIR
2009
?][FILES ?]]
68
命令部に関して、CFD図を描け
2009
69
LHA例題に対するケースフロー図
(Case-Flow Diagram )
N:Not specified
命令部
IS:Identifier specified
a
オプション部
f
-
N
r
N
N
x
l
N
N
無効
LZH 書庫
ディレクトリ
IS
IS
N
N
2009
ファイル
IS
N
70
IEV
Final Case-Flow Diagram
for LHA Example
N:Not specified
Operators
IS:Identifier specified
a
Option list
f
-
N
r
N
N
x
l
N
N
無効
Fig 6.29 EVS for Example LHA Operators
LZH Lib.
Fig 6.30 EVS for Example LHA Option List
Directory
IS
IS
N
N
File
IS
N
2009
71
IEV
Fig 6.31 EVS for Example LHA Parameter option
070630演習の結果
 田中宏宗:分岐数は正解
 貫大路:ごく部分的
2009
72
例題 原因結果グラフとCFDの2通り表示せよ
原因結果グラフ
原因 40通り
内訳
命令部 14通り(12種類命令+誤り+空白)
オプション部 17通り
その他パラメタ 9通り(除くファイル名のループ)
2009
73
1
or
2
11
3
4
and
70
or
5
12
6
7
CED原因結果グラフ
2009
74
CFD流れ図
 CFDでは1,2,3と4,5,6,7は独立とみなす
4
1
2
3
分岐数が3の場合
2009
5
6
7
分岐数が4の場合
75
原因結果グラフとCFD流れ図
 左側原因欄の件数を比較せよ
2009
76
より効果的で効率的な検証へ
テストケース
Causes
1
2
3
4
5
6
7
Effective Results
1 2 3 4 5 6 7 8 9 10 11 12
1
1 1 1 1
1
1 1 1 1
1
1
1
1
1
1 1 1 1
1
1 1 1
Table 6.3 CEDで設計したテスト項目
2009
1
1
1
1
1
1
1
1
1 1
3 4
1
1
1
1
2
1
1
1 1
1
1
1
1
1
1 1 1
Table 6.4 CFDによるテスト項目
77
Towards More Effective and
Efficient Verification
Test Items
Causes
1
2
3
4
5
6
7
Effective Results
1 2 3 4 5 6 7 8 9 10 11 12
1
1 1 1 1
1
1 1 1 1
1
1
1
1
1
1 1 1 1
1
1
1
1
1
1 1 1
1
1
1 1
1
1
1
Table 6.3 Test Items designed by Cause-Effect Method
2009
1
1
1
1
1 1
3 4
1
1
1
1
2
1
1
1 1 1
Table 6.4 By Case Flow Diagram
78
特別:VODの要諦
 1.V字型工程と検証
 2.設計検証
 3.効果的なテストを効率的に
 4.状態遷移プログラムの検証
2009
79
状態遷移を伴うシステムの検証
 特別の配慮が要る
 システムの外部から次のことが困難
– ある状態に設定すること(含むその確認)
– 他の状態に遷移させること(含むその確
認)
2009
80
状態遷移プログラムの状態
I
O
M
S
I:Input
O:Output
S:State
M:State Transit
Program
M1:Output Setup
M2:State Setup
Fig.6.35a Blackbox Program having State Transit
2009
Fig.6.35b Program Subdivide
81
状態遷移プログラムの状態
I
O
M
S
I
M1
I:Input
O:Output
S:State
M:State Transit
Program
M1:Output Setup
M2:State Setup
Fig.6.35a Blackbox Program having State Transit
2009
O
M2
S
Fig.6.35b Program Subdivide
82
State in State-transition
Program
I
O
M
S
I
M1
I:Input
O:Output
S:State
M:State Transit
Program
M1:Output Setup
M2:State Setup
Fig.6.35a Blackbox Program having State Transit
2009
O
M2
S
Fig.6.35b Program Subdivide
83
状態遷移プログラムを分解
Decompose
I
I:入力
M1
M1:状態設定
S
o
M2:出力設定
S:状態変数
Si:入力変数複数
I
M2
O:出力
O
Si
Fig.6.36 Decompose M to M1 and M2
2009
84
Decompose State Transition
Program
I
I:Input
M1
S
M1:State Setup
M2:Output Setup
S:State
Si:Input States
I
M2
O:output
O
Si
Fig.6.36 Decompose M to M1 and M2
2009
85
状態遷移プログラムのデバッ
グの仕組み
I
O
M2
M1
Si
2009
Debugger
S
Fig.6.37 Test Environment for State Transit Program
So
86
How to test State Transit
Program
I
O
M2
M1
Si
2009
Debugger
S
Fig.6.37 Test Environment for State Transit Program
So
87
“テスト設計”先行で設計と
実装を制約
Traditional
A
Test Phases
GD
DD
DT
TR
DT:テスト設計
TR:テストラン
VOD
A
A:分析
DT
GD
DD
TR
GD:概要設計
DD:詳細設計
Fig 6.38 VOD Lifecycle vs.Traditional
2009
88
"Test Design" constraints
Design and Implementation
Traditional
A
Test Phases
GD
DD
DT
TR
DT:Design for Test
TR:Test Run
VOD
A
A:Analysis
DT
GD
DD
TR
G/DD:Gross/
Detail design
Fig 6.38 VOD Lifecycle vs.Traditional
2009
89
VODでの設計制約の仕方
Decision Table
モジュール
Control
Decision
Causes
Data
Active
Process
Effects
Process
Passive
Control
External Data/
Internal Data
2009
Processed
Process
Fig 6.40 Data and Module Structure in VOD
90
制約のポイント
 モジュールをアクティブとパッシブに
峻別し、前者をマーク
 データを制御向けと処理向けに峻別
し、前者をマーク
2009
91
Design Constraints in VOD
Decision Table
Modules
Control
Decision
Causes
Data
Active
Process
Effects
Process
Passive
Control
External Data/
Internal Data
2009
Processed
Process
Fig 6.40 Data and Module Structure in VOD
92
Who will be Competitive?
TQC will no longer be enough.
 VOD is a promising technology for
software houses to keep striving
through good quality, because VOD
enables us to avoid as much defects
that will always cause failures.
 VOD plus Product Architect makes
software happen.

2009
93