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

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

2、軟件系統(tǒng)行為行為規(guī)范形式驗(yàn)證形式模型邏輯公式程序正確性軟件系統(tǒng)行為行為規(guī)范形式模型邏輯公式基于謂詞邏輯的描述基于顯式狀態(tài)的描述(有窮狀態(tài)系統(tǒng))程序正確性軟件系統(tǒng)行為行為規(guī)范形式模型邏輯公式命題邏輯、謂詞邏輯：狀態(tài)描述時(shí)序邏輯：行為描述程序正確性軟件系統(tǒng)行為行為規(guī)范形式驗(yàn)證形式模型邏輯公式程序推理模型檢測(cè)課程主要內(nèi)容形式驗(yàn)證形式模型邏輯公式程序推理模型檢測(cè)謂詞邏輯模型顯式狀態(tài)模型程序邏輯11預(yù)期目標(biāo)程序邏輯程序與系統(tǒng)模型驗(yàn)證方法掌握并能夠綜合應(yīng)用以下知識(shí):基本原理幾類簡(jiǎn)單的幾類簡(jiǎn)單的課程資料網(wǎng)頁(yè)http:/ Loeckx and Kurt Sieber. The Foundation of Pr

3、ogram Verification. John Wiley & Sons Ltd., 1984.Gerard J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1990.Nissim Francez. Program Verification. Addison-Wesley Publishing Company Inc., 1992.Edmund Clark, Orna Grumberg and Doron Peled. Model Checking. MIT press, 1999.Doron

4、A. Peled. Software Reliability Methods. Springer-Verlag. 2001.Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. MIT Press. 2008.Krzysztof R. Apt, Frank S. de Boer, Ernst-Rdiger Olderog. Verification of Sequential and Concurrent Programs. Springer-Verlag. 2009. Questions?課程主要內(nèi)容形式驗(yàn)

5、證形式模型邏輯公式程序推理模型檢測(cè)謂詞邏輯模型顯式狀態(tài)模型程序邏輯課程主要內(nèi)容(1)形式模型謂詞邏輯模型顯式狀態(tài)模型Kripke Structures-AutomataTimed AutomataPetri Nets結(jié)構(gòu)化循環(huán)語(yǔ)句模型流程圖模型衛(wèi)式遷移模型課程主要內(nèi)容(2)邏輯公式程序邏輯線性時(shí)序邏輯LTL計(jì)算樹邏輯CTL/CTL*-演算課程主要內(nèi)容(3,4)形式驗(yàn)證程序推理模型檢測(cè)衛(wèi)式遷移模型/LTL流程圖模型/前后斷言線性時(shí)序邏輯PLTL計(jì)算樹邏輯CTL課程主要內(nèi)容形式驗(yàn)證形式模型邏輯公式程序推理模型檢測(cè)謂詞邏輯模型顯式狀態(tài)模型程序邏輯課程主要內(nèi)容形式驗(yàn)證形式模型邏輯公式程序推理模型檢測(cè)謂詞邏輯模型顯式狀態(tài)模型程序邏輯描述問題刻