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

である。

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