修 士 論 文 概 要 書 Summary of Master’s Thesis

専攻名（専攻分野）

Department

研究指導名 Research guidance

氏名 Name 学籍番号 Student ID

number

指 導 教 員 Advisor

印 Seal

研究題目 Title

Date of submission: 1 / 31 / 2012 (MM / DD / YYYY)

修 士 論 文 概 要 書

Summary of Master’s Thesis

CD 5110B063 – 9 情報理工学

並列知識情報処理

清水 涼子

上田 和紀

     Explicit-time methodに基づくモデル検査器SLIMのリアルタイムシステムモデル検査器への拡張

1 研究の背景と目的

システムの挙動に関して実時間制約をもつリアルタイ ムシステムは， 手作業による検証が容易でないことから，

ツールによる検証が重要になってくる．リアルタイムシ ステムのモデリングには，implicit-time methodとexplicit-

time methodに大別される．前者は，時間の概念が組み込

まれた表現体系を利用するもので,既存のリアルタイムモ デル検査器の多くはこちらの手法を基礎にしている．一方 後者は，リアルタイムシステム向けでない通常の言語・モ デル検査器の上で，現在時刻を明示的に表す変数を用い てモデリングを行う．本研究の目的は，そのモデル検査器 SLIM上でExplicit-time methodを使用したリアルタイム モデル検査を行うための拡張を行い，その評価をすること である．

2 モデリング言語 LMNtal とモデル検 査器 SLIM

LMNtalは，データ構造をルールと呼ばれるプロセスが

書き換えていくことで処理が進行する．LMNtalコンパイ ラはソースコードをLMNtal抽象機械の中間命令列に変換 する．SLIMはこの中間命令列を解釈実行するほか，すべ ての書換え方法を試みて全状態空間を構築する非決定実行 機能と，本機能を拡張したLTLモデル検査機能が備わって いる．非決定実行機能とLTLモデル検査器機能は共有メ モリ計算機向けの並列化が施され，良好な並列効果が達成 している．

3 Explicit-time method

Explicit-time methodを簡潔に説明すると，現在時刻を インクリメントするプロセスTickをモデルへ導入し，これ らにより時間の経過を制御するというものである．Tickは システムの仕様が離散時間である場合1ずつ時刻をインク リメントする．時間の制約はカウントダウンタイマー変数 によって表現する．

if(∀t∈Thread(ubTimer[t]>d))then atomic{

now=now+d;

foreach(t)

if(ubTimer[t]=∞)then ubTimer[t]=∞;

elseubTimer[t]=ubTimer[t]−d;

foreach(t)

lbTimer[t]=max(lbTimer[t]−d,0);

}

図1 Tickアルゴリズムの例

4 リアルタイムシステムのエンコード

Explicit-time methodを使用し，代表的なリアルタイム システムの例題のLMNtalにおける記述を行いSLIMで モデル検査を行えることを確認した．エンコードをした 例題は，Fischerのアルゴリズム，Leader election protocol, train-gate, PAR protocol ,FDDI protocolである．その際に，

LMNtalでの記述に問題があった．

4.1 問題点

LMNtalの言語仕様では，プロセスTickのアルゴリズム

が簡潔に記述できなかった．Tickアルゴリズムの一例を図

1に示す．LMNtalで図1を実装するには，複数のルール

で記述しなくてはならない．しかし，ルールはそのままで は非決定的に実行されてしまう．また，プロセスT ickは モデル検査の観点から，1ステップで実行するのが望まし かったため，複数のルールを中間命令列にコンパイルした 後，図1の振る舞いをするよう，中間命令列を手で書き変 えていた．さらに，Tickでは全てのタイマーを参照・更新 するため，記述が冗長になりがちである．

4.2 LMNtal 拡張言語の導入

これらの問題を解消すべく，LMNtal 拡張言語を導入 した.

■集合記法 同一構造のLMNtalプロセスを繰り返し記述 するときに，この集合記法を使うとプログラムコードが簡 略化できる．この集合記法は次のように記述する．

#If

##[[ubTimer(%i)=T%i]]| i in 0..5 ## , \ :-

##[[T%i>1]]|i in 0..5 ##| .

#Then

##[[ (lbTimer(%i)=T1 :- T1>0, T2=T1-1 | lbTimer(%i)=T2),

(ubTimer(%i)=T1 :- T1=\=1000, T2=T1-1|

ubTimer(%i)=T2 ]]| i in 0..5 ##.

#End If

図2 LMNtalマクロを使用して記述したTick

"!"

#$%$ &&('

)%'+*

図3 Fischerのアルゴリズムのsafetyの実行時間

##[[process|set]]##

process中の置換指定子の部分を，setの要素で置換したも

のを全ての要素について列挙する．

■中間命令列制御構造 Tickを実装するための手作業を自 動化するため，次のような中間命令列操作のための制御構 造を用意した．この構造を適用すると，guardruleは全体 の実行をガード条件的なルールになり，guardruleの適用 に成功するとThen以下のルールが並び順に1回ずつ，そ れぞれの成否にかかわらずrulemまで実行される1ステッ プのルールのように実行される．

#Ifguardrule #Thenrule1. . .rulem(m>0) #End If 図1をこのマクロ言語を使用して記述したものを図 2で ある.

5 評価

記述したリアルタイムシステムの例題のうちFishcer の ア ル ゴ リ ズ ム と leader election protocol に つ い て ， SLIMとリアルタイムモデル検査器であるUPPAAL[2],

TLC[3]の間でモデル中のパラメータを変化させ時間性

能の測定を行い比較した．実験は，OS CentOS 5.4, CPU AMD Opteron(tm) Processor 6176 SE, 48CPUsメモリ容量

256GBである共有メモリ並列計算機にて行った．

■Fischerのアルゴリズム Fischerのアルゴリズムは,極 めてシンプルな時間制約を利用した，スレッドの排他制御 のアルゴリズムである．この例題に関し，safetyの実験結 果を図3に掲載する．

図3より，TLCとSLIMの実行時間が同様に推移してい

! #"%$'&

)(*,+-. /0(2143/57689 :4;'(, -5<6=89:>

?A@4B CD

EF@4B CD

EHG@4BCD

GJIJ@4BCD

K;LNM

OPJPAQQL

図4 Leader election protocolのsafetyの状態数と実行時間[s]

ることから，SLIMへのexplicit-time methodによるリアル タイムシステムのモデル検査が妥当に行われたといえる．

UPPAALは，パラメータに依存せずごく短い時間で検査で

きる一方，explicit-time methodによる検査はパラメータが 大きくなると，状態数が増加するので，時間も増加する．

図3から，SLIMは使用するコア数に比例した時間性能に なっている．

■Leader election protocol Leader election protocolは文 献[1]にて取り上げられているネットワークの分散アルゴ リズムの例題である．この例題では，十分な時間が経過し たときにアルゴリズムが安定状態になるかについて到達性 検査を行う．

図4に実験結果を示す．UPPAALの測定結果の中で，3 つのケースでout of memoryにより検証中止になってい る．全体的にみてもUPPAALをほとんどのパラメータで SLIMやTLCが時間性能で上回った．UPPAALの性能は，

並行に動作しているタイマー数に依存するため，モデル中 のタイマーの数が増えると性能が悪化するためと考察され ている[1]．

6 まとめと今後の課題

Explicit-time methodを使って代表的なリアルタイムシ ステムの例題をLMNtalへエンコードすることで，SLIM でリアルタイムモデル検査が行えることを確認した．そ の上で，リアルタイムシステムモデル検査を簡単に行える

LMNtalマクロ言語を設計・実装した．

今後の課題点としては，まず，今回用意したマクロだけ では十分に記述できない例題もあるので，その部分に対 する対応を考えたい．さらなる課題点としては，今後この SLIMのリアルタイム拡張を発展させていくため，処理系 の中で時間概念を特別扱いし，それに対するモデル検査ア ルゴリズムを用意することが考えられる．

参考文献

[1] Lamport, L., Real time is really simple.

TechnicalReport MSR-TR-2005-30, Microsoft Research, March 2005.

[2] Larsen, K. G., Pettersson, P. Yi, W., UPPAAL in a nutshell.

Int. J. of Software Tools forTechnology Transfer, Vol. 1, No. 1–2, pp. 134–152, 1997.   

[3] http://www.tlaplus.net/tools/tla-tools/The