2011/03/27

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文が使いやすい。

2011/03/23

NuSMVで階層化状態マシン

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

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

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

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

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

∈ 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モデルを作ることができる。





2011/03/21

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

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




2011/02/11

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 = p1p3p6.  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.