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

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

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

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