程序驗證與系統(tǒng)分析中的若干符號計算問題.pdf

1、形式化方法是開發(fā)高可信軟件和安全攸關系統(tǒng)的有效途徑，是高可信計算的研究重點之一。高可信計算追求軟件和系統(tǒng)提供可信賴的計算服務能力，而這種可信賴性是建立在嚴格數(shù)學證明上的。形式化方法主要研究軟硬件系統(tǒng)的規(guī)格描述、開發(fā)過程、以及檢測驗證，特別是程序正確性證明和系統(tǒng)安全性分析。研究的問題有活性、安全性、公平性、終止性、不變式、同步、異步、互斥、可達性、持續(xù)性、穩(wěn)定性等。
　　 在處理這些程序和系統(tǒng)中的分析與驗證問題時，傳統(tǒng)的邏輯方法會

2、因為狀態(tài)空間爆炸而無法檢測出全部錯誤，不能徹底地保證安全性；單純數(shù)值計算又會產生浮點誤差，影響整體的可靠性。因而，近年來研究者正在嘗試使用以絕對準確性為目標的符號計算方法來處理它們，即將這些性質的檢驗問題轉換成代數(shù)系統(tǒng)的求解問題。特別是隨著計算機性能和計算機數(shù)學的不斷發(fā)展，為開展該方向的研究提供了強有力的支撐。
　　 本文的主要貢獻由以下幾部分組成：
　　 1.理論部分：主要研究了若干種廣義多項式的實根隔離問題。在M.A

3、chatz等人2008年的工作基礎上，提出了用連分數(shù)技巧逼近超越數(shù)e和區(qū)間算術思想進行準確計算，改進了現(xiàn)有指數(shù)多項式實根隔離算法；同時對于冪指數(shù)多項式，推廣了偽導數(shù)序列的構造方法，證明了廣義Budan-Fourier定理對其仍然成立，并給出一個正根隔離近似算法。
　　 2.應用部分：主要嘗試了將上述理論成果應用在程序驗證和系統(tǒng)分析領域。一方面，利用估計多指數(shù)多項式實根界算法，完善了A.Tiwari在2004年關于線性循環(huán)終止性的

4、結論。在其終止性可判定理論的基礎上，對于給定非終止循環(huán)構造出其非終止輸入作為反例，使該結果更加完整。另一方面，將廣義多項式實根隔離算法用于判定線性系統(tǒng)的可達性問題，除去了線性系統(tǒng)矩陣的可對角化限制，豐富了輸入函數(shù)的類型，擴展了G．Lafferrierre等人在2001年的結果。
　　 3.軟件部分：主要在計算機代數(shù)系統(tǒng)MAPLE下編制了程序包RFACH，能夠準確求解任意由指數(shù)多項式等式和不等式所組成系統(tǒng)，實現(xiàn)了判定有理特征值線性