程序的形式驗(yàn)證課件

1、程序正確性的重要性應(yīng)用廣泛航空航天金融設(shè)備的控制日常生活軟件錯(cuò)誤的可能后果火箭 Ariane 5 Explosion (1997)火星氣候軌道器 NASA Mars Climate Orbiter (1999)第1頁(yè)，共22頁(yè)。程序正確性程序軟件系統(tǒng)軟件系統(tǒng)行為正確性符合行為規(guī)范第2頁(yè)，共22頁(yè)。程序正確性軟件系統(tǒng)行為行為規(guī)范測(cè)試Program testing can be used to show the presence of bugs, but never to show their absence! - Edsger W. Dijkstra第3頁(yè)，共22頁(yè)。程序正確性軟件系統(tǒng)行為行為規(guī)

2、范形式驗(yàn)證?第4頁(yè)，共22頁(yè)。程序正確性軟件系統(tǒng)行為行為規(guī)范形式驗(yàn)證形式模型邏輯公式第5頁(yè)，共22頁(yè)。程序正確性軟件系統(tǒng)行為行為規(guī)范形式模型邏輯公式基于謂詞邏輯的描述基于顯式狀態(tài)的描述(有窮狀態(tài)系統(tǒng))第6頁(yè)，共22頁(yè)。程序正確性軟件系統(tǒng)行為行為規(guī)范形式模型邏輯公式命題邏輯、謂詞邏輯：狀態(tài)描述時(shí)序邏輯：行為描述第7頁(yè)，共22頁(yè)。程序正確性軟件系統(tǒng)行為行為規(guī)范形式驗(yàn)證形式模型邏輯公式程序推理模型檢測(cè)第8頁(yè)，共22頁(yè)。課程主要內(nèi)容形式驗(yàn)證形式模型邏輯公式程序推理模型檢測(cè)謂詞邏輯模型顯式狀態(tài)模型程序邏輯第9頁(yè)，共22頁(yè)。10預(yù)期目標(biāo)程序邏輯程序與系統(tǒng)模型驗(yàn)證方法掌握并能夠綜合應(yīng)用以下知識(shí):基本原理幾類

3、簡(jiǎn)單的幾類簡(jiǎn)單的第10頁(yè)，共22頁(yè)。課程資料網(wǎng)頁(yè)/zwh/pv第11頁(yè)，共22頁(yè)。主要參考資料軟件系統(tǒng)行為與程序正確性。/zwh/pv/pv13.pdf第12頁(yè)，共22頁(yè)。參考書Jacques Loeckx and Kurt Sieber. The Foundation of Program Verification. John Wiley & Sons Ltd., 1984.Gerard J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1990.Nissim Francez. Program V

4、erification. Addison-Wesley Publishing Company Inc., 1992.Edmund Clark, Orna Grumberg and Doron Peled. Model Checking. MIT press, 1999.Doron A. Peled. Software Reliability Methods. Springer-Verlag. 2001.Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. MIT Press. 2008.Krzysztof R

5、. Apt, Frank S. de Boer, Ernst-Rdiger Olderog. Verification of Sequential and Concurrent Programs. Springer-Verlag. 2009.第13頁(yè)，共22頁(yè)。 Questions?第14頁(yè)，共22頁(yè)。課程主要內(nèi)容形式驗(yàn)證形式模型邏輯公式程序推理模型檢測(cè)謂詞邏輯模型顯式狀態(tài)模型程序邏輯第15頁(yè)，共22頁(yè)。課程主要內(nèi)容(1)形式模型謂詞邏輯模型顯式狀態(tài)模型Kripke Structures-AutomataTimed AutomataPetri Nets結(jié)構(gòu)化循環(huán)語(yǔ)句模型流程圖模型衛(wèi)式遷移模型第16頁(yè)，共22頁(yè)。課程主要內(nèi)容(2)邏輯公式程序邏輯線性時(shí)序邏輯LTL計(jì)算樹邏輯CTL/CTL*-演算第17頁(yè)，共22頁(yè)。課程主要內(nèi)容(3,4)形式驗(yàn)證程序推理模型檢測(cè)衛(wèi)式遷移模型/LTL流程圖模型/前后斷言線性時(shí)序邏輯PLTL計(jì)算樹邏輯CTL第18頁(yè)，共22頁(yè)。課程主要內(nèi)容形式驗(yàn)證形式模型邏輯公式程序推理模型檢測(cè)謂詞邏輯模型顯式狀態(tài)模型程序邏輯第19頁(yè)，共22頁(yè)。課程主要內(nèi)容形式驗(yàn)證形式模型邏輯公式程序推理模型檢測(cè)謂詞邏輯模型顯式狀態(tài)模型程序邏輯描述問(wèn)題刻畫行為描述問(wèn)題刻畫行為第20頁(yè)，共