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

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

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

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

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