可驗證的數(shù)字機器.pdf

1、隨著數(shù)字時代的到來，工程師們研發(fā)系統(tǒng)的周期越來越短，對系統(tǒng)的可靠性要求越來越高。圖形建模是當今工程領域的一項重要技術。一個系統(tǒng)或是協(xié)議在它的分析設計階段，本文通過建立相應的圖形化的模型，使它具有實際系統(tǒng)的某些性質(zhì)。模型是對系統(tǒng)的抽象，它較易于理解、分析和驗證，對模型的驗證結(jié)果可以直接作用于實際系統(tǒng)，而且糾正錯誤的成本也相對于實際系統(tǒng)而言比較低。 本文構(gòu)筑一個圖形化的建模環(huán)境，基于狀態(tài)機的原理對系統(tǒng)進行圖形建模，并定義其應具有的性

2、質(zhì)。然后分別對系統(tǒng)模型和性質(zhì)進行形式化，最后通過計算機對其驗證。 本論文利用狀態(tài)機強大的圖形化的描述能力對系統(tǒng)進行描述建模并定義了與之相關的語法以及語義，引入了EHA作為中間模型生成系統(tǒng)的LTS，解決了狀態(tài)機對結(jié)構(gòu)化的破壞問題，最后得出相應的Büchi自動機。 研究了如何使用LIL公式表達模型性質(zhì)并給出LTL公式到Büchi自動機的轉(zhuǎn)換方法。通過對兩個自動機的乘積進行判空，可以判斷模型是否滿足欲驗證的性質(zhì)。由于狀態(tài)機本身