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)) ) ] ))
© Copyright 2025 ExpyDoc