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.

決定論的故障⇒決定論的原因故障

systematic failureを決定論的故障と呼ぶことにかなり違和感があった。ソフトにバグがあれば必ずおかしな動作をする。これが決定論的な動作で、そのような故障原因は安全ライフサイクルの様なシステマティックなアプローチで解決する。と言うことだと理解している。間違っていたら指摘してもらいたい。

日本語は原因の特徴について述べていて、英語は対処法について述べている。ここに違和感があったのだが、Webを見ていたら決定論的原因故障と訳している場合も多く、こちらであれば、「決定論的原因による故障」と解釈することで何とか納得できる。

決定論的原因とは原因箇所を論理的に絞り込めたり、それを証明することができるタイプの故障で、またそのことによって完全に取り除くことができる故障原因と定義してはどうだろうか。


例えばコンポーネントがA,B,Cとあってある機能Fが動かなくなってコンポーネン
トBをB1交換すると動く場合には、A, B, B1, Cがそれぞれ正常であるという命題とすると

￢(A∧B∧C)∧(A∧B1∧C)⇒￢B

によってBが原因であることを特定かつ証明できる。この論理式は常に真になる。取り替えてみてチャンと動けばOKと言う時の論理的根拠だ。しかし、

￢(A∧B∧C)∧(A∧B1∧C)⇒￢B1
￢(A∧B∧C)∧(A∧B1∧C)⇒￢A

では、偽になる部分があり見落としを指摘される。

ソフトの故障を確率的だ言う議論もあるが上記のような論法は成立するのでソフトの故障は決定論的だろう。キャッシュを使ったCPUにおけるソフトの実行時間は確率的と言っても良いが、それでも詳細に解析すれば場合の数が多いだけでその中のどれかに、条件を揃えることができれば確定する。条件を揃えると言うのはソフトウェアの外の話である。実際、おなじソフトをキャッシュ無しで動かせば確率的変動は取り除くことができる。で、これは取り替えてみてチャンと動くと言う論法で証明できる。

ソフトを含めたシステムで、そのシステムが正しく動いたとすれば、関連するモノ･コトの全てが正しいと言える。しかし、関連するモノ・コト全てを列挙することは不可能なので。検証可能なのは列挙できる要因だけになる。このことは、ある機能が正しいと言う命題をFとすると

F⇒A∧B∧C

と表現できる。前記の例をこの形式で書くと

(F⇒A∧B∧C)∧(F1⇒A∧B1∧C)∧￢F∧F1⇒￢B

となる。この場合、全ての場合でこの推論が成立するわけではなく、A, B, C, B1全てが正しい時が反例として検出される。すなわち、列挙できていない要因によってFが失敗した場合に対応する。ここで、FとF1はテスト結果と考えた方が良いかも知れない。

ソースコードの論理構造

要求を構造化した要求木と言う考え方を2010年2月号のインタフェース誌で紹介した。

要求管理ツールなどで要求のトレーサビリティを管理する例はあるが、それは単なる関係ではなくて論理的関係である。このことを利用して知識ベース化しようと言う考え方である。
今月のインタフェース誌(2010年4月号)はこの続きで、要求木の一番下のソースコードとの関係をプログラム検証ツールCBMC ( Bounded Model Checking for ANSI-C )を利用してソースコードも論理式にしてしまって要求木に組み込んで見ようと言う試みである。

上の図でCが左のソースコードの論理式表現になる。Rがアサーションでソースコードが満たすべき仕様になる。要求木の図ではReq6とかReq7にあたる。
CBMCはソースコードを論理化するのが目的ではなくPolySpaceと同じようなソースコード検証をするためのツールである。PolySpaceに比べるとフリーのツールなので使いづらいが、同じソースコードに対して同じ箇所の問題を指摘してくれる。ただし、PolySpaceと違って指摘の仕方がちょっと分かりづらい。また、Bounded Model Checkingを使っているので無限ループになることを検出するのは無理だ。

参考文献
[1] A Tool for Checking ANSI-C Programs,
http://www.kroening.com/papers/tacas2004.pdf
[2] astah 6.1 で「要求モデル」が目指している姿 T

原因結果グラフ-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]