個別の事例を対象としたモデル検査
M2012MM023

長谷康宏

指導教員：佐々木克巳

1

はじめに

定義 2.3 3 つ組 M = (S, R, V ) は，次の条件を満たすとき，クリプキモデルという．また，V を付値関数と呼ぶ．

本研究では，モデル検査に必要な準備をした上で，自分で選んだ製品である，電動ポットと自動車のルームラン (1) (S, R）はクリプキフレームプに対するシステムに対して，モデル検査を行った．モ (2) V : S × AP → {⊤, ⊥}デル検査に必要な準備には，[1],[2] を用いた．本稿では，自動車のルームランプシステムのモデル検査の例を挙げ 定義 2.4 クリプキフレーム F = (S, R) における（無限）る．2 節でモデル検査に必要な準備，3 節で CTL のモデ パスとは状態がなす無限の列 π = s0 , s1 , · · · であってル検査の手法，4 節で自動車のルームランプシステムの i = 0, 1, · · · に対して，si Rsi+1 となるもののことをいう．
例を説明する．
パス π = s0 , s1 , · · · に対して，その si から始まる末尾をπ i とかくことにする．すなわち，π i は無限パスで π i =2 モデル検査に必要な準備
si , si+1 , · · · である．また，無限パスの最初の有限部分を
ここでは，様相論理 CTL について説明する．
有限パスということにする．

2.1

CTL の論理式

この節では，様相論理 CTL の論理式について説明する．集合 AP を 1 つ定めておく．その元 p ∈ AP を原子論理式と呼ぶ．また，用いる論理記号は、∧, ∨, ⊃, ¬ とパス量化子 E, A と時相演算子 X, F, G, U, R である．パス量化子と時相演算子をあわせて様相演算子という．様相演算子で，自動車のルームランプの例で用いるもののみを，直観的な意味とともに以下にまとめておく．
パス量化子 Aψ ：すべてのパスにおいて（f or All）
時相演算子 Fψ ：ある未来（in the F uture ）
時相演算子 Gψ ：これからずっと（Globally ）CTL の状態論理式は，次のように定義する．以下，とくに必要のない限り， CTL の状態論理式を単に状態論理式という．
定義 2.1（CTL の状態論理式）(1) p ∈ AP ⇒ p は状態論理式(2) φ, ψ は状態論理式 ⇒ ¬φ, φ ∧ ψ, φ ∨ ψ, φ → ψ は状態論理式(3) φ, ψ は状態論理式 ⇒ AXφ, EXφ, AFφ, EFφ, AGφ,EGφ, A(φUψ), E(ψUφ), A(φRψ), E(φRψ) は状態論理式
2.2

CTL の意味論

定義 2.5 クリプキモデル M = (S, R, V ) が定まっている
とき，各状態 s ∈ S と各状態論理式 φ との関係 M, s |= φを論理式の構成に関して帰納的に定める．詳細は省略する．
定義 2.6 二つの状態論理式を φ と ψ とする．すべてのクリプキモデル M とそのすべての状態 s に対して M, s |=φ ⇐⇒ M, s |= ψ が成り立つとき，φ と ψ は論理的に同値であるといい，φ ∼= ψ と表す．
補題 2.1 CTL の 10 種類の様相演算子は，すべて EX,EG, EU の 3 種類を用いてかける．ここでは，EF, AG,AF についてのみ示しておく．
(1) EFφ ∼= E(TrueUφ)(2) AGφ ∼= ¬EF¬φ∼(3) AFφ = ¬EG¬φ
ただし，True は，勝手な p ∈ AP を決めた時の p ∨ ¬p の略記である．

3CTL のモデル検査

ここでは，[1] にしたがって，CTL のモデル検査の手法について説明する．基本的なモデル検査の手法は，以下に示すとおりである．

モデル検査の手法(I) 検証したいシステムをクリプキモデル M として表す．
この節では，様相論理 CTL の意味論について説明する．クリプキフレームとそのフレームにおける CTL の (II) 検証したい性質を状態論理式 φ として表す．
論理式の真偽を定めたクリプキモデルを定義する．
(III) モデル検査問題を解いて，状態の集合 S(φ) = {s |M, s |= φ} を求める．公平性制約を加える場合もあ
定義 2.2 空でない集合 S と S 上の二項関係 R の組 (S, R)
る．この集合の中に初期状態（システムの実行開始をクリプキフレームという．S の各元を可能世界または時の状態）が入っていれば，検証したい性質の正し状態と呼び，R を到達可能関係と呼ぶ．
さが保証される．
上の (I),(II),(III) を，以下の 3.1 節,3.2 節,3.3 節で説明する．ただし，(III) の公平性制約については，3.4 節で説明する．

3.1

システムをクリプキモデル M で表すと解釈し，クリプキモデルのパスを用いて表現すると，• 「すべてのパスにおいて，「電子レンジのスタートボタンを押せば，すべてのパスにおいて，ある未来必ず中の物が温まる」」

この節では，検証したいシステムをクリプキモデル Mとして表現することを，例を挙げて説明する．
である．よって，これを状態論理式で表すと，
図 1 は，電子レンジのシステムを状態遷移図で表現しAG(Start → AFHeat)たものである．この状態遷移図における 7 つの四角がシである．
ステムの状態を表し，矢印がシステムの計算過程を表す．
各状態にかかれている Start,Close,Heat,Error 等の意味 3.3 S(φ) を求める
は以下のとおりである．
この節では，検証したしたい論理式 φ に対して， S(φ)• Start：電子レンジのスタートボタンが押されている を計算するアルゴリズムについて説明する．補題 2.1 よ• Close：電子レンジのドアが閉まっている
り，チェックしたい CTL の状態論理式 φ は• Heat：調理するものが温まっている• Error：エラーになっている• ∼：でないp(p ∈ AP), ¬φ, φ ∨ ψ, EXφ, E(φUψ), EGφの形に制限されているとしてよい．
S(EGφ) を求めるのには，次の準備が必要である．
定義 3.1 クリプキフレーム F = (S, R) の強連結成分とは C = (S ′ , R′ ) で次の条件を満たすもののことをいう．

(1) C は F の部分フレームである．すなわち，S ′ ⊆S,R′ ⊆ R ∩ (S ′ × S ′ ) である．
(2) C は強連結である．すなわち，任意の状態 s, s′ ∈ S ′に対して，s から s′ への C の中での有限パスが存在する．

図 1 電子レンジの状態遷移図（出典 [1]）これらの構成要素をクリプキモデルでは，

1. システムの状態をクリプキモデルの状態 s ∈ S
2. システムの計算過程をクリプキモデルの到達可能関係
R(3) C は極大である．すなわち，C ⊆ C ′ でかつ C ′ が強連結ならば，C ′ = C である．
さらに，この強連結成分 C が非自明とは次のようでない
こという．
(4) S が 1 点集合，かつ，R = ∅ である．
この節の冒頭で示した 6 つの形の状態論理式に対して，次の定理が成り立つので，S(φ) を，論理式 φ の構成にしたがって計算することができる．この定理の (2) については，4 節での計算をしやすくするために加えている．
定理 3.1 M = (S, R, V ) をクリプキモデルとする．

3. Start, Close, Heat, Error を AP の要素(1) φ = p ∈ AP のとき，S(p) = {s ∈ S | V (s, p) = T }4. 「Start, · · · が四角 s の中にかかれていること」を
V (s, Start) = ⊤, · · ·(2) φ = ψ ∧ χ のとき，S(ψ ∧ χ) = S(ψ) ∩ S(χ)

5. 「∼ Start, · · · が四角 s の中にかかれていること」を
V (s, Start) = ⊥, · · ·と解釈する．この解釈によって，検証したいシステムをクリプキモデルとして表現できる．
3.2

検証したい性質を状態論理式 φ として表す

この節では，図 1 のシステムにおける検証したい性質の例を挙げて，それを状態論理式で表現する．
検証したい性質は，• 「電子レンジのスタートボタンを押すと必ず中の物が温まる」という性質である．これを• 「これからずっと「電子レンジのスタートボタンを押せば，いつか必ず中の物が温まる」」(3) φ = ψ ∨ χ のとき，S(ψ ∨ χ) = S(ψ) ∪ S(χ)(4) φ = ¬ψ のとき，S(¬ψ) = S\S(ψ)(5) φ = EXψ のとき，S(EXψ) = {s ∈ S | ある s′ ∈ S が存在して，(s, s′ ) ∈ R かつ s′ ∈ S(ψ)}(6) φ = E(ψUχ) のとき，状態 s ∈ S(χ) のそれぞれからスタートして，R をさかのぼっていく．さかのぼっていくうち ψ が成り立っているうちは，その状態をS(E(ψUχ)) に加えていく．
(7) φ = EGψ のとき，S(EGψ) は，次の 2 条件を満たす状態 s ∈ S を全部集めた集合(a) s ∈ S(ψ)(b) (S(ψ), R(ψ)) の中に非自明な強連結成分 C があって，かつ s から C の中の状態 t に至る

(S(ψ), R(ψ)) の中の有限パスが存在する．

(1) M, s |=FC Fair ⇔ s から始まる公平なパスが存在する

ただし，
R(φ) = R ∩ (S(φ) × S(φ))
である．

(2) (p ∈ AP) に対して， SFC (p) = S(p ∧ Fair)

3.4(4) φ = ψ ∨ χ のとき，SFC (ψ ∨ χ) = SFC (ψ) ∪ SFC (χ)

公平性制約

この節では，公平性制約について述べる．3.2 節の状態論理式を ψ としたとき，3.3 節の方法で，S(ψ) を計算すると，S(ψ) = { } になる．これはモデル検査が失敗したことを表す．その理由は，「ドアをずっと開けたり閉めたり」というパスがあるためである．そこで，このようなパスは排除したい．このようなパスは，公平性制約をうまく定めることによって排除できることがある．
定義 3.2(3) φ = ψ ∧ χ のとき，SFC (ψ ∧ χ) = SFC (ψ) ∩ SFC (χ)(5) φ = ¬ψ のとき，SFC (¬ψ) = S\SFC (ψ)(6) φ = EXψ のとき，SFC (EXψ) = {s ∈ S | ある s′ ∈S が存在して，(s, s′ ) ∈ R かつ s′ ∈ SFC (ψ)}(7) φ = E(ψUχ) のとき，状態 (s ∈ SFC χ ∧ Fair) それぞれからスタートして，R をさかのぼっていく．さかのぼっていくうち ψ が成り立っているうちは，その状態を SFC (E(ψUχ)) に加えていく．
(8) φ = EGψ のとき，SFC (EGψ) は，次の 2 条件を満たす状態 s ∈ S を全部集めた集合(1) M = (S, R, V ) をクリプキモデルとするとき，集合{S ′ | S ′ ⊆ S} を M 上の公平性制約という．

(a) s ∈ SFC (ψ)(2) M のパス π = s0 , s1 , · · · に対して，状態の集合 inf (π)
を inf (π) = { s ∈ S | 無限にたくさんの i ≥ 0 に対して，s = si } と定める．

(b) (SFC (ψ), RFC (ψ)) の中に非自明で公平な強連結成分 C があって，かつ s から C の中の状態 tに至る (SFC (ψ), RFC (ψ)) の中の有限パスが存在する．

(3) M のパス π = s0 , s1 , · · · が公平性制約 FC について公平であるとは次が成り立つことをいう．
すべての P ∈ FC に対して，inf (π) ∩ P 6= ∅ただし，RFC (φ) = RFC ∩ (SFC (φ) × SFC (φ))
Fair = EGTrueである．

集合

FC ＝ {{s | s |= Start ∧ Close ∧ ¬Error}}

4

自動車のルームランプシステムの例

は，3.1 節の電子レンジシステムにおける，公平性制約のここでは，自動車のルームランプシステムを例に挙げ，例である．この制約で「ドアの開け閉め」のパスを排除
前章の冒頭で示した手順で，モデル検査を行う．
できる．その理由をおおまかに述べておく．まず，図 3.1
より，FC = {{6, 7}} である．よって，「ドアの開け閉め」(I) 図 2 は，自動車のルームランプシステムの状態遷移図でによるパスであるある．システムの状態は，7 つの文 on,switch, brightlight,
1, 3, 1, 3, · · · や 2, 5, 2, 5, · · ·key open, door open, darklight, error で決定される．各は FC について公平でないとわかる．すなわち，公平な 文の意味を示す．
パスのみを考えることにより，これらのパスを排除でき• on：ルームランプのスイッチが押されているることになる．
• switch：ルームランプが点滅している
定義 3.3 クリプキモデル M = (S, R, V ) と公平性制約
FC を定めたとき，CTL の状態・パス論理式 φ が M とFC のもとで真であるという関係 M, s |=FC φ を論理式の構成に関して帰納的に定める．詳細は省略する．

SFC (φ) = {s ∈ S | M, s |=FC φ} とする．以下，3.3 節と同様に SFC (φ) を求める方法を示す定理を述べる．
定義 3.4 M = (S, R, V ) をクリプキモデル，FC をその上の公平性制約とする．クリプキフレーム (S, R) の強連結成分 C が公平であるとは，各 Pi ∈ FC について
C ∩ Pi 6= ∅ が成り立つことをいう．
定理 3.2 M = (S, R, V ) をクリプキモデル，FC をその上の公平性制約とする．

• brightlight：ルームランプが全点灯している• darklight：ルームランプが半点灯している• key open：車の鍵が開いている• door open：車のドアが開いている• error ：エラーになっている
7 つの要因があるので，27 = 128 通りの状態が考えられる．図 2 では，128 通りのうち 9 通りを対象としたシステムを表している．以下，7 つの文を AP の要素とし，3.1
節と同様に，図 2 の状態遷移図をクリプキモデルとして考える．
(II) 検証したい文は，「解錠したら, 明るいルームランプまたは暗いルームランプが必ず点灯する」という文である．
これを論理式で表現すると，AG(key open → AF(darklight ∨ brightlight))

S(ψ) が空集合になったので，モデル検査はうまくいかなかった．
公平性制約がある場合を考える．公平性制約を「ルームランプのスイッチが常にオンでかつ，車の鍵が開いている」
つまり，FC = {{s | s |= on ∧ key open}} = {{5, 7, 8}}とする．この FC のもとで SFC (ψ) を求める．
(1) 1 からはじまる公平なパス 1, 2, 5, 7, 5, 7, · · · がある．
(∵ 図 2, 定義 3.3)
(2) 各状態からはじまる公平なパスがある．
(∵ 図 2, 定義 3.3)
(3) SFC (Fair) = {1, 2, 3, 4, 5, 6, 7, 8, 9}(∵ (1), (2), 定理 3.2(1))(4) SFC (darklight) = {5} (∵ (3), 定理 3.2(2))(5) SFC (brightlight) = {7, 8}(∵ (3), 定理 3.2(2))(6) SFC (darklight ∨ brightlight) = {5, 7, 8}(∵ (4), (5), 定理 3.2(4))(7) SFC (¬(darklight ∨ brightlight))= {1, 2, 3, 4, 6, 9} (∵ (6), 定理 3.2(5))(8) SFC (¬(darklight ∨ brightlight)) の任意の部分集合 C に対して，C ∩ {5, 7, 8} = ∅(∵ (7))(9) SFC (¬(darklight ∨ brightlight)) の公平な強連結成分は存在しない． (∵ (8), 定義 3.4)
図 2 ルームランプシステムの状態遷移図である．この論理式を φ とおく．

(10) SFC (EG¬(darklight ∨ brightlight)) = {(∵ (6), (9), 定理 3.2(8))}(11) SFC (key open) = {4, 5, 6, 7, 8, 9}(∵ (3), 図 2)(12) SFC (key open ∧ EG¬(darklight ∨ brightlight))= { } (∵ (10), (11), 定理 3.2(3))(III) まず，補題 2.1 より φ の AG, AF を EU, EG で表現した状態論理式 ψ を求めると以下のようになる．
(13) SFC (E(TrueU(key open ∧ (EG¬darklight ∨¬E(TrueU(key open∧(EG¬(darklight∨brightlight))))brightlight)))) = { } (∵ (12), 定理 3.2(7))
次に，S(ψ) を求める．ここでは，公平性制約は考えない．
(14) SFC (ψ) = {1, 2, 3, 4, 5, 6, 7, 8, 9}(1) S(darklight) = {5} (∵ 図 2)(∵ (13), 定理 3.2(5))(2) S(brightlight) = {7, 8} (∵ 図 2)
(3) S(darklight ∨ brightlight) = {5, 7, 8}(∵ (1), (2), 定理 3.1(3))(4) S(¬(darklight ∨ brightlight)) = {1, 2, 3, 4, 6, 9}(∵ (3), 定理 3.1(4))(5) {1, 2, 4, 6, 9} は，S(¬(darklight ∨ brightlight))の強連結成分である． (∵ (4), 定義 3.1)
(6) S(EG¬(darklight ∨ brightlight))= {1, 2, 3, 4, 6, 9} (∵ (4), (5), 定理 3.1(7))

SFC (φ) = SFC (ψ) = {1, 2, 3, 4, 5, 6, 7, 8, 9} になったので，公平性制約 FC のもとで，モデル検査が成功した．

5

おわりにモデル検査の研究では，モデル検査を行うまでの準備が大変あると感じた．特に状態遷移図の作成で製品の状態を網羅できているかというところで苦労した．
今後，モデル検査の準備段階をスムーズに行えば，確実で，迅速な製品の品質保証ができると思った．

(7) S(key open) = {4, 5, 6, 7, 8, 9} (∵ 図 2)

参考文献

(8) S(key open ∧ EG¬(darklight ∨ brightlight))= {4, 6, 9} (∵ (6), (7), 定理 3.1(2))[1] 蓮尾一郎：『モデル検査入門』．http://www.kurims.kyoto-u.ac.jp/ cs/lecture2009/lecture09ModelChecking.pdf(9) S(E(TrueU(key open ∧ EG¬(darklight∨ brightlight)))) = {1, 2, 3, 4, 5, 6, 7, 8, 9}(∵ (8), 定理 3.1(6))(10) S(ψ) = { }(∵ (9), 定理 3.1(4))[2] Edmund M. Clarke, Jr., Orna Grumberg, and Doron
A.Peled：Model Checking．The MIT Press, London,
1999．