《課程總結(jié)-講》PPT課件

1、程序的方式驗證 內(nèi)容中國科學院軟件研討所張文輝lcs.ios.ac/zwh/pv課程主要內(nèi)容程序與系統(tǒng)模型預備知識: 邏輯/函數(shù)/有向圖程序邏輯驗證方法: 推理證明/模型檢測課程內(nèi)容程序與系統(tǒng)模型隱式遷移模型顯式形狀遷移模型標號遷移系統(tǒng)時間遷移系統(tǒng)等模型一階線性時序邏輯課程內(nèi)容程序邏輯線性時序邏輯PLTL分枝時序邏輯CTL時序邏輯CTL*等課程內(nèi)容程序的推理證明衛(wèi)式遷移模型的推理謂詞遷移模型的推理流程圖模型的推理構(gòu)造化程序模型推理課程內(nèi)容程序的模型檢測基于途徑的模型檢測基于形狀的模型檢測限界語義模型檢測課程總結(jié)給定一個程序和一些性質(zhì)用嚴厲的方法證明程序能否滿足給定的性質(zhì)程序性質(zhì)模型邏輯公式驗證

2、方法主要內(nèi)容 程序模型 程序邏輯 驗證方法模型邏輯公式驗證方法 驗證工具 驗證明例一、程序模型 隱式遷移系統(tǒng)描畫 構(gòu)造化循環(huán)程序、流程圖程序 衛(wèi)式遷移系統(tǒng)、謂詞遷移系統(tǒng) 顯式形狀遷移系統(tǒng)描畫 Kripke構(gòu)造、標號Kripke構(gòu)造 公平Kripke構(gòu)造 標號遷移系統(tǒng) 標號遷移系統(tǒng)、自動機 交錯遷移系統(tǒng)、交錯自動機 時間遷移系統(tǒng) 時間遷移系統(tǒng)、時間自動機 混成遷移系統(tǒng)、 Petri網(wǎng)、通訊系統(tǒng)不同類型模型的特點模型之間的關(guān)系用模型描畫系統(tǒng)構(gòu)造化循環(huán)程序 謂詞邏輯、解釋、賦值 語句組合 運轉(zhuǎn)、語義 前斷言、后斷言 推理驗證方法流程圖程序 謂詞邏輯、解釋、賦值 指令集合、begin - end 運轉(zhuǎn)

3、、語義 前斷言、后斷言 推理驗證方法衛(wèi)式遷移系統(tǒng) 謂詞邏輯、解釋、賦值 遷移集合、初始條件 形狀、形狀序列、可執(zhí)行遷移、運轉(zhuǎn) 推理驗證方法謂詞遷移系統(tǒng) 謂詞邏輯、解釋、賦值 遷移的謂詞、初始條件 形狀、形狀序列、可執(zhí)行遷移、運轉(zhuǎn) 推理驗證方法Kripke構(gòu)造 S: 形狀集合 RSxS: 遷移關(guān)系 I S: 初始形狀集合形狀、形狀序列、遷移、途徑、運轉(zhuǎn)標號Kripke構(gòu)造 S: 形狀集合 RSxS: 遷移關(guān)系 I S: 初始形狀集合 L: S2AP: 標號函數(shù)言語公平標號Kripke構(gòu)造 S: 形狀集合 RSxS: 遷移關(guān)系 I S: 初始形狀集合 L: S2AP: 標號函數(shù) F 2S: 公平要

4、求的集合公平運轉(zhuǎn)、言語標號遷移系統(tǒng) :標號集合 S: 形狀集合 S x x S: 遷移關(guān)系 I S: 初始形狀集合運轉(zhuǎn)、字符串、言語Buchi自動機 :標號集合 S: 形狀集合 S x x S: 遷移關(guān)系 I S: 初始形狀集合 F 2S: 接受條件不同類型的自動機可接受運轉(zhuǎn)、可接受字符串、言語交錯遷移系統(tǒng) :標號集合 S: 形狀集合 S x x 2S: 遷移關(guān)系 I S: 初始形狀集合樹構(gòu)造的運轉(zhuǎn)交錯自動機 :標號集合 S: 形狀集合 S x x 2S: 遷移關(guān)系 I S: 初始形狀集合 F 2S: 接受條件可接受運轉(zhuǎn)、可接受字符串、言語時間遷移系統(tǒng) :標號集合 S: 形狀集合 C: 時鐘集

5、合 S x x 2C x(C)xS: 遷移關(guān)系 I S: 初始形狀集合時間字符串、時間字符串上的運轉(zhuǎn)時間自動機 :標號集合 S: 形狀集合 X: 時鐘集合 S x x 2X x(X)xS: 遷移關(guān)系 I S: 初始形狀集合 F 2S: 接受條件可接受運轉(zhuǎn)、可接受時間字符串、言語混成遷移系統(tǒng) :標號集合 S: 形狀集合 X: 實數(shù)變量集合 S x x (X) x (X) x S: 遷移關(guān)系 I S: 初始形狀集合 flow: S (X,X) 時間字符串、時間字符串上的運轉(zhuǎn)Petri網(wǎng) P: 位置集合 T: 遷移集合 F (P T) (T P) : 邊的集合 M0 : PN 初始形狀形狀、遷移、運

6、轉(zhuǎn)、可達形狀通訊單元、通訊系統(tǒng) Q: 形狀集合 C: 通道集合 Q (C) Q: 遷移關(guān)系 q0 Q: 初始形狀事件、可執(zhí)行事件、形狀、遷移、運轉(zhuǎn)二、程序邏輯 線性時序邏輯 命題線性時序邏輯 一階線性時序邏輯 線性-演算 分枝時序邏輯 計算樹邏輯(CTL) CTL* 模態(tài)-演算公式之間的關(guān)系公式和模型的對應關(guān)系公式和形狀集的對應關(guān)系用公式描畫系統(tǒng)或性質(zhì)不同邏輯的特點邏輯之間的關(guān)系線性時序邏輯 命題邏輯、謂詞邏輯 言語 語義 邏輯公式之間的關(guān)系 邏輯公式用于描畫性質(zhì)和系統(tǒng)模型 邏輯公式對應于系統(tǒng)模型(自動機)分枝時序邏輯 命題邏輯 言語 語義 邏輯公式之間的關(guān)系 邏輯公式用于描畫性質(zhì) 邏輯公式對

7、應于Kripke構(gòu)造的形狀集三、驗證方法 推理驗證 衛(wèi)式遷移系統(tǒng) 流程圖程序 構(gòu)造化程序 模型檢測 基于形狀 基于途徑 限界模型檢測模型檢測方法：特點運用相關(guān)的構(gòu)造和算法程序推理方法：特點運用推理驗證 衛(wèi)式遷移系統(tǒng) 程序推理規(guī)那么 線性時序邏輯推理規(guī)那么 流程圖程序 根據(jù)操作語義證明 根據(jù)途徑分段證明、最弱寬松前斷言計算方法 構(gòu)造化程序 根據(jù)指稱語義證明 根據(jù)公理語義、Hoare邏輯證明平安性質(zhì)呼應性質(zhì)部分正確完全正確模型檢測 基于形狀 顯式形狀遷移系統(tǒng) 符號形狀遷移系統(tǒng)(最簡二元決策圖) 基于途徑 用自動機表示系統(tǒng) 用自動機表示性質(zhì)(由公式構(gòu)造自動機的方法) 限界模型檢測 限界模型 限界語義及運用四、驗證工具與實例 驗證工具 程序推理輔助工具XYZ/VERI-II 模型檢測工具SMV 模型檢