汽車電子軟件的實(shí)時(shí)性驗(yàn)證方法研究.pdf

1、隨著人們要求的日益增高，現(xiàn)代汽車集成各種各樣復(fù)雜的應(yīng)用，在應(yīng)用程序與硬件之間加入操作系統(tǒng)成為必然。如何驗(yàn)證帶操作系統(tǒng)的汽車電子軟件的實(shí)時(shí)性成了許多研究人員共同關(guān)注的問題。
　　 對(duì)于嵌入式系統(tǒng)實(shí)時(shí)性的驗(yàn)證，形式化推理分析與模型分析是現(xiàn)存的兩大最重要的方法，但前者往往分析過程比較復(fù)雜，且沒有直觀的運(yùn)行界面，不能模擬整個(gè)系統(tǒng)的真實(shí)運(yùn)行情況。而模型分析方法則形式各異，各有所長。PETRI網(wǎng)適合于描述異步的、并發(fā)的計(jì)算機(jī)系統(tǒng)模型，它既有

2、嚴(yán)格的數(shù)學(xué)表述方式，也有直觀的圖形運(yùn)行界面，能分析系統(tǒng)的實(shí)時(shí)性、可靠性等各種性能。
　　 本文在TOPPERS操作系統(tǒng)基礎(chǔ)上，以汽車自適應(yīng)巡航控制系統(tǒng)為例，分析得出一種汽車電子軟件的實(shí)時(shí)性驗(yàn)證方法。
　　 文章首先分別闡述現(xiàn)代汽車電子系統(tǒng)和車載操作系統(tǒng)的發(fā)展，并歸納總結(jié)對(duì)于實(shí)時(shí)性的驗(yàn)證所存在的方法，包括形式化推理、時(shí)間自動(dòng)機(jī)、AADL建模等；接著文章在分析Petri網(wǎng)的時(shí)間擴(kuò)展與性質(zhì)基礎(chǔ)上，得出一種利用時(shí)間Petri網(wǎng)來

3、驗(yàn)證汽車電子系統(tǒng)實(shí)時(shí)性的方法，并制定從帶時(shí)間參數(shù)的狀態(tài)轉(zhuǎn)換圖到時(shí)間 Petri網(wǎng)的映射規(guī)則；然后在TOPPERS操作系統(tǒng)的基礎(chǔ)上設(shè)計(jì)實(shí)現(xiàn)驗(yàn)證實(shí)例汽車自適應(yīng)巡航控制系統(tǒng)，并測(cè)試相關(guān)的任務(wù)運(yùn)行時(shí)間；最后建立汽車自適應(yīng)巡航控制系統(tǒng)相對(duì)應(yīng)的時(shí)間Petri網(wǎng)模型，通過驗(yàn)證工具EXSPECT運(yùn)行模型系統(tǒng)，在兩種不同模式下分別分析驗(yàn)證其實(shí)時(shí)性并進(jìn)行相關(guān)方面的比較。
　　 結(jié)果顯示本文所提出的驗(yàn)證汽車電子軟件實(shí)時(shí)性的方法能準(zhǔn)確得出整個(gè)系統(tǒng)運(yùn)行所