論文紹介： Time Limited Model Checking

Presentation on theme: "論文紹介： Time Limited Model Checking"— Presentation transcript:

1 論文紹介： Time Limited Model Checking
2006/10/18 上田研究室 M1 西村　光弘

2 Introduction 筆者の目標：以下の２面性をサポートする論理型言語とmodel checking techniquesを見つけること
詳述性、検証性、正当性 Reactiveかつ実時間のシステムをデザイン・実装 ツールとしてのHybrid cc ハイブリッドオートマトンをhccプログラムに変換するメカニズムが存在する オートマトンとして見ると、直感的に容易であるようなシステムをモデル化するにはとても向いている P1 論理型言語は宣言的性質をもつということが、詳しく記述できることと実装の間の距離が小さくなる。それによって～性のプロセスが容易 Reactive：環境に制御される比率で環境に反応する

3 Model Checking Hcc + Model Checking techniques
Reactiveなシステムの動きを検証可能 アルゴリズムは到達可能性のある状態すべてを列挙し、動きのすべてを分析する 利点 完全自動的 数学的な専門性が必要とならない 反例が返ってくる P2 Hcc + Model Checking techniques ↓ Hccで記述したシステムにModel Checkingを適用可能にする環境の記述

4 Model Checkingの適用するのに必要なこと
Model Checking toolにほぼ受け入れられる形式にシステムの仕様を変える 時間の概念と変数の初期値を使って、Model Checkerで操作されるような構造にグラフ構造を変換する デザインが適切な論理形式を満たすというプロパティからなっていること ↓ 注目していくところ モデルを表現するための形式化 有限性を保証するための制限 P2下

5 Hybrid Concurrent Constraint programming
Syntax P3下 Tell Tell operatorは今現在aを持ってる、保持している

6 定義をみて伺えること 否定情報と決定した行動の実行が同時に起こるから、強いプリエンプションをモデル化できる
プログラムのストアは有限の時間隔の間で、無限の時間、変化できない→安定条件

7 prevはinterval phaseが始まった点(point phase)での制約の値を返す
dot(X)はXの微分係数

8 Modelling システムのプロパティを検証する際に初めにするこ との一つは、システムのための正式なモデルを作 ること
このモデルでは検証するつもりのプロパティを捉えることが必要 ↓ システムの状態を捉える＝ある瞬間の変数値を含 むシステムの記述を捉える Hccを形式化することから初めて、状態遷移グラフ を作り、最終的に時間の概念を含むこと

9 Basics ハイブリッドシステムの振る舞いを捉えることのできるグラフ構造を定義する（Kripke Structure）
Var：変数の全体集合 V：V⊆Verで変数の集合 システムのプロパティを記述したプログラムの節を表す集合 各瞬間のプログラムの状態を記述した集合 Var内の変数は型(boolean, integer,etc)をもつ

10 状態と遷移の集合を一階述語論理式で記述 遷移を(Ｒ(V,V’,T,A))と表す グラフ構造は制約の集合とラベルの集合
Ｔは、遷移がp→i, i→p, normal transitionのどれかを表現する Ａは、今の遷移で、どのagentが実行されているかを教えてくれる グラフ構造は制約の集合とラベルの集合 制約は変数の値を定義する。もし実数変数なら時間の経過とともに値の変化を定義する ラベルはシステムの実行点を表し、その時のシステムのストアに依存してactiveかdisabledになる

11 定義１．１ Ｈｃｃのsyntaxで制約の集合をＣ 可能性のあるラベル全ての集合をＬ 　　↓ 状態の集合をS⊆2C∪Lと定義する

12 定義１．２ 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は次のページ 原子命題「明日、太陽が東から昇る」「お隣の田中さんは犬を飼っている」などのように、それ自体で意味的に完結した単独の命題である。

13 定義１．２ 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は s0=s and R(si, si+1, X, Y) (∀i≧0)

14 Labelling Hccソースにラベル付けを行う Ｐはstatement Plは以下の表に従って変換できる ↓

15 Graph construction Hybrid cc Structure M =(S,S0,T,A,R,L)のグラフの書き方
nodeは状態、arcs(n,p,iの3種類)は遷移を表す 初期nodeでは、最初に実効される命令に相当するラベルの集合を、ラベル付けした機能に割り当てる 各状態で、次ステップで実行されうる命令のラベルによってプログラムの実行点を表す ストアの中でactiveになっているラベルの集合を得る機能revisionをもつ

16 各ラベルは異なる並行プロセスに相当し、activeかdisabledになる
Disabled：storeが必要条件を満たしていないため、このラベルによって表される操作が、その時点では実行できない Ｈｃｃ計算はpointとinterval phaseの相互の順序である 各point phaseではDefault ccが実行され、それに対応して特定の時点でのシステムのstoreを計算する 瞬間の計算では、プリエンプション操作に含まれない全てのagentが実行されなければならない その後で、全てのプリエンプションagentが実行される（静止点に到達するまでずっと） 最後にstoreにあるtemporal agentが実行される

17 point phaseの終わりの一時的な操作の実行はPoint phaseからinterval phaseへの道筋に相当する
上記のphaseでは今のDefault ccの実行で更新される。同時にask agentのガード条件が変わらない間の最小の時間間隔も計算されている 一度、全てのagentを分析したら、時間間隔を得る。それから、離散的変数値（他のプロセスによって修正されるかもしれないため、どんな瞬間でも変わりうる）が安定したpathに従って、次のpoint phaseへいく。 新nodeでは、時間を更新し、その瞬間の変数値を前のinterval phaseでの変数の限界値にセットする プログラムのglobalな処理時間で制約を課すためにuserが特定した時間間隔を使う この制約がグラフ構造を有限にする

18 今のnodeと、nがつなげられているのと同じnodeを結ばな いといけない この場合、とても強い結果を得る
次の2つの場合を区別する １つ目の場合 今の瞬間で、もしpoint phase（前の瞬間ですでに出現していて、もう一つのnode nによってグラフに表された）の終わりとなる静止点があるのなら、 ↓ 今のnodeと、nがつなげられているのと同じnodeを結ばな いといけない この場合、とても強い結果を得る userに特定された時間制限に到達したため、グラフの構造をカットしなかったから、グラフは完結する 　つまり、システムはどんな動きも表す

19 もし、今の静止点がグラフにまだ出現していなかったのなら、
もう一つの場合 もし、今の静止点がグラフにまだ出現していなかったのなら、 構造を続けなければならない 今のnodeと、p-arcによってつなげられる新しいnodeを作らないといけない 次のinterval phaseの初期状態と比較して、storeと実行点を含む新しいnodeを作らなければならない 　 Userによって定められた時間制限に到達した場合、構造は終わり、かつ、得られるモデルは現行の検証に対してだけ有効である そのモデルは異なる検証に対して再使用できない 仕様と実際のagentがあるとして、仕様内で後に続くagentがどれかを決定するのは容易である 上記の目的で機能followを使う 機能revisionはどのラベルがactiveでdisabledであるかを決定するために定義される

20

21 Operator Tell：ある情報をstoreに加える操作
グラフでは新しいnodeを作り、前の時点でのstoreに新しい制約を加える Positive Ask：ガード条件がstore内で満たされているかどうかを識別→満たされているならＡ実行 グラフでは新しいnodeを作り、そのnodeには前の時点の変数における制約を持ち続け、positive askの条件を加える Storeに制約が加えられ、矛盾が生じるとプログラムの実行をやめる 自分への矢印（ループ）はstoreがpositive askの条件を取り入れない時をモデル化するときに使う bodyのラベルが加えられる

22 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で表されるラベルを加える

23 Operator3 Hiding：変数の∃を表す Parallel：言語の並行な振る舞いを表す
グラフではstoreが変化しないが、ラベルは更新される新しいnodeを作る 変数のリネーム情報は補助構造から導入される Parallel：言語の並行な振る舞いを表す 実行の異なる枝をつくる 一つのノードに対してActiveなラベルの数と同じ直系の子ができる Hence：bodyのagentが今から後の各瞬間で実行される ラベルは静止点に達するまでdesabledになる 今のnodeから新しいnodeをつくる（p-arc） Storeとlabel functionはhccによって計算される

24 定理１．３ グラフの正当性を証明する Hccの仕様Ｓから組み立てたHybrid cc StructureをＴとすると δ（Ｔ）⊆【S】
δ： （rootから始めて、一つのpathでの各hccのnodeのプログラムstoreの繋がりによって与えられる）Ｔのtraceを表す 【S】：hccの仕様Ｓのoperational semanticを表す

25 Transformation Hybrid cc Strutureのinterval phaseを線形ハイブリッドオートマトンのlocation(=節)とする 同様にpoint phaseをlocationをつなぐarcsとする 各locationにおいて、変数の集合と変数の微分係数を、（interval phaseに対応して得られる）状態によって定義する Invariantはinterval phaseで定義されたask agentのガード条件の否定

26 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に異なるラベルを割り当てる

27

28 Conclusions Hccのプログラムに対して、システムの振る舞いをグラフ構造として表現を返す自動変換を定義した
Hccのプログラムの意味論で安定性に基づいて設計したので、point phaseとinterval phaseの一連の順序通りに計算することが保証される 分析とそれに伴う制限を時間間隔に与えることで、有限状態のmodel-checkerを使用できることを保証できる 線形ハイブリッドオートマトンで制限をつけないようなアルゴリズムを研究していく