正規描述與自動驗證FormalDescriptionAutomatedVerification.pptVIP

* * * * * * * * * * * * * * * * * * 正規描述與自動驗證Formal Description Automated Verification 王 凡 國立台灣大學 電機工程系 Verification （驗證）? 找出系統設計中的所有錯誤。 確認系統中已經（接近）沒有錯誤。 非常困難！ 複雜系統的決勝關鍵！ 各位同學的一條生路！ 台灣產業的一條生路！ 簡介 瞭解電腦系統的formal semantics 學習電腦輔助驗證的理論與製作 你曾經對我說，永遠愛著我！ 如果你媽和我一起掉下水，你要先救誰？ 厚！以後存款 、房子是誰 的名下？ …?? …?? …!! …!! 你愛不愛人家嗎？ 當然愛你啦！北鼻！ 瞭解電腦系統的formal semantics divide (a, b) { while (a 0) a = a-b; if (a == 0) return 1; else return 0; } Is this program correct ? How do I know what it is supposed to do ? It checks if a is divisible by b. I doubt it! What happens when b = 0 ? Well, sometimes happens! 瞭解電腦系統的formal semantics divide (a, b) { while (a 0) a = a-b; if (a == 0) return 1; else return 0; } Seriously, what does “a=a-b;” means ? What does this `if’ statement means ? 瞭解電腦系統的formal semantics When we say a program is correct, what is the behavior model of the program ? What is the mathematics of program behaviors ? 瞭解電腦系統的formal semantics (②,10,3) (③,10,3) a0 (②,7,3) a=a-b; a0 (③,7,3) (②,4,3) a=a-b; (③,4,3) a0 (②,1,3) (③,1,3) a=a-b; a0 (②,-2,3) ?a0 a=a-b; (④,-2,3) (⑤,-2,3) ?a==0 state, possible world Kripke structure ①divide (a, b) { ② while (a 0) ③ a = a-b; ④ if (a == 0) return 1; ⑤ else return 0; ⑥} 瞭解電腦系統的formal semantics- an attempt ①divide (a, b) { ② while (a 0) ③ a = a-b; ④ if (a == 0) return 1; ⑤ else return 0; ⑥} p(k): the statement at state k; a(k): the value of a at state k; b(k): the value of b at state k; ?k?0(p(k)== ③ ? a(k+1)==a(k)-b(k)) First-order arithmetic! A lot of tools can help you predict the behaviors of the program. The wonderful logics! 太棒了！北鼻！有了logics，我們現在可以清楚瞭解彼此的行為與結構。 倫倫！一切的誤會，都可以說清楚，講明白了。 兩位好瞎！一定沒有修過離散、邏輯。Goedel已經證明有些定理是邏輯無法判別的。 即使可以判別，但也可能有state-space爆炸問題呀！ Some incomputable problems (1/2) The validity of 1st-order logic formula (Hilbert’s 2nd problem) ?x?y?z(single(x) ? (parent(y,x)?worried(y)) Mortal matrix problem Given 15 3?3 matrices, M1,