FlexRay通信協(xié)議的模型檢查.pdf

1、目前,車載系統(tǒng)主要采用電子控制單元(ECUs)來實現(xiàn)X-by-wire技術(shù)。通過X-by-wire技術(shù),使不能機械地被實現(xiàn)的功能或需求變?yōu)榭赡?。一般來說,在一個汽車系統(tǒng)中的ECU按照通信協(xié)議相互通信,通過一個或多個總線。由于通信協(xié)議極大地影響汽車系統(tǒng)的性能,協(xié)議能夠支持高傳輸速率和可靠性的要求。最近,FlexRay通信協(xié)議被視為實際標(biāo)準(zhǔn)的汽車通信協(xié)議。FlexRay通信協(xié)議支持高傳輸速率可達10Mbs,同時仍保持可靠性和容錯性。這些特性

2、使FlexRay特別適用于安全關(guān)鍵系統(tǒng)。另一方面,汽車系統(tǒng)的測試過程既費時又復(fù)雜的。在工業(yè)領(lǐng)域,應(yīng)準(zhǔn)備實現(xiàn)通信協(xié)議的設(shè)備需測試應(yīng)用程序在ECUs上執(zhí)行,連接ECUs和協(xié)議控制設(shè)備,形成一個測試環(huán)境。從以前的測試的數(shù)據(jù)支持進行測試,專注于特定的節(jié)點或數(shù)據(jù)傳輸。由于更高的要求,導(dǎo)致復(fù)雜的功能,因此需要更多的ECU,并且測試過程中伴隨著大量的設(shè)備和高財務(wù)成本使測試變得更加困難。
　　本文提出了一個框架驗證FlexRay車載系統(tǒng)的設(shè)計模型

3、。該框架基于UPPAAL,它是一個時間自動機模型檢查器為時間相關(guān)的行為建模。通過該框架驗證設(shè)計模型,在設(shè)計階段開發(fā)人員用模型檢驗技術(shù)可以更好的機會發(fā)現(xiàn)缺陷。這樣做可以減少系統(tǒng)的開發(fā)的成本,同時提高應(yīng)用程序的質(zhì)量。類似于設(shè)備為基礎(chǔ)的測試,UPPAAL框架由一個FlexRay模型和應(yīng)用模型組成。前者代表的FlexRay設(shè)備,后者代表的ECU執(zhí)行的應(yīng)用程序。UPPAAL只提供了應(yīng)用通道的同步方法,因此FlexRay模型和應(yīng)用模型必須進行特殊處

4、理?；贔lexRay規(guī)格書,對其進行三步抽象最終建立FlexRay模型。FlexRay模型還提供了通信和訪問應(yīng)用模型之間的參數(shù)和接口。應(yīng)用模型只需要按照這些參數(shù)和接口,與FlexRay模型合作為車載系統(tǒng)的設(shè)計模型。為了評估框架,進行了如下實驗:(1)應(yīng)用模型基本行為的測試是為了檢查FlexRay模型的有效性,(2)建立一個簡單的應(yīng)用驗證系統(tǒng)的響應(yīng)時間,通過使用觀測器模型進行測試(3)介紹了簡化的自適應(yīng)巡航控制系統(tǒng),為了顯示了可行性通過