モデル検査 状態遷移系 PLTL（propositional linear-time temporal logic） PLTLのモデル検査 無限経路のもとでの論理式の解釈 PLTLのモデル検査 オートマトンの構成 無限経路に関する条件 状態遷移系との同期的合成 fairnessの表現 SPIN概要 http://spinroot.com/spin/Doc/ieee97.pdf
証明支援系 PVSチュートリアル http://www.csl.sri.com/papers/forte97/ 状態遷移系の記述 モデル検査 invariantの検証 抽象化 抽象モデル検査 抽象化の妥当性の検証
抽象モデル検査：事例 alternating bit protocol 抽象化 レポート課題２ sender: header, message receiver: header message queue ack queue verify queue 抽象化 レポート課題２
認証プロトコルの検証 状態遷移系としてのプロトコル ストランドを用いた推論 状態 遷移 Needham-Schroeder公開鍵プロトコル ストランドのマルチセット メッセージの集合 遷移 ストランドの伸長 攻撃者による偽メッセージの送信 ストランドを用いた推論 Needham-Schroeder公開鍵プロトコル
Javaプログラムの検証 JMLとESC/Java ESC/Javaマニュアル 卒論紹介 LOOP http://research.compaq.com/SRC/esc/download.html 卒論紹介 Verification of the Validity of Java Card Transactions LOOP JavaからPVSへの変換
レポート課題１ untilオペレータUの双対である releaseオペレータRを次のように導入し、 その意味を定めよ。 φ R ψ ≡ ￢(￢φ U ￢ψ) UとRを含む線形時間時相論理に対して、 モデル検査の手続きを与えよ。
レポート課題２ キューを抽象化し、 抽象状態を網羅することにより、 alternating bit protocolの安全性を検証せよ。 （メッセージは0か1とする。） 抽象化の正当性について議論せよ。 alternating bit protocolの活性について 議論せよ。
レポート課題３ 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
レポート課題４ quicksortのJavaプログラムを書き、 配列のインデックスが限界を超えないことを 検証するためのESC/Javaのpragmaを 各メソッドに挿入せよ。 また、quicksortの正当性をpragmaによって 表現してみよ。 このために必要なloop invariantなども できる限りprogmaとして表現せよ。
４題のうち、２題を選んで レポートを提出して下さい。 〆切は米澤先生の〆切と 同じにします。