論文紹介：
Time Limited Model Checking
2006/10/18
上田研究室 M1
西村 光弘
1
Introduction
• 筆者の目標：以下の２面性をサポートする論理型言
語とmodel checking techniquesを見つけること
– 詳述性、検証性、正当性
– Reactiveかつ実時間のシステムをデザイン・実装
• ツールとしてのHybrid cc
– ハイブリッドオートマトンをhccプログラムに変換するメカニ
ズムが存在する
– オートマトンとして見ると、直感的に容易であるようなシス
テムをモデル化するにはとても向いている
2
Model Checking
• Reactiveなシステムの動きを検証可能
• アルゴリズムは到達可能性のある状態すべてを列挙し、
動きのすべてを分析する
• 利点
– 完全自動的
– 数学的な専門性が必要とならない
– 反例が返ってくる
Hcc + Model Checking techniques
↓
Hccで記述したシステムにModel Checkingを適用可
3
能にする環境の記述
• Model Checkingの適用するのに必要なこと
– Model Checking toolにほぼ受け入れられる形式にシ
ステムの仕様を変える
– 時間の概念と変数の初期値を使って、Model Checker
で操作されるような構造にグラフ構造を変換する
– デザインが適切な論理形式を満たすというプロパティ
からなっていること
↓ 注目していくところ
モデルを表現するための形式化
有限性を保証するための制限
4
Hybrid Concurrent Constraint
programming
Syntax
5
定義をみて伺えること
• 否定情報と決定した行動の実行が同時に
起こるから、強いプリエンプションをモデル
化できる
• プログラムのストアは有限の時間隔の間で、
無限の時間、変化できない→安定条件
6
• prevはinterval phaseが始まった点(point
phase)での制約の値を返す
• dot(X)はXの微分係数
7
Modelling
システムのプロパティを検証する際に初めにするこ
との一つは、システムのための正式なモデルを作
ること
– このモデルでは検証するつもりのプロパティを捉えるこ
とが必要
↓
システムの状態を捉える＝ある瞬間の変数値を含
むシステムの記述を捉える
↓
Hccを形式化することから初めて、状態遷移グラフ
を作り、最終的に時間の概念を含むこと
8
Basics
• ハイブリッドシステムの振る舞いを捉えるこ
とのできるグラフ構造を定義する（Kripke
Structure）
– Var：変数の全体集合
– V：V⊆Verで変数の集合
• システムのプロパティを記述したプログラムの節を
表す集合
• 各瞬間のプログラムの状態を記述した集合
– Var内の変数は型(boolean, integer,etc)をもつ
9
状態と遷移の集合を一階述語論理式で記述
• 遷移を(Ｒ(V,V’,T,A))と表す
– Ｔは、遷移がp→i, i→p, normal transitionのどれかを表
現する
– Ａは、今の遷移で、どのagentが実行されているかを教
えてくれる
• グラフ構造は制約の集合とラベルの集合
– 制約は変数の値を定義する。もし実数変数なら時間
の経過とともに値の変化を定義する
– ラベルはシステムの実行点を表し、その時のシステム
のストアに依存してactiveかdisabledになる
10
定義１．１
• Ｈｃｃのsyntaxで制約の集合をＣ
• 可能性のあるラベル全ての集合をＬ
↓
• 状態の集合をS⊆2C∪Lと定義する
11
定義１．２ Hybrid cc Structure
• APをatomic propositionの集合として、
Hybrid cc Structure M =(S,S0,T,A,R,L)
–
–
–
–
–
Sは状態の有限集合
S0はS0⊆S、Ｓの初期状態
T={n,p,i} 遷移の型の集合（pがp→Iのほう）
Aは各種のagentを表す命題の集合
RとLは次のページ
12
定義１．２ Hybrid cc Structure
– R⊆S×S×T×Aは遷移関係である
• 例：状態s,s’⊆S, agentのAがあったとすると、
R(s,s’,n,A) or R(s,s’,p,A) or R(s,s’,i,A)
– LはS→2AP
• 原子命題がその状態において真であるような状態
にラベル付けされた機能をLとする
• 状態の無限列をπ=s0s1s2・・・として、状態s
からのMのpathは
13
s0=s and R(si, si+1, X, Y) (∀i≧0)
Labelling
• Hccソースにラベル付けを行う
• Ｐはstatement
• Plは以下の表に従って変換できる
↓
14
Graph construction
• Hybrid cc Structure M =(S,S0,T,A,R,L)のグラフの
書き方
– nodeは状態、arcs(n,p,iの3種類)は遷移を表す
– 初期nodeでは、最初に実効される命令に相当するラ
ベルの集合を、ラベル付けした機能に割り当てる
– 各状態で、次ステップで実行されうる命令のラベルに
よってプログラムの実行点を表す
– ストアの中でactiveになっているラベルの集合を得る
機能revisionをもつ
15
• 各ラベルは異なる並行プロセスに相当し、activeか
disabledになる
– Active：このラベルに関連する操作が実行されるための状態が
満たされている時
– Disabled：storeが必要条件を満たしていないため、このラベルに
よって表される操作が、その時点では実行できない
• Ｈｃｃ計算はpointとinterval phaseの相互の順序である
• 各point phaseではDefault ccが実行され、それに対応して
特定の時点でのシステムのstoreを計算する
– 瞬間の計算では、プリエンプション操作に含まれない全ての
agentが実行されなければならない
– その後で、全てのプリエンプションagentが実行される（静止点に
到達するまでずっと）
– 最後にstoreにあるtemporal agentが実行される
16
• point phaseの終わりの一時的な操作の実行はPoint phase
からinterval phaseへの道筋に相当する
• 上記のphaseでは今のDefault ccの実行で更新される。同時
にask agentのガード条件が変わらない間の最小の時間間
隔も計算されている
• 一度、全てのagentを分析したら、時間間隔を得る。それか
ら、離散的変数値（他のプロセスによって修正されるかもし
れないため、どんな瞬間でも変わりうる）が安定したpathに
従って、次のpoint phaseへいく。
• 新nodeでは、時間を更新し、その瞬間の変数値を前の
interval phaseでの変数の限界値にセットする
• プログラムのglobalな処理時間で制約を課すためにuserが
特定した時間間隔を使う
– この制約がグラフ構造を有限にする
17
次の2つの場合を区別する
１つ目の場合
• 今の瞬間で、もしpoint phase（前の瞬間ですでに出現して
いて、もう一つのnode nによってグラフに表された）の終
わりとなる静止点があるのなら、
↓
今のnodeと、nがつなげられているのと同じnodeを結ばな
いといけない
• この場合、とても強い結果を得る
• userに特定された時間制限に到達したため、グラフの構
造をカットしなかったから、グラフは完結する
↓
つまり、システムはどんな動きも表す
18
もう一つの場合
• もし、今の静止点がグラフにまだ出現していなかったのなら、
– 構造を続けなければならない
– 今のnodeと、p-arcによってつなげられる新しいnodeを作らないといけない
– 次のinterval phaseの初期状態と比較して、storeと実行点を含む新しい
nodeを作らなければならない
• Userによって定められた時間制限に到達した場合、構造は終わり、か
つ、得られるモデルは現行の検証に対してだけ有効である
• そのモデルは異なる検証に対して再使用できない
• 仕様と実際のagentがあるとして、仕様内で後に続くagentがどれかを
決定するのは容易である
• 上記の目的で機能followを使う
• 機能revisionはどのラベルがactiveでdisabledであるかを決定するため
に定義される
19
20
Operator
• Tell：ある情報をstoreに加える操作
– グラフでは新しいnodeを作り、前の時点でのstoreに新
しい制約を加える
• Positive Ask：ガード条件がstore内で満たされて
いるかどうかを識別→満たされているならＡ実行
– グラフでは新しいnodeを作り、そのnodeには前の時点
の変数における制約を持ち続け、positive askの条件
を加える
– Storeに制約が加えられ、矛盾が生じるとプログラムの
実行をやめる
– 自分への矢印（ループ）はstoreがpositive askの条件を
取り入れない時をモデル化するときに使う
– bodyのラベルが加えられる
21
Oprator2
• Negative ask： (if a else A)でガードのaが今
のstoreで満たされないこと識別する→満た
されていないならＡ実行
– １：ガードのaがstoreから得られる時
• 新しいnodeを作り、そのnodeのラベルに条件aを加
え、実行されるagentの集合からnegative ask操作を
削除する
– ２：storeとdefault情報がagentのbody実行を許
す場合
• 別の１つのnodeを作り、negative askのbodyで表さ
れるラベルを加える
22
Operator3
• Hiding：変数の∃を表す
– グラフではstoreが変化しないが、ラベルは更新される
新しいnodeを作る
– 変数のリネーム情報は補助構造から導入される
• Parallel：言語の並行な振る舞いを表す
– 実行の異なる枝をつくる
– 一つのノードに対してActiveなラベルの数と同じ直系
の子ができる
• Hence：bodyのagentが今から後の各瞬間で実行
される
– ラベルは静止点に達するまでdesabledになる
– 今のnodeから新しいnodeをつくる（p-arc）
– Storeとlabel functionはhccによって計算される
23
定理１．３
グラフの正当性を証明する
• Hccの仕様Ｓから組み立てたHybrid cc Structure
をＴとすると
δ（Ｔ）⊆【S】
δ： （rootから始めて、一つのpathでの各hccのnode
のプログラムstoreの繋がりによって与えられる）Ｔ
のtraceを表す
【S】：hccの仕様Ｓのoperational semanticを表す
24
Transformation
• Hybrid cc Strutureのinterval phaseを線形ハイブ
リッドオートマトンのlocation(=節)とする
• 同様にpoint phaseをlocationをつなぐarcsとする
• 各locationにおいて、変数の集合と変数の微分
係数を、（interval phaseに対応して得られる）状態
によって定義する
• Invariantはinterval phaseで定義されたask agent
のガード条件の否定
25
• locationでプログラムが満たす最大時間間隔を課す制約
を加える。この限界はinterval phaseで計算される区間に
よって定義される
• 線形ハイブリッドオートマトンの各arcはHybrid cc Structure
のpoint phaseにあたる
• arcは２つのlocationを結ぶ（それぞれのpoint phaseの前と
次のinterval phaseを表す）
• 変数の集合は更新され、新しい値はpoint phaseで計算さ
れたstoreから得られる
• arcに関するラベルはpoint phaseからinterval phaseにいく
arcに関するラベル
• urgentラベルの集合はnull（この概念はhccでは使われな
いため）
• 最後に、synchronizationラベルには制限を課さず、各arc
に異なるラベルを割り当てる
26
27
Conclusions
• Hccのプログラムに対して、システムの振る舞い
をグラフ構造として表現を返す自動変換を定義し
た
• Hccのプログラムの意味論で安定性に基づいて
設計したので、point phaseとinterval phaseの一連
の順序通りに計算することが保証される
• 分析とそれに伴う制限を時間間隔に与えることで、
有限状態のmodel-checkerを使用できることを保
証できる
• 線形ハイブリッドオートマトンで制限をつけないよ
うなアルゴリズムを研究していく
28
© Copyright 2024 ExpyDoc
