講義資料 - 筑波大学

LTL の意味論
LTL を使ったモデル検査
LTL の意味論
LTL を使ったモデル検査
目次
システム検証論
− モデル検査によるシステム検証−
1
LTL の意味論
2
LTL を使ったモデル検査
亀山幸義
筑波大学コンピュータサイエンス専攻
LTL の意味論
LTL を使ったモデル検査
クリプケ構造
LTL の意味論
LTL を使ったモデル検査
LTL の意味論
クリプケ構造 M = (S, S0 , Atom, R, L)
LTL
S: 「状態」の集合。通常は有限集合。
パス π に対する真理値
S0 : 「初期状態」の集合。S0 ⊂ S
Atom: 「原子命題」の有限集合。Atom = {p, q, . . . }.
R: 「遷移関係」。S 上の 2 項関係で、s1 → s2 を表す。
M, π |= φ
クリプケ構造 M におけるパス (path):
π = s0 , s1 , s2 , . . . ただし ∀i . (si → si +1 ) ∈ R. (ここでは
s0 ∈ S0 ということは、要求しない。)
L: 「ラベル関数」L(s) は状態 s において真である原子命題
の集合。
π(i ) は π の i 番目の状態 si .
様相論理における「フレーム」にラベル関数と初期状態を追加し
たもの。(世界の集合 W を、状態の集合 S に名前換え)
有限オートマトンとも類似。
LTL の意味論
LTL を使ったモデル検査
LTL のクリプケ意味論-2
π i は π の先頭から i 個を除いたパス si , si +1 , . . . .
LTL の意味論
LTL のクリプケ意味論-2
M, π |= φ: クリプケ構造 M のパス π での φ の真理値は以下の
通り。
M, π |= X φ は、M, π 1 |= φ と同じ真理値。
M, π |= F φ が真となるのは、
ある i があって、M, π i |= φ となる時。
M, π |= p は p ∈ L(π(0)) と同じ真理値。
M, π |= ¬φ は、M, π |= φ の値の否定。
M, π |= G φ が真となるのは、
すべての i に対して、M, π i |= φ となる時。
M, π |= φ ∧ ψ は、M, π |= φ と M, π |= ψ の論理積 (and).
M, π |= φ ∨ ψ は、M, π |= φ と M, π |= ψ の論理和 (or).
LTL の意味論
LTL を使ったモデル検査
LTL を使ったモデル検査
LTL のクリプケ意味論-3
LTL の意味論
LTL を使ったモデル検査
LTL のクリプケ意味論-4
最終的に、M |= φ を以下で定める。
M, π |= φUψ が真となるのは、
ある i があって、M, π i |= ψ となり、かつ、0 ≤ j < i となる
全ての j に対して、M, π j |= φ となる時。
M, π |= φW ψ が真となるのは、
M, π |= φUψ が真となるか、あるいは、0 ≤ j となる全ての j
に対して、M, π j |= φ となる時。
M, π |= φRψ が真となるのは、
ある i があって、M, π i |= φ となり、かつ、0 ≤ j ≤ i となる
全ての j に対して、M, π j |= ψ となる時、あるいは、0 ≤ j と
なる全ての j に対して、M, π j |= ψ となる時。
π(0) ∈ S0 となる、全ての M におけるパス π に対して
M, π |= φ となるとき真である。
そうでないとき (1 つでも上記を満たさないパスがあると
き)、偽である。
言葉で言いかえると:
M の初期状態から始まる全てのパスに対して φ が真である
とき、φ は M で真である。
(CTL を知っている人向けの補足: 「全てのパス」を考えるので、
LTL 論理式 φ は、一番外に暗黙のうちに A オペレータがついてい
る、と見なせる。)
LTL の意味論
LTL を使ったモデル検査
例題の改良モデル
LTL の意味論
LTL を使ったモデル検査
LTL と CTL の表現力
s0
n1,n2
LTL と CTL は論理としては、互いに比較不能。
s5
s1 t1,n2
AGEF φ は CTL のみで表現可能。
n1,t2
(GF φ) → F ψ は LTL のみで表現可能。
s2 c1,n2
s3 t1,t2
t1,t2
システムやハードウェア、通信プロトコルの検証では CTL モ
デル検査がよく用いられる。
s6 n1,c2
s9
s4
ソフトウェアの検証では LTL モデル検査がよく用いられる。
LTL と CTL を真に包含する論理として、 CTL* がある。
s7 t1,c2
c1,t2
状態 s3 を 2 つの状態 s3 と s9 に分ける。
s1 → s3 → s4 は許すが，s1 → s3 → s7 は許さない．
活性: G (t1 → Fc1) が s0 で真になる。
LTL の意味論
LTL を使ったモデル検査
LTL と CTL の表現力
LTL の意味論
LTL を使ったモデル検査
目次
AGEF φ は LTL で表現できない。
not p
p
1
LTL の意味論
2
LTL を使ったモデル検査
not p
(GF φ) → F ψ は CTL で表現できない。
相互排除の例 (最初の例) で、GF (t2 → Xc2) → G (t2 → Fc2).
LTL の意味論
LTL を使ったモデル検査
LTL モデル検査
LTL の意味論
LTL を使ったモデル検査
モデル検査とは？
モデル検査問題:
モデル M と時相論理式 φ が与えられたとき、
システムと仕様のモデル化
M |= φ であるかどうかを判定する問題。
システム: クリプケ構造として記述。
仕様: LTL 論理式として記述。
モデル検査アルゴリズム:
モデル検査
入力: モデル M と時相論理式 φ
仕様が成立するとき「真」を返す。
仕様が成立しないとき「偽」を返す。
「偽」のときは、更に反例を返す。
出力: M |= φ が成立するかどうか。
出力のおまけ: 不成立のときには、反例も得られる。
モデル＝クリプケ構造、あるいは、変換するとクリプケ構造にな
るもの。
LTL の意味論
LTL を使ったモデル検査
モデル検査器 (モデル検査ツール)
LTL の意味論
モデル検査の演習
モデル検査を行うソフトウェア.
SMV - Symbolic Model Verifier
CTL モデル検査器、最初の記号モデル計算器。
Ed Clarke の当時の学生 Ken McMillan が開発。
その後、NuSMV, Cadence SMV などの派生システムが発生。
NuSMV
イタリアの Torento のグループが開発。
広く利用。
CTL だけでなく、LTL モデル検査にも対応。
http://nusmv.fbk.eu/
他のモデル検査器
SPIN: LTL に対するモデル検査器, 特にソフトウェアモデル
検査。
UPPAAL: 実時間モデル検査。
本講義では、NuSMV Version2 (NuSMV2) を使う。
以下の場所に、演習の説明があります。
http://logic.cs.tsukuba.ac.jp/
~kam/lecture/sysverif2010/HOWTO.txt
LTL を使ったモデル検査
LTL の意味論
LTL を使ったモデル検査
モデル記述例-1
LTL を使ったモデル検査
仕様記述例-1
-- test1
LTLSPEC G (request -> F (status = busy))
MODULE main
VAR
request : boolean;
status : {ready, busy};
ASSIGN
init(status) := ready;
next(status) :=
case
request : busy;
TRUE : {ready,busy};
esac;
LTL の意味論
LTL の意味論
-- test2
LTLSPEC F (status = busy)
-- test3
LTLSPEC G ((status = busy) -> F (status = ready))
-- test4
LTLSPEC request U (! (status = busy))
LTL を使ったモデル検査
モデル記述例-2
LTL の意味論
LTL を使ったモデル検査
仕様記述例-2
相互排除 (最初のバージョン):
MODULE main
VAR
pr1 : {normal, trying, critical};
pr2 : {normal, trying, critical};
ASSIGN
init(pr1) := normal;
init(pr2) := normal;
next(pr1) :=
case
(pr1=normal) : {normal,trying};
(pr1=trying) & (pr2=normal) : {trying,critical};
(pr1=trying) & (pr2=trying) : {trying,critical};
(pr1=trying) & (pr2=critical) : trying;
...
esac;
...
LTL の意味論
LTL を使ったモデル検査
演習
演習の課題は別途指示する。
-- safety
LTLSPEC AG ! ((pr1 = critical) & (pr2
-- livenss
LTLSPEC AG ((pr1 = trying) -> AF (pr1
-- non-blocking
LTLSPEC AG ((pr1 = normal) -> EX (pr1
-- no strict sequencing
LTLSPEC EF ((pr1 = critical)
& (E[(pr1 = critical) U
(! (pr1 = critical) &
E[(! (pr2 = critical))
U (pr1 = critical)]
= critical))
= critical))
= trying))
) ] ))

Download Report