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

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

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

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