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

である。

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