智能汽車CAN總線通信系統的建模與驗證

張 芮 王 瑞 楚 敏

(首都師范大學信息工程學院 北京 100048)(首都師范大學輕型工業機器人與安全驗證北京市重點實驗室 北京 100048)

0 引 言

智能汽車的興起為普通汽車向無人駕駛汽車轉變提供了可能性，但這個過程不是一蹴而就的，需要經歷一個漫長的時期[1]。車載通信系統是智能汽車內外交互和信息傳輸的載體，因此保證智能車輛通信系統的安全是一個非常重要的問題。控制器局域網絡總線是一種串行總線，同時支持分布式控制，是應用較為廣泛的一種現場總線[2]。它包含了收發器、仲裁器和網關等模塊，收發器能夠保證報文接收和發送的暢通，仲裁器能夠保證報文的格式和優先級的正確，而網關[3]則是針對報文傳輸速率的差別，對這些報文重新進行打包并且發送。這些通信總線上的關鍵模塊保證了數據在傳輸過程的正確性。

本文主要對基于CAN總線的智能車輛通信系統進行分析，并對報文的傳輸過程中各模塊建立時間自動機模型，特別加入了對通信過程中網關的建模，保證了報文能夠在高速和低速時正常傳輸，較好地模擬車輛內部通信的過程。其次，將智能汽車在行駛過程中需要滿足的屬性用計算樹邏輯公式進行抽象和形式化描述，運用模型檢測工具對這些屬性進行驗證，確保車輛在遇到突發緊急的交通情況下，通信系統能夠及時傳遞數據，車輛決策正確，輔助駕駛者做出相應操作。

1 系統描述

1.1 基于CAN總線通信的智能車輛系統

通信過程中，數據和命令的傳輸過程借助于汽車總線系統，汽車總線的種類是多種多樣的，例如：CAN總線[4]適用于實時系統，它的優點是線束少、重量輕，可以實現豐富的車身功能；局域互聯網絡(Local Interconnect Network, LIN)總線可為車載通信系統提供輔助功能，它價格低、性能可靠，主要應用于車燈、外后視鏡和門鎖等對帶寬要求較低的功能中；FlexRay可以對多重安全和舒適功能進行有效管理，適用于電子線控，是一種高速數據傳遞總線，但是它的成本較高；面向媒體的系統傳輸總線(Media Oriented System Transport, MOST)運用環形拓撲的結構，一般以光導纖維作為傳導媒介，通常應用于多媒體的傳輸。目前，在車載通信系統中最為常見的仍然是CAN總線[5]。

智能汽車搭載的傳感器種類繁多，有檢測自身速度、加速度的傳感器，如攝像頭、紅外傳感器和激光雷達傳感器等，它們共同組成了智能汽車的傳感器系統[6]。通信過程中，報文傳輸的載體是CAN總線系統。它包含了收發器[7]、仲裁器[8]和網關等模塊，這些通信總線上的關鍵模塊能夠保證傳輸過程的正確性。圖1是智能車輛的通信系統[9]在工作時的過程。

圖1 智能車輛的框架

1.2 CAN協議介紹

CAN總線[10]實時性強、可靠性高，同時易于開發和擴展，因此也被廣泛應用在汽車[11]、軌道交通、航海船舶和導航等領域。

對CAN協議的驗證一般采取傳統的辦法，如仿真、模擬和測試等。仿真和模擬就是運用軟件系統對CAN總線運行環境進行模擬，分析通信過程并得出結論。Lindsey等[12]對CAN總線的IP抗輻射和加固進行研究；Kim等[13]使用了CANoe對重型貨車通信系統進行仿真，證實了它基于CAN總線通信的可靠性。CANoe是一個具有編程功能的仿真軟件，可以實時分析傳遞的信號，但是它過分依賴硬件設施，參數的個數也有限，致使實驗結果不完備。而測試的方法一般是在設計的收尾階段才能進行，不僅耗費大量時間，而且可復用度很低，造成很大的成本浪費。

(1) CAN總線結構。CAN總線是成麻花狀纏繞的雙線制結構，這樣就避免了向外輻射和電磁波干擾。與總線連接的每個電子控制單元(ECU)均可傳遞數據，并能夠選擇性地讀取自身所需數據。當其中一個ECU發生故障之后，不會影響其他電控單元，安全性能較好。CAN總線能夠實現不同速率的傳輸，高速總線被用于驅動系統中，低速總線被用于車身系統中。對于速率不同的總線連接網關，需要進行“翻譯”，網關通常是獨立控制模塊或者借用其他控制模塊。CAN總線結構如圖2所示。

圖2 CAN總線結構

(2) CAN報文格式。 CAN協議將報文劃分為數據幀、遠程幀、錯誤幀和過載幀這4種類型，每種類型都有其固定的格式，CAN協議的幀格式分為標準和擴展兩種格式，標準格式的標識符是11位，擴展格式的是29位，本文建立模型采用的是標準格式。報文中的數據全部由顯性位(0)和隱性位(1)構成，顯性位的優先級高，隱性位的優先級低。

(3) CAN的仲裁機制。CAN總線運用的是非破壞仲裁技術。其中，非破壞性指數據和時間都無損，借助逐位仲裁時幀的ID來實現。如果有發送任務時總線空閑，任一數據幀都能占用該總線，接收報文的單元收到數據后會向發送單元傳遞反饋消息，收到反饋表示任務完成，否則報文將重新發送；當兩個或以上不同ID的單元同時傳遞數據時會產生沖突現象，此時仲裁器需要進行仲裁，也就是逐位比較報文的標識符，優先級高的報文直接發送，優先級低的報文則退回，等待總線空閑時再次發送。因此優先級最高的報文發送時間就沒有損失，優先級的高低由數據包的ID決定，ID越小表明優先級越高。

2 形式化建模

形式化驗證的方法近年來在眾多領域中都發揮了相當的作用[14]，如建筑領域[15]和醫療領域[16]等。它包括模型檢測[17]和定理證明[18]，相比之下，模型檢測[19]能夠對系統進行自動化證明，減少了人工干預。時間自動機理論是模型檢測技術的重要基礎[20]之一，為實時系統的形式化驗證起到了關鍵的作用，其思想是運用時間自動機的形式建立目標系統的模型，搜索并遍歷模型的所有狀態，驗證系統是否滿足屬性的要求。

模型檢測的過程可以分為三個步驟。首先，對目標系統進行分析，從中描述出需要滿足的屬性，將其邏輯表達公式表示出來，如CTL公式和LTL公式等。其次，對系統進行合理的抽象并建立模型，建模過程中可以使時間自動機、Kripe結構或者轉移結構。最后，用模型檢測工具驗證屬性，若結果正確則說明建立的模型滿足需求；若結果錯誤則會給出反例，應該通過反例檢查模型找出問題，如果模型建立沒有問題，則需考慮該系統是否有不滿足要求的情況。

2.1 符號化模型檢測工具UPPAAL

UPPAAL[21]是一個模型檢測工具，它提供了對死鎖的檢測方法，同時運用時鐘變量，可以精準地描述模型必須滿足的時間方面的條件，更好地分析目標系統的實時性。現在已有的工作中，文獻[22]對物理信息系統進行建模與驗證，主要是對車輛系統的驗證，但是沒有考慮到傳輸速率的差別對系統產生的影響；文獻[23]對智能汽車的規劃策略問題進行了建模與驗證。

UPPAAL[24]是由Uppsala大學和Aalborg大學提出的一個圖形化的自動模型檢測工具箱，可以用時鐘變量來刻畫連續的時間變化。本文對智能汽車通信系統中各關鍵模塊分別建立時間自動機模型并組成時間自動機網絡，以此來模擬整個通信系統，然后通過窮舉搜索所有可能出現的狀況，驗證其屬性的正確性。

UPPAAL由并發進程組成[25]，每個進程都被建立成為對應的時間自動機。每個時間自動機包含一系列節點(location)來表示它的不同狀態，還有一系列變遷(transition)來表示改變狀態需要的條件和參數的更新。UPPAAL可以運用帶有有界整型變量的時間自動機模型網絡對存在并發的實時系統展開模擬，每個進程均可通過有參數控制結構、時鐘變量和進程間的通道來描述。其中，通道的作用是實現進程間的同步通信。比如，用a來表示一個通道，那么a!表示向其他進程發出了一個同步信號，a?則表示收到了一個來自其他進程的同步信號。在UPPAAL中,也可以通過共享變量實現異步通信。

UPPAAL采用巴科斯范式(BNF)語法描述目標系統的屬性，該語法對CTL公式進行了簡化，主要包括路徑公式和狀態公式，路徑公式是對模型中路徑或軌跡的描述，狀態公式是對模型中的狀態進行描述。表1給出了幾種常用的路徑公式。

表1 UPPAAL中的路徑公式

建立的屬性在模型中體現為對節點和變遷的驗證。從初始節點開始，UPPAAL遍歷每個節點和變遷形成路徑，若能夠完整遍歷該路徑，則路徑上的節點可達，變遷上的條件也可以達到。下面以圖3為例說明。

圖3 UPPAAL建模驗證實例

圖3為一個模擬燈亮度的時間自動機網絡，由User和Lamp兩個時間自動機組成。User的作用是發送press!信號，也就是按下開關；Lamp的作用是接收到在不同時間間隔中收到的press?信號，改變燈光的強弱。我們假設燈處于關閉的狀態，第一次按下開關時燈處于弱亮度，在5個時間單位內再次按下開關燈則變為強亮度，否則就會執行關燈操作。我們抽取的屬性為：

A<> y>=5 imply Lamp.off：對于所有路徑來說，兩次按開關間隔超過5個時間單位則燈處于關閉狀態。所經過的Lamp自動機中的其中一條路徑為:

A<> y<5 imply Lamp.bright：對于所有路徑來說，兩次按開關間隔在5個時間單位則燈處于強亮度狀態。所經過的Lamp自動機中的其中一條路徑為:

2.2 通信系統模型的建立

智能車輛的通信過程可以描述為以下步驟：傳感器系統將收集到的數據傳給CAN總線中的收發器，等待仲裁；仲裁器對報文的每一幀數據進行逐位仲裁，判斷各個報文的優先級，并根據優先級發送給收發器；網關對發送的報文進行判斷是否需要變速傳輸，速度一致后發送給收發器；收發器接收到反饋消息之后，將報文傳輸到車輛的主控制器上；主控制器對報文內容分析之后再經由總線系統將命令發送給各個子控制模塊；收到報文后每個子控制模塊各司其職，執行相應的操作；執行完畢，每個控制單元將會給傳感器系統發送反饋信息，至此一輪通信過程結束，可以開始新一輪的傳輸。

根據智能車輛從數據采集到處理的整個過程，關注車輛的通信過程并且忽略其他無關因素，本文對智能車載通信系統進行合理抽象。如圖4所示，抽象模型分為傳感器系統、主控制器、子控制器和CAN總線系統，其中CAN總線系統又可劃分為總線、收發器、仲裁器和網關四部分。對上述這些部分進行形式化建模和分析，忽略了與通信系統不相關的部分，并且能夠進一步明確車輛通信過程關鍵模塊之間的作用關系，保證了模型的精確和可靠。

圖4 抽象模型的框架

根據CAN總線的定義，在車輛通信系統中會有多個控制單元接入CAN總線，例如各傳感器和子控制器。為了建模的精煉，本文對各個傳感器和子控制器均只建立一個模型，必要時再在UPPAAL中根據模板將其實例化為多個模型。因此在傳感器模型中集合了多個傳感器的特征，將各傳感器是否采集數據設置為布爾變量，當傳感器發送數據時布爾變量更新為true，反之則為false；子控制器，也就是執行器中集合了多個執行器的特征，將各個執行器是否收到命令設置為布爾變量，當觸發該執行器時，布爾變量更新為true；反之則為false。

(1) 傳感器模型。傳感器系統是通信過程中不可或缺的一部分，它的作用是利用不同傳感器對外部事物的數據進行收集，并且對自身屬性進行檢測，同時傳遞數據給車輛的主控制器。及時地傳遞數據為車輛通信系統處理報文內容奠定基礎。傳感器系統在工作過程中有初始化狀態(initial)、空閑狀態(idle)、準備發送數據狀態(ready_sending)、等待仲裁狀態(wait_arb)、發送數據狀態(sending)、結束發送數據狀態(finish_sending)、準備接收反饋狀態(ready_recei-ving)、接收反饋狀態(receiving)、結束接收反饋狀態(finish)。

首先，系統處于初始狀態，每一次傳輸的開始都將變量begin置為1，一個通信周期開始之后，將begin置0，待到下一個周期開始再將它初始化為1。報文開始傳輸時，傳感器系統準備發送已經接收到的數據，向收發器發出同步信號start_data!后，如果總線系統沒有被占用，那么就進入準備發送的狀態，此時收發器收到信號之后運用函數writing_data()對各個數據包進行寫入，其中數據包包括報文ID、類型、標識符和傳輸速度等內容。在仲裁成功的情況下，數據包將會遷移到正在發送(sending)的狀態。在發送過程中如果攝像頭或者各個傳感器捕捉到緊急情況，則將相應的變量置1，最后結束一個周期的傳輸。其次，在收到子控制器處理完成命令的同步信號interruptted?之后開始接受反饋信息，并執行各個子控制模塊的工作，將相應的布爾變量更新為true，表示車輛系統對緊急情況作出了相應的反應。傳感器的模型如圖5所示。

圖5 傳感器系統的形式化模型

(2) 主控制器模型。主控制器在智能車輛的通信過程中承擔了“大腦”的工作，它是連接傳感器系統和車輛執行器的中間模塊，既要對報文數據進行分析和處理，又要分發命令給各個子控制模塊執行相應的操作，是通信系統中不可或缺的一部分。主控制器在工作過程中存在初始狀態(idle)、等待仲裁狀態(wait_arb)、仲裁狀態(arb)、發送命令狀態(sending)、結束發送狀態(finish_sending)、接收反饋狀態(receiving)。

收到傳感器系統串的同步信號start_data?和報文之后，主控制器開始處理并發送命令給各個子控制模塊，經由收發器寫入命令包和仲裁器進行仲裁，接著進行數據傳輸，最后結束整個工作周期。主控制器的模型如圖6所示。

圖6 主控制器的形式化模型

(3) 子控制器模型。子控制器在通信系統中承擔執行器的任務，智能車輛中各模塊承擔著不同的任務，上文已經分析過。收到主控制器分發的命令后，由各模塊分別執行相應的操作，結束操作之后，通過CAN總線系統為傳感器系統提供反饋，并且開始新一輪任務。子控制器在模型中定義了以下狀態：初始狀態(idle)、等待仲裁狀態(waiting_arb)、等待總線空閑狀態(wait_ack)、執行狀態(execute)、發送反饋狀態(sending)、結束發送反饋狀態(finish_ack)、接收反饋狀態(receiving)。其中，每個模板均可實例化為多個時間自動機模型。

子控制器在接收報文之后開始執行命令，過程中要求執行的時間不超過3個時間單位。執行過程中，要求通信系統在處理緊急情況時發出聲音、燈光、視覺和視頻等方面的提示，輔助駕駛員做出正確的反應。執行完畢之后向傳感器系統發送反饋信息，表示可以開始下一輪傳輸，并且將總線的狀態由忙碌變為空閑。子控制器的模型如圖7所示。

圖7 子控制器的形式化模型

(4) 收發器模型。收到傳感器發送的數據之后，收發器首先判斷CAN總線的狀態，若總線處于忙碌狀態，也就是data_active為0，那么報文進入等待的狀態；若總線是空閑狀態，也就是data_active為1，那么報文進入仲裁器進行優先級判斷。如果該報文仲裁成功，則開始發送數據；如果仲裁失敗，則重復上述步驟。收發器的模型如圖8所示。

圖8 收發器的形式化模型

(5) 仲裁器模型。數據收發器發送的同步信號readyData_arb?被仲裁器收以到后，開始進行仲裁工作，對報文的內容逐位計算，也就是比較當前數據位的值與求得的總線的值是否匹配，若不匹配就表明報文傳輸失敗，退出仲裁，該自動機遷移到請求失敗的狀態；若二者匹配，但是標識符還未比較完，那么將對下一位進行仲裁；如果二者匹配且標識符都已比較完畢，則報文傳輸成功，仲裁工作隨之完成。仲裁器的模型如圖9所示。

圖9 仲裁器的形式化模型

(6) 網關模型。結束仲裁之后，報文進入網關，在數據包中聲明了該報文發送的速度，如果它的速度與下一個報文相同，則不需要變速；如果不同，則需要將該報文的速度進行改變，并且要求整個變速的過程不超過1個時間單位。網關的工作原理如圖10所示。

圖10 網關的工作過程

網關的模型如圖11所示。

圖11 網關的形式化模型

(7) 總線模型。CAN總線在模型中存在兩個狀態：空閑狀態和忙碌狀態，當傳遞報文時，需要的總線數量data_account大于0， data_active將置為1，成為忙碌狀態，當發送報文之后，data_active恢復為0，總線也恢復為空閑狀態。CAN總線模型如圖12所示。

圖12 總線的形式化模型

3 屬性的形式化描述和驗證

通過對智能車輛通信系工作流程和特性的分析，要求它滿足的屬性可分為兩大類：安全性屬性和功能類屬性。

3.1 系統的安全性

在驗證其他屬性之前，首先要確保整個通信過程沒有死鎖的發生。

A[] not deadlock

3.2 通信系統的正確性

在報文發出之后總會收到反饋的消息，說明在這期間報文傳輸成功并且子控制器執行了相應的操作。

A<> (Sensor.sending imply Sensor.finish)

3.3 仲裁時間

由于Uppaal是以時間單位計時的，因此考慮到系統的實時性，要求仲裁時間不超過1個時間單位。

A<> t_darb<=1

3.4 網關判斷時間

考慮到系統的實時性，要求網關變速時間不超過1個時間單位。

A<> dgw_t<=1

3.5 防抱死系統(ABS_system)

緊急剎車時車輛會觸發ABS系統，此時車輛可以對制動力的大小進行控制，這樣輪胎就不會被抱死，而是邊滾邊滑。輪胎上裝有的感應速度或加速度傳感器在速度值驟減或加速度絕對值為很大的負值時，即可將數據傳輸給主控制器，主控制器經過判斷之后向ABS系統和警報系統發出命令，汽車自動觸發ABS，并且提示司機當前警告。

A<> Speed_transmitter==1 imply (ABS_system==1 and sound_warning==1 and ABS_reflect==true and Sub_controller.t_execute<=3)

3.6 防碰撞預警系統(AWS_system)

危險碰撞發生之前，及時發出警報信號提醒駕駛者。在車前裝有超聲波等傳感器，在司機精神分散或者疲勞時與前車沒有保持安全距離，傳感器將數據傳給主控制器，再由它觸發警報系統對駕駛人員進行聲音和其他形式的預警。

A<> Range_sensor==1 imply (AWS_system==1 and light_warning==1 and view_warning==1 and AWS_reflect==true and Sub_controller.t_execute<=3)

3.7 夜視輔助系統(NVA_system)

車燈上裝有紅外攝像機，在夜晚光線情況不好的情況下幫助駕駛人員提前看到燈光照不到的地方。紅外攝像機可感受前方道路的熱量情況，對駕駛者進行輔助，在車內以視頻的形式幫助駕駛人員對外界的情況進行觀察。

A<> Infrared_camera==1 imply (NVA_system==1 and video_assist==1 and NVA_reflect==true and sub_controller.t_execute<=3)

3.8 變道輔助系統(LCA_system)

前后車門之間的車身被稱為C柱，駕駛人員在駕駛位上存在C柱盲區。C柱邊緣裝24 GHz雷達傳感器，在變道時自動監測左后方或者右后方是否有車輛靠近，若有則主控制器向子控制器發送消息，對駕駛人員發出警報提醒。

A<> Infrared_camera==1 imply (NVA_system==1 and video_assist==1 and NVA_reflect==true and sub_controller.t_execute<=3)

3.9 主動防追尾系統(ARE_system)

車尾裝有超聲波傳感器，一旦后車沒有保持安全距離，則車后燈發出警報，主動警示后車駕駛人員注意保持安全距離。

A<> Radar_sensor==1 imply (LCA_system==1 and sound_warning==1 and view_warning==1 and LCA_reflect==true and Sub_controller.t_execute<=3)

4 驗證結果

4.1 驗證實例

現以通信系統的正確性為例，對驗證過程進行闡述：A<>(Sensor.sending imply Sensor.finish)。其含義是：對于所有的路徑來說，如果到達Sensor.sending數據發送狀態，那么一定會到達Sensor.finish完成處理狀態。也就是說，對于每一個傳輸的數據都可以發送并且處理成功。運用UPPAAL中的模擬軌跡功能對模型進行隨機路徑的模擬。圖13是在模擬軌跡中截取的初始狀態、發送狀態和完成狀態。

圖13 模型路徑隨機模擬過程

該屬性的驗證經過Sensor模型的以下路徑，路徑的形式化驗證描述如圖14所示。

圖14 模型路徑的形式化描述

UPPAAL可以完整地遍歷該路徑的每個節點和變遷，那么屬性驗證成功。

路徑的隨機模擬只是偌大模型中的其中一條路徑，因此為避免狀態爆炸問題，本文使用驗證器對該屬性進行驗證，UPPAAL的驗證器會枚舉所有可能的狀態路徑進行驗證，圖15所示為驗證結果。

圖15 驗證實例結果

4.2 結果分析

本文中UPPAAL軟件運行的計算機環境為：3.60 GHz的八核CPU，內存環境為8.00 GB。表2為以上屬性在該環境中的驗證結果。其中驗證總用時較短，均在秒級以下；常駐內存和虛擬內存的使用峰值也在可以接受的合理范圍內。驗證結果表明，基于CAN總線的智能汽車通信系統可以順利地傳輸數據，對外界情況作出及時的反應，滿足實時性的要求。

表2 驗證結果

5 結 語

本文研究了基于CAN總線的智能汽車通信系統的形式化驗證，通過對此類車輛的通信系統進行剖析和抽象，建立模型并且進行實驗驗證，結果表明：采用本文提供的模型檢測方法能夠有效地驗證智能車輛通信系統的邏輯正確性和實時性。通過UPPAAL軟件的驗證，能夠確保在車輛遇到突發狀況時通信系統及時發送數據，車輛及時作出正確反應，輔助駕駛員做出相應的判斷。

本文的貢獻之一是對基于CAN總線的智能汽車通信系統進行安全性和實時性的驗證，為現代汽車通信系統的安全驗證提供了一種方法，為智能汽車過渡到無人駕駛汽車提供了硬件基礎的保證；其二是對通信總線中網關進行了建模，確保差異速率下報文傳輸的正確性。實驗結果也表明了本文模型的設計邏輯可行，驗證屬性的方法正確，其能夠對智能汽車通信功能的正確性和實時性進行很好地驗證。

本研究也存在一定的不足，比如只能通過提前定義輸入的形式來定義報文內容，而不能動態地輸入數據。下一步工作可能對解決動態輸入傳輸內容的問題進行研究，同時也可以將模型檢測的方法應用到其他的系統和領域中去。