KRONOS – Model Checking of Real

Systems and Software Verification
16. KRONOS – Model Checking of
Real-time Systems
システム情報科学府情報工学専攻
荒木研究室修士2年住田辰雄
目次
•
•
•
•
•
•
16.0 KRONOS
16.1 KRONOSで何ができるのか？
16.2 KRONOSの要点
16.3 オートマトンの記述
16.4 同期積
16.5 モデル検査
2006/10/16
モデル検査勉強会
2
16.0 KRONOS
• VERIMAGのS. Yovin, A. Olivero, C.
Draws and S. Tripakisらが開発
• モデル検査ツールはインターネットを通じ
て，利用可能である
2006/10/16
モデル検査勉強会
3
16.1 KRONOSで何ができるのか？
• TCTL論理のモデル検査ツールである
– 時間オートマトンに対する様々な性質の検査
– 論理式はテキスト形式で与えられる
2006/10/16
モデル検査勉強会
4
16.2 KRONOSの要点
1. KRONOSは時間時相論理に対するモデル検査アルゴリ
ズムを実装した数少ないツールの一つである
– 活性を検証することができる
– UPPAALやHYTECHのように到達可能性に制限されない
2. システムサイズの制限に加えて，グラフィカルやシミュ
レーションモードがない
• まとめ
– KRONOSは注目に値するパフォーマンスをもつ，真の時間モデ
ル検査ツールである
– しかし，形式手法に関する知識をもつ熟練者を対象にしている
2006/10/16
モデル検査勉強会
5
16.3 オートマトンの記述
• 踏み切りモデル
2006/10/16
モデル検査勉強会
6
16.3 オートマトンの記述
• 踏み切りモデル
– 電車
/* train1 */
#loc 3
#trans 3
#clocks x1
#sync app1 exit1
loc: 0
prop: far
inv: TRUE
trans : TRUE => app1; x1:=0; goto 1
loc: 1
prop: near
inv: x1<30
trans: x1>20 and x1<30 => enter; ; goto 2
loc: 2
prop: on
inv: x1<50
trans: x1>20 and x1<50 => exit1; ; goto 0
2006/10/16
モデル検査勉強会
7
16.4 同期積
• 遷移は空でないラベルの集合をもつ
– ラベルの組やリネーム操作は禁止している
• 同期ラベルは単にコンポーネントのラベル
の集合の和によって得られる
– 遷移集合の中の一つにある各ラベルが他の
遷移の（少なくとも）一つの集合に属している
ならば，遷移の集合は同期する
2006/10/16
モデル検査勉強会
8
16.4 同期積
• 例：
{a ,b}
 r1
– A1 : t1 : q1 
{b ,c}
 r2
– A2 : t2 : q2 
– bが同期ラベルの場合
{a ,b ,c}
 r1r2
• q1q2 
– 以下の遷移はない
{a ,b}
 r1q2
• q1q2 
• t1はt’2のような遷移と同期しなければならないが，t’2と同期す
るラベルが存在しないため，不可能である

– t2' : q2 
 q2
– ラベル集合が互いに素の場合には，基本的に同期遷
移は存在しない
2006/10/16
モデル検査勉強会
9
16.4 同期積
• A1とA2を同期させ，結果（A12）とA3を同期させる
kronos -out A12.tg A1.tg A2.tg
kronos -out A12A3.tg A12.tg A3.tg
– A(12)3
• 遷移をもたない
– A1(23)（A2とA3を同期させ，結果（A23）とA1を同期させる）
• 唯一の遷移ラベル{a,b}をもつ
2006/10/16
モデル検査勉強会
10
16.4 同期積
•
この問題を克服する方法
1. 与えられたシステムの全てのコンポーネント
を一回の操作で同期させる
kronos -out S.tg Tr1.tg Tr2.tg Gate.tg Contr.tg Ct.tg
2. 特別なオプション-sd（互いに素なラベルの集
合をもつ遷移を結果に追加する）を使用する
kronos -sd -out A12.tg A1.tg A2.tg
2006/10/16
モデル検査勉強会
11
16.4 同期積
2006/10/16
モデル検査勉強会
12
16.5 モデル検査
• 検査する性質はTCTL論理式を用いて記
述しなければならない
– それぞれの性質は，拡張子.tctlの別のファイ
ルに保存する
2006/10/16
モデル検査勉強会
13
16.5 モデル検査
• 安全性
– 電車が踏切内にいるときは，ゲートは閉じている
• init imple AB(on impl closed)
(safe.tctl)
– impl : 含意（=>）
– AとB : それぞれCTLのAとGに対応する
– 安全性を検証するKRONOSコマンド
• kronos –back S.tg safe.tctl
– 後方解析（オプション -back）によって得られた結果（今回は真）
を含むファイルsafe.evalが生成される
– 前方解析（オプション -forw）は，サイズの問題のため失敗する
2006/10/16
モデル検査勉強会
14
16.5 モデル検査
• 活性
– もう電車が到着しない瞬間から，ゲートはd単
位時間後に最後には開くだろう
• init  AG(near  on  E(near  on  open)U (>d) true))
• KRONOS（d = 20）
init impl
AB((not near and not on) impl
not ((not near and not on and not open) EU{>20} TRUE))
2006/10/16
モデル検査勉強会
15
16.5 モデル検査
• 活性
– V20.eval
kronos:
kronos:
kronos:
kronos:
begin evaluation of V20.tctl
end evaluation of V20.tctl
compacting
file V20.eval created
------------------------------------------------------------------kronos: fixpoint
: system 0.000s * user 0.030s * #iterations 5
kronos: compact time: system 0.000s * user 0.000s *
kronos: total time : system 0.000s * user 0.050s *
------------------------------------------------------------------2006/10/16
モデル検査勉強会
16
16.5 モデル検査
• 活性
– d=19の場合，性質を満たさない
• V19.tctlの評価
– 13回の反復が必要である
– 論理式V19を満たすシステムの状態を含む，Sat(V(19))
を生成する
– この性質は真でない
• 部分集合Sat(V(19))はシステムの全状態の集合と
等しくない
2006/10/16
モデル検査勉強会
17

Download Report