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

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

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

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