Generating Method for Combinatorial Testing Data Using Propositional Normal Form Conversion

In an embedded system which operates multiple devices, combinatorial testing of multiple events is needed to verify proper behavior of the system. However, the number of test cases becomes huge, especially for the order in which events happen in parallel, and it is difficult to carry out all cases.  So many methods to generate minimum test data set have been already proposed, but their reduction is not enough or their usage is less flexible.  This paper describes a simple and flexible algorithm of generating combinatorial test data efficiently.  This method represents combination conditions with propositional logic formula in the conjunctive normal form (CNF) and converts it into the disjunctive normal form (DNF).  Each term of the DNF becomes a set of test data to cover all combinations.  This method is available to use for any type of combinatorial testing data generation, not only for an event order, and is able to impose additional conditions.  However, since this method is applicable only to the problem of small size, improvement of the algorithm is required.


The relation of CNF and DNF used here is explained using a simple example.  Assume that there are 6 kinds of food, p1...p6, and there are 5 kinds of vitamins, c1...c5, which are contained in those foods. Table 1 shows the vitamins contained in foods.  This table is called an AND-OR table, because an OR combination is used for column elements and an AND combination is used for raw elements.

The purpose here is searching for combinations of foods p1-p5 which can take in all vitamins.  In order to take in c1, p1 or p3 or p6 are required.  This is expressed as c1 = p1∨p3∨p6.  About each vitamin the conditions for required foods are as follows.

The condition which takes in all vitamins is (2).  This is the CNF which is the total condition.

This condition is converted into DNF as follows:

Each clause of DNF becomes the combination of the food which satisfies the expression (2).  For example p1 and p2 is one of the minimum set.  The foods and the vitamins in this example correspond to the test cases and the conditions to be satisfied respectively.

単体テストできない関数

ヨーロッパの鉄道の安全規格[1]で一番厳しいSIL4ではブランチテストの100%カバレッジが求められるらしい。if文がネストしている複雑な関数の場合、そこにたどり着く入力データを作り出すのはなかなか難しい。CBMCを使って簡単にテストデータを生成する方法としてassert(0)を埋め込む方法がある。到達したい場所にassert(0)を仕込んで置いてCBMCで検証をすればCBMCが向きになってそこまで行って転けてくれるのでたどり着く方法が明確になる。必要があればprintf文も仕込んでおく、さらにテキストファイルに書き出すようにすれば、テストツールに掛けられる形でテストケースを得ることができる。

しかし、この方法も構造化されたプログラムでないとうまく行かない。構造化されたプログラムというのは、逐次、分岐、繰り返し構造だけでできているプログラムで、前方に跳ぶgoto文とか入れ子にならない繰り返しを持っていないプログラムである。今時、この様なプログラムはアセンブラで書かれたOSのディスパッチャぐらいだろう。ところが、並列性がある場合は任意のgoto文が動的に入るのと同じだからうまく行かない。要するに単体テストできないのと同じである。
グローバル変数を使っていても並列性が無ければ単体テストはできるが、それがvolatileなものだとそうはいかない。いちいちvolatile宣言しないとテスト以前にコンパイルがチャンとできているか心配になる。

並列性がある場合には、節操なくグローバル数を使うことは控えなければならない。空海がどのように並列に文章を書くのか、文章だけはできていて出力だけが並列なのか、文章も考えながらつじつまの合うものを書き出すのか、これはアーキテクチャがぶれていては実現できない。
グローバル変数を多用して、並列性のあるシステムを作っていて、単体テストもチャンとやってますとか言う組織は多いけれどどんな単体テストをやっているのだろうか。

[1] European Committee forElectrotechnical Standardization. Railway Applications -
Communication, signalling and processing systems - Software forrailway control
and protection systems, http://www.cenelec.eu

原因結果グラフ-2 MASK

結果グラフで　A masks B とした場合の扱いは

1) A⇒￢B
2) Aが真ならBは未定義(三値論理の利用)
3) Aの真偽による場合分け

の三通りが考えられる。

1)の場合REQ制約の否定として表現できる。CEGTestの場合は、問い合わせ中だが、REQの否定を柔軟に利用できればMASKは要らなくなってしまう。 赤い四角で囲った部分を表現することが出来るので1)の意味でのMASKは特に必要ない。

青丸で囲んだところはちょっと怪しい。と言うか括弧で括るような、否定を取る優先順位を決めなければならない。そう言うことを考えなくても良いようにREQとMASKが定義してあると言うのは合理的かも知れない。ただし、最近FXの秋山氏の指摘で新たな謎が生まれた。MASKは結果側に付ける[1]と言うものである。もしそうなら原因結果グラフは結構簡単で使いやすいものになる気がする。この謎の裏にどんな合理性があるのか調べてみたい。


2)調べてみると三値論理には何種類もある[2]。マスクされた側をどう解釈するか(a.真か偽か決まらない状態、b.真でも偽でもない第三の状態、c.無意味)によって使用する論理系が変わる。VDMはaによって未定義を扱える。ただし、実装上の都合で一部変更して利用している[3]。用途によって結構自由に使って良い見たいな感じである。原因結果グラフを命題論理の範囲で扱うことを考えているので、各ノードは命題でなければならず、単に真偽が決まっていない状態とするのが話が難しくならなくて良いと思う。VDMの様な手直しをするかどうかはまた別の問題として考えれば良いだろう。三値論理を使うと、結果側に不定が現れる。結果側に現れる不定が妥当かどうか、ちゃんと解釈できるかどうかで使用する論理系を決めれば良いと思う。それで、幾つかやってみたが三値論理を使わなかった場合すなわち、1)の方法で真にも偽にもなり得るという結果に落ち着く。aの場合の真理表は以下のようになる。*が真偽が決まらない状態。赤いところをVDMでは*として扱う。

A	B	A∧B	A∨B	A⇒B	￢A
T	T	T	T	T	F
T	F	F	T	F
T	*	*	T	*
F	T	F	T	T	T
F	F	F	F	T
F	*	F	*	T
*	T	*	T	T	*
*	F	F	*	*
*	*	*	*	*

3)“A masks B”をAが真の時はBを考慮しなくて良いというそのままの意味に解釈して。Aが真の時はBを含まない原因結果グラフを作ってしまう。これは、原因結果グラフ全体を表す論理式の真偽がどのような意味を持つのかに関わる問題と関係する。


参考文献
[1] http://en.wikipedia.org/wiki/Cause-effect_graph
[2]http://ja.wikipedia.org/wiki/3値論理

原因結果グラフを利用した形式仕様記述

形式仕様記述というと述語論理から始まるが、命題論理でもやれることは多い。その一つが原因結果グラフである。これについては以前インタフェース誌[1]に書いたことがある。しかし、最近ニフィのK氏がCEGTestをリリースされたのだがどうも仕様が違う様なので悩んでいる。また、FXのA氏のツール(X-CEG)とも違う様だ。特にMASKの扱いが違う。それで本当はどうなのか少し整理しておきたい。インタフェース誌[1]に掲載した変換規則を以下に示す。元ネタは[2]である。EとOは要素数が3ヶ以上の時は論理式の形が変わる。それは[1]を参照。

原因結果グラフの本来の使い方はテストケースを絞り込むことであり、仕様を記述することではない。仕様記述としてはMC/DC等の手法を使って絞り込む前の論理式表現に興味がある。同じ文章から原因結果グラフを作っても人によって違うグラフが出来ることが多い。それは元の文章の解釈の違いを反映するが、論理式で表現すると論理的には等価であることが分かったりする。等価でなくても、どこが違うか明確化できて仕様の解釈のブレをなくすことが出来る。

取りあえず以下の3点が気になっている。

(1)まず原因から結果に向かう線の解釈だけれど、私は⇒(ならば)でなく⇔(同値)をディフォルトで使用していた。これは問題文に依存して決めるべき。例えば、料金表などでは同値関係にしないと別の条件でも同一料金になることを認めることになる。排他的に扱いたいかどうかで使い分ける必要があるだろう。

切符の払い戻しの場合、誤購入の時は必ず払い戻すのであれば
(誤購入)⇒(払い戻し)
となる。払い戻すのは電車が止まってしまった時にも行われるので
(払い戻し)⇒(誤購入)
は成立しない。と言うようなことを考察しないと決められないのだと思う。
一般的には、原因結果グラフの元になる文章はある特定の状況を表すフレーズなのでその範囲では、電車が止まってしまうことなどは想定しない場合が多いので
(誤購入)⇔(払い戻し)

として良い場合が多いように思う。つまり普通は、
(誤購入)⇒(払い戻し)　または　(誤購入)⇔(払い戻し)
だろう。逆向きになるのは原因が目的で、結果が実現方法の様な場合かも知れない。
別の見方としてこれは論理関係ではなく定義であると思った方が良い場合もある。結果を定義しているdefine文のようなものであり、結論を一つの素命題とするのではなく単なるラベルと考える。

(2)MASKは三値論理を使用するのが正しいかも知れない。しかし、その場合結果も不定になることがある。結果が不定でも良いのかは元の文章を書いた人に確認する必要がある。たぶん不定は意図していないのではないか。

(3)これが一番重要かも知れないけれど、原因結果グラフの論理式が真になると言うことがその仕様が矛盾無いと言うことを表す。形式仕様記述は全体が真になる範囲で分析をする。偽になるところは、あり得ないと元の文章を書いた人が言っているところだから分析の対象外にする。テストの場合は、全体の真偽はあまり考えないのか? 全体が偽になるところから選んだテストケースはハードが故障した場合とかユーザーのオペレーションミスのテストに対応するのか?


幾つか事例についてそれぞれのツールの結果を比較してみたい。長くなったので(2)と(3)はまた改めて。


参考文献
[1] 新・組み込みソフトへの数理的アプローチ（第6回）

原因結果グラフ――原因と結果の関係を木構造で表現する

[2]

信頼性について-2: MTTFによるテスト

クリーンルーム手法では品質保証を目的としたテストの指標としてMTTF(Mean Time To Failure)を利用する。そして、バグ密度のような指標は品質にとっては意味がないと言っている。クリーンルーム手法はホーア理論に基づいた形式手法の一種である。

また一方、ソースコード検証ツールであるPolySpaceのWebセミナーは

1. プログラム検証によって発見されたソースコードのバグを100%取る必要は無い。95%ぐらいでよい。
2. 機能テストとプログラム検証は違う。
3. プログラム検証をやっても機能テストは必要だ。5%の取り残しバグがあっても機能テストをパスすれば良い。

と言っている。

クリーンルームの方は、機能テストをすればプログラム検証は必要ないという言い方になっていて一見すると別のようだが、障害の有無が重要でありfaultの数は重要でないと言う点では一致している気がする。バグは欠陥(fault)に対応し障害(failure)と同じでないことはすでに述べた。テストの世界では、ホワイトボックステストとブラックボックステストという分類があるが、ホワイトボックスはfaultの検出、ブラックボックスはfailureの検出と対応づけることができるかも知れない。

クリーンルームでは、ユーザの使用特性を分析して、それに基づいて実際にシステムを動かしてMTTFを測定する。ある欠陥が発見されてから次の欠陥が発見されるまでの時間がMTTFになる。このMTTFがある値以上になれば出荷基準に達したと判断する。

クリーンルーム手法によってプログラムを作ればfaultは無いはずだからfailureの検出が重要だとも説明している。またfaultの無いプログラムを高品質と定義している。faultの無いプログラムであればMTTFの測定が出来る。それでどのようなテストをするかというと、品質を測定するためのテストであり、まず利用モデルと言うものを作る。利用モデルには以下のものが含まれる。

利用者: システム外部の実態、アクターやデバイスなど
利用の仕方: 動作モデル
環境: プラットフォーム、利用の状況(昼/夜、緊急時、オートモード)

動作モデルは、状態遷移図や決定表で表現される。利用モデルからテストケースを生成するには利用の仕方の統計的情報が必要になる。具体的には各遷移の遷移確率を入れた状態マシンを利用する。同値分割とかは利用しない。ソースコードの作り方はシステムの品質とは無関係と考える。具体的にどのようにテストケースを生成するのか、MTTFをどのように測定するのかについては色々な論文を読まなくてはならない様だ。

参考文献