基于調(diào)度機(jī)調(diào)度的并發(fā)執(zhí)行任務(wù)的邊界模型檢測(cè).pdf

1、OSEK/VDX作為一個(gè)汽車(chē)操作系統(tǒng)的標(biāo)準(zhǔn)已經(jīng)被廣發(fā)的運(yùn)用到車(chē)載系統(tǒng)中,并且隨著汽車(chē)科技的發(fā)展,越來(lái)越多的復(fù)雜的輔助功能被運(yùn)用到了汽車(chē)中。眾所周知,對(duì)于基于OSEK/VDX開(kāi)發(fā)的汽車(chē)軟件,安全性與可靠性是非常重要的,但是由于軟件的復(fù)雜度的提高,如何確保安全性以及可靠性是對(duì)開(kāi)發(fā)者的巨大挑戰(zhàn)。
　　據(jù)我所了解的知識(shí),對(duì)于OSEK/VDX操作系統(tǒng)的驗(yàn)證已經(jīng)出現(xiàn)了很多技術(shù),最具有代表性的是運(yùn)用形式化驗(yàn)證軟件SPIN對(duì)其驗(yàn)證,但是還沒(méi)有對(duì)在

2、其之上開(kāi)發(fā)的軟件進(jìn)行驗(yàn)證,因此本文提出一個(gè)模型化檢測(cè)的方法,該方法可以被用來(lái)幫助開(kāi)發(fā)者發(fā)現(xiàn)基于OSEK/VDX操作系統(tǒng)開(kāi)發(fā)的軟件的潛在的與不容易驗(yàn)證的錯(cuò)誤。
　　由于基于OSEK/VDX OS開(kāi)發(fā)的軟件可以使用服務(wù)API與OSEK/VDX進(jìn)行交互,并且服務(wù)API可能會(huì)影響下一個(gè)要運(yùn)行的任務(wù),簡(jiǎn)單的描述一個(gè)軟件的執(zhí)行行為是非常困難的。在本論文中,我們用一個(gè)k步execution-Tree描述軟件的執(zhí)行k步的執(zhí)行行為,并且我們使用邊界

3、模型檢測(cè)(BMC)技術(shù)把存在于樹(shù)中的執(zhí)行路徑轉(zhuǎn)化成為與之等價(jià)的用CNF表述的公式。對(duì)于要驗(yàn)證的系統(tǒng)的屬性,在我們研究中我們用線性時(shí)序邏輯(LTL)表示。最后為了得到驗(yàn)證結(jié)果,我們將每一條路徑的CNF與表示驗(yàn)證屬性的LTL公式輸入到先進(jìn)的SMT求解器Yices中進(jìn)行求解。為了評(píng)價(jià)我們提出方法的驗(yàn)證效率與正確性,我們按照我們所提出的方法開(kāi)發(fā)了一個(gè)簡(jiǎn)單的工具,并且用我們的工具做了大量的實(shí)驗(yàn),實(shí)驗(yàn)結(jié)果表明我們的模型檢測(cè)方法可以高效地正確地檢測(cè)一