NuSMVで非決定性状態マシン

非決定性の状態遷移があると実装には落とせないので、非決定性の有無は設計検証の対象になる。しかし、要求仕様の段階では非決定性のままで検証したいこともある。たとえば、ランダムな振る舞いをする外部デバイス等を環境モデルに取り込む場合などである。

ASSIGN
  next (s) :=
    case
       T_S1 : Sl;
       T_S2 : S2;
       T_S3 : S3;
       !inS & next(inS) : S1; -- start state
       TRUE : s;
    esac;


この状態マシンで、T_S1とT_S2が同時に真になった場合、NuSMVはcase式の最初の分岐しか使わないのでS2への遷移がおこなわれなくなる。そこで

ASSIGN
  next (s) :=
    case

       T_S1 & T_S2 : {S1, S2};
       T_S1 : Sl;
       T_S2 : S2;
       T_S3 : S3;
       !inS & next(inS) : S1; -- start state
       TRUE : s;
    esac;

の様にモデル化すれば良い。しかし、この方法は、非決定性遷移の数が少なければ良いが、増えてくると組合せ的に遷移条件数も増えるてしまう欠点がある。そこで、非決定性遷移が多い場合は、ASSIGN文ではなくTRANS文を使用する。TRANS文は論理式なので評価順と言うものが無い。


TRANS
(
(T_S1 & next(inS1)) |
(T_S3 & next(inS3)) |
(T_S2 & next(inS2)) |
(!T_S1 & !T_S2 & !T_S3 & next(s)=s)
)


TRANS
(
!inS & next(inS) -> next(s)=S1 -- start state
)

設計検証ではASSIGN文、要求検証ではTRANS文が使いやすい。

NuSMVで階層化状態マシン

NuSMVはSPINよりもモデル化の自由度が大きくUML等で出てくる階層化状態マシンをAND状態も含めてモデル化することができる。

まず、与えられた階層化状態マシンについて二つの集合を作成する。

Τ : root stateの集合、トップ状態とAND状態の子供
Α : atomic stateの集合とAND状態

ある状態 s について v(s)は直近の親を表すとする。Tは　v(s) = s ∈ T となるような集合。

Tの要素はNuSMVの列挙型変数とする。そして、列挙型の要素 b は、

a ∈ T の時に、v(b) ∈ a　となるようなb


によって構成される。

この状態図の場合


VAR

  M: {P, Q};

  R: {UI, U2, V};

  S: {Sl, S2, S3};

となる。

次に、以下の様な、その状態にいる時真になる様なマクロを定義する。全ての状態Bについて、

inB := TRUE;          Bはルート状態

inB := inA;           BはAND状態Aの子供

inB := inA & (A = B); BはΑの要素で、Bの親はTの要素

inB := inB1 | inB2 | . . . | inBk; BはOR状態でB1, B2,.., Bkはその子供、そしてBはTの要素ではない

上の状態図では

DEFINE
inM := TRUE;
inP := inM & (M = P);
inQ := inM & (M = Q);
inR := inQ;
inS := inQ;
inU := inU1 | inU2;
inU1 := inR & (R = U1);
inU2 := inR & (R = U2);
inV := inR & (R = V);
inS1 := inS & (S = S1);
inS2 := inS & (S = S2);
inS3 := inS & (S = S3);

そして遷移条件は、たとえばSの場合は

ASSIGN
  next (S) :=
    case
       T_SI : Sl;
       T_S2 : S2;
       T_S3 : S3;
       !inS & next(inS) : S1; -- start state
       TRUE : S;
    esac;

の様になる。ここでT_SxはSx状態への遷移条件である。MとRについても同様のASSIGN文を定義することでAND状態を含んだ階層化状態マシンのNuSMVモデルを作ることができる。

NuSMVでタイミング解析

モデル検査ツールのNuSMVを使用してタイミング解析が可能である。従来のCPU使用率に基づく手法に比べて悲観的な結果が出ることもなく、起動オフセットも含めて網羅的な検証が可能である。さらに、最小応答時間と最大応答時間を求めることもできる。ただし、従来の手法に比べて計算時間が長くなる。
Cheddarを紹介した際の問題をNuSMVで解いてみる。

まず、基本的な定数を定義する


DEFINE
C1:=20; C2:=40; C3:=100; -- Ciは実行時間
D1:=100; D2:=150; D3:=350; -- Diはデッドライン=起動周期

次に変数

VAR

c1:0..C1; -- ci: taskiの実行残り時間

c2:0..C2; 

c3:0..C3; 

d1:0..D1; -- di: デットラインまでの時間、起動オフセット

d2:0..D2; 

d3:0..D3;

そして、各タスクの状態の定義

-- Task1の状態定義

T1_rq := c1 < C1; -- Task1は実行中

T1_lv := c1 < C1 & d1 < D1 - 1; -- 実行中、次のJobはまだ起動されない

T1_lv_rls := c1 = C1 - 1 & d1 = D1 - 1;　　-- 実行中、次のJobがnext()で起動される

T1_slp := c1 = C1 & d1 < D1 - 1; 　　　-- 実行終了、次のJobはまだ起動されない

T1_slp_rls := c1 = C1 & d1 = D1 - 1; 　　　-- 実行終了、次のJobがnext()で起動される

T1_miss := D1 - d1 < C1 - c1; 　　　-- デッドラインオーバー

各タスクの状態遷移は、以下の様になる

next(c1) := case

T1_lv & T1_gp : c1 + 1;

T1_lv_rls & T1_gp | T1_slp_rls: 0;  

T1_slp | !T1_gp : c1;  

TRUE : 0;

esac;

next(d1) := (d1 + 1) mod D1;

タスク2と3については上記のコードのT1をT2, T3とすればよい。

デッドラインに関する検査式は

DEFINE

MISS:= T1_miss|T2_miss|T3_miss;

SPEC AG !MISS

の様になる。応答時間については

COMPUTE MIN[d1=0 & c1=0,c1=C1 - 1 & T1_gp]

COMPUTE MAX[d1=0 & c1=0,c1=C1 - 1 & T1_gp]

によって得ることができる。

検査した結果は

>nusmv task01.smv

*** This is NuSMV 2.5.2 (compiled on Fri Oct 29 11:40:52 UTC 2010)

*** Enabled addons are: compass

*** For more information on NuSMV see

*** or email to .

*** Please report bugs to

*** Copyright (c) 2010, Fondazione Bruno Kessler

*** This version of NuSMV is linked to the CUDD library version 2.4.1

*** Copyright (c) 1995-2004, Regents of the University of Colorado

*** This version of NuSMV is linked to the MiniSat SAT solver.

*** See http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat

*** Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson

-- specification AG !MISS  is true

-- the result of MIN [ (d1 = 0 & c1 = 0) , (c1 = C1 - 1 & T1_gp) ]  is 19

-- the result of MAX [ (d1 = 0 & c1 = 0) , (c1 = C1 - 1 & T1_gp) ]  is 19

-- the result of MIN [ (d2 = 0 & c2 = 0) , (c2 = C2 - 1 & T2_gp) ]  is 39

-- the result of MAX [ (d2 = 0 & c2 = 0) , (c2 = C2 - 1 & T2_gp) ]  is 59

-- the result of MIN [ (d3 = 0 & c3 = 0) , (c3 = C3 - 1 & T3_gp) ]  is 174

-- the result of MAX [ (d3 = 0 & c3 = 0) , (c3 = C3 - 1 & T3_gp) ]  is 239

の様になる。応答時間は、COMPUTE出力に+1した時間になる。

同じ問題をCheddarで検査した結果と一致している。Cheddarでは最悪応答時間しか求まらないがその結果は

20

40

240

である。

この方法は、マルチコアにも拡張することができる。

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はテスト結果と考えた方が良いかも知れない。

Cheddar: タイミング解析ツール

フリーのタイミング解析ツールCheddarを使ってみた。Windows版をダウンロードして解凍するとexeが出てくるのでそれをダブルクリックすれば立ち上がる。

一通り使えるだけの情報を提供するマニュアルもあるし、そこから関連する論文へのインデックスも付いているので時間を掛ければ色々面白いことができそうだ。
まず、プロセッサを定義する。Edit>Update Processorでスケジューラを指定する。RTOSの優先度ベースのスケジューリングに対応するのはHighest Priority Firstなので、これを選んでみる。この他にデッドラインモノトニックとか定番のモノが用意されている。Rate Monotonicを選べばタスク優先度を付けなくても良いので最初はこの方が良いかも知れない。独自に定義することもできる。

次にEdit>Update address spaceでメモリを定義する。取りあえず名前を付けるだけで先に進む。タスクとプロセッサとの対応付けはメモリによっておこなう様になっているのでメモリを定義しないとタスクの定義ができない。タスク定義はEdit>Update taskによっておこなう。適当な本に載っている例題を解いてみる。

以下の様にスケジュール可能であることが分かる。

これは使える。

implyとequivalent及びBranch coverageとDecision coverage

Twitterで話していたがまとめて話さないと伝わらないので、まとめてみる

ここに、Branch/Decision Testingという記事があって、冒頭に

For components with one entry point 100% Branch Coverage is equivalent to 100% Decision Coverage (入り口が一つのコンポーネントに対しては100%BCは100%DCと等しい)

と書いてある。

equivalentとは?
等しいのだからBDが100%ならDCも100%になりその逆も成立する。等価性には対称律が成立する。

入り口が複数あるとは?
構造化プログラム言語を使っていると関数の入り口は一つに決まっているが、昔のFortranのentry文を使うとサブルーチンの入り口を複数作ることができる。今でもOSのディスパッチャ等はマルチエントリの関数として実装されている。

この様な、プログラムでは100% Branch Coverage is equivalent to 100% Decision Coverageでは無くなる。

これとは別に


「デシジョンカバレッジとブランチカバレッジはお互いに、"A implies B"と定義されています。なので"A=B"となりますが、・・・」

と言うつぶやきがあり、これは違うでしょうと言ったのだけれど上の話と混ざってしまって140字では伝わらない。



implyとは?
implyとequivalentは違う。implyは片方向で、equivalentは両方向である。A implies B and B implies Aの時にequivalentと言って良い。これが対称律だ。

つまり

100%DC = 100%BC
DC⇒BC

は成立するが、

DC=BC

は成立しない。ここでBCと表しているのは、Branch/Decision Testingという記事で言えば

BC = {
B1 -> B2
B2 -> B3
B2 -> B9
B3 -> B4
B3 -> B5
B4 -> B8
B5 -> B6
B5 -> B7
B6 -> B8
B8 -> B2
}


と言う制御ブロック間の実行順序対の集合である。これは、元のプログラムのフローグラフの辺の集合として得ることができる。

一方、DCの方はプログラム内の論理判断の結果なので

DC = {

B2 -> B3

B2 -> B9

B3 -> B4

B3 -> B5

B5 -> B6

B5 -> B7

}

となる。従って

DC⇒BC

が成立していることが分かる。これは、DCの任意の要素を持ってくるとそれはBCの要素にもなっていると言う意味である。DCの要素ならばBCの要素でもある。これを省略して「DCならばBCである」と言うこともある。また

BC⇒DC

が成立していないことも分かる。これで、話は終わりかも知れないが、それなら100%DCだけど100%BCにならない例を見せてみろと尤もな突っ込みがあった。これは既に、シングルエントリの場合には、反例はないと言っているので、マルチエントリの場合を考えれば良いので、先のフローグラフの途中から実行を開始するようなパスを追加すれば良い。

だいたい
implyを暗黙に・・・等という訳の分からない日本語にするのが良くない。ことばを置き換えただけで分かったつもりになってしまう。

「ならば」と等価の区別はきっちり付けないといけない。アリバイがないから犯人にされてしまう世の中にはなって欲しくない。

カバレッジは幾つもあるが、そのカバレッジが定義する全体集合を実際に手で作って見れば色々なものが見えてくる。面倒くさいが実際に集合を作ってみて包含関係を見れば一目瞭然である。