基于時間多棧下推網(wǎng)絡(luò)的實時系統(tǒng)驗證技術(shù)研究.pdf

1、隨著計算機領(lǐng)域內(nèi)多核技術(shù)日益發(fā)展，實時并發(fā)軟件已滲透到國民經(jīng)濟和國防建設(shè)的各個領(lǐng)域，然而軟件上微小錯誤都有可能導(dǎo)致重大事故，甚至危及人身安全，諸如交通控制和航空航天等領(lǐng)域。增強軟件的安全性與可靠性已成為目前研究人員急需解決的問題。對一些安全攸關(guān)的實時系統(tǒng)來說，其安全性要求更高，但是傳統(tǒng)的測試方法，其測試方案不滿足完備性，使得系統(tǒng)分析時可靠性得不到保證。故如需充分驗證實時并發(fā)系統(tǒng)的關(guān)鍵性質(zhì)，那么利用模型檢驗技術(shù)對其形式化驗證分析將是非常好

2、的方法。論文針對目前模型檢驗在實時系統(tǒng)中的可達性分析進行了相關(guān)研究，取得了一些科研成果，具體如下：
　　(1)分析實時系統(tǒng)形式化驗證的發(fā)展現(xiàn)狀，提出了將描述連續(xù)時間的時鐘引入到多棧下推網(wǎng)絡(luò)(MPDN)的思想，并給出了具體的時間多棧下推網(wǎng)絡(luò)(TMPDN)模型，及其語法和語義。然后利用時鐘域等價的優(yōu)化技術(shù)，通過靜態(tài)和動態(tài)兩種轉(zhuǎn)換方法，將連續(xù)時間的TMPDN模型轉(zhuǎn)換成離散的MPDN模型，同時證明了狀態(tài)qF在TMPDN可達當(dāng)且僅當(dāng)其轉(zhuǎn)換狀

3、態(tài)qF′在MPDN可達，并給出了模型轉(zhuǎn)換算法，最后分析了時間下推網(wǎng)絡(luò)模型的上下文切換限界可達性問題。該模型解決了傳統(tǒng)的時間自動機無法描述并發(fā)遞歸的情況，為模型檢驗驗證分析實時并發(fā)遞歸程序提供了一種新思路。
　　(2)針對實時系統(tǒng)運行時進程/線程動態(tài)創(chuàng)建的情況，將時間多棧下推網(wǎng)絡(luò)模型進行了擴展，使其能夠充分的描述程序運行時創(chuàng)建進程/線程的機制，并給出了擴展后的模型轉(zhuǎn)換成時間多棧下推網(wǎng)絡(luò)模型的算法，實時并發(fā)程序轉(zhuǎn)換為時間多棧下推網(wǎng)絡(luò)的