モデル検査 状態遷移系 PLTL（propositional linear-time temporal logic） PLTLのモデル検査

Presentation on theme: "モデル検査 状態遷移系 PLTL（propositional linear-time temporal logic） PLTLのモデル検査"— Presentation transcript:

1 モデル検査 状態遷移系 PLTL（propositional linear-time temporal logic） PLTLのモデル検査
無限経路のもとでの論理式の解釈 PLTLのモデル検査 オートマトンの構成 無限経路に関する条件 状態遷移系との同期的合成 fairnessの表現 SPIN概要

2 証明支援系 PVSチュートリアル http://www.csl.sri.com/papers/forte97/ 状態遷移系の記述 モデル検査
invariantの検証 抽象化 抽象モデル検査 抽象化の妥当性の検証

3 抽象モデル検査：事例 alternating bit protocol 抽象化 レポート課題２
sender: header, message receiver: header message queue ack queue verify queue 抽象化 レポート課題２

4 認証プロトコルの検証 状態遷移系としてのプロトコル ストランドを用いた推論 状態 遷移 Needham-Schroeder公開鍵プロトコル
ストランドのマルチセット メッセージの集合 遷移 ストランドの伸長 攻撃者による偽メッセージの送信 ストランドを用いた推論 Needham-Schroeder公開鍵プロトコル

5 Javaプログラムの検証 JMLとESC/Java ESC/Javaマニュアル 卒論紹介 LOOP
卒論紹介 Verification of the Validity of Java Card Transactions LOOP JavaからPVSへの変換

6 レポート課題１ untilオペレータUの双対である releaseオペレータRを次のように導入し、 その意味を定めよ。
φ R ψ ≡ ￢(￢φ U ￢ψ) UとRを含む線形時間時相論理に対して、 モデル検査の手続きを与えよ。

7 レポート課題２ キューを抽象化し、 抽象状態を網羅することにより、 alternating bit protocolの安全性を検証せよ。
（メッセージは0か1とする。） 抽象化の正当性について議論せよ。 alternating bit protocolの活性について 議論せよ。

8 レポート課題３ A®B : {A,NA}KB B®A : {NA,NB}KA A®B : {B,NA}KA－1
次のプロトコルの正しさについて議論せよ。A®B : {A,NA}KB　 B®A : {NA,NB}KA A®B : {B}NB　 次のプロトコルの正しさについて議論せよ。 A®B : {A,NA}KB　 B®A : {NA,NB}KA A®B : {B,NA}KA－1　

9 レポート課題４ quicksortのJavaプログラムを書き、 配列のインデックスが限界を超えないことを
検証するためのESC/Javaのpragmaを 各メソッドに挿入せよ。 また、quicksortの正当性をpragmaによって 表現してみよ。 このために必要なloop invariantなども できる限りprogmaとして表現せよ。

10 ４題のうち、２題を選んで レポートを提出して下さい。 〆切は米澤先生の〆切と 同じにします。