作者 |郭建上海控安可信軟件創新研究院特聘專家

版塊 |鑒源論壇 · 觀模

汽車工業發展至今，硬件方面如車身材料、發動機等已無太大升值空間，而汽車電子則有著廣闊的前景。為此各大汽車廠商對汽車電子的研究都投入了大量的人力財力。2003 年，汽車開放系統架構AUTOSAR（AUTomotive Open SystemArchitecture）由全球汽車制造商、部件供應商及其他電子、半導體和軟件系統公司聯合建立，主要目標是為汽車軟件體系架構建立一個開放的、標準化工業標準，以同時滿足供應商和生產商之間的需求。AUTOSAR 通過控制復雜度不斷增長的汽車電子體系架構，將軟件從硬件中分離開來，允許軟件的重用，從而減少二次開發和驗證的成本。AUTOSAR包括了汽車電子功能劃分、統一軟件架構和軟件開發過程等整套基于汽車電子開發的方法學。CAN、TTCAN、LIN、FlexRay等是可用于汽車內部網絡通信的協議。在現階段CAN及TTCAN協議因其穩定可靠、結構簡單、通信靈活等特點而最常被使用。基于AUTOSAR的網絡協議規范已有很多被發布。如基于AUTOSAR的CAN協議、基于AUTOSAR的TTCAN協議等，這些規范詳細闡述了在AUTOSAR規范下該網絡協議的驅動及接口規范，隱藏了底層網絡通信的細節，向上層應用軟件提供調用底層服務的接口。通過這種方式使軟硬件分離，使上層軟件的開發更為靈活，對功能的擴充更方便，縮短了開發周期。

本文針對AUTOSAR的TTCAN協議進行研究，并用Timed CSP（Timed Communication Sequential Processes）形式化語言對其進行建模，通過LTL（linear temporal logic）及斷言（Assertion）對TTCAN模型需要滿足的性質進行描述，運用模型檢驗工具PAT完成了對模型的驗證。

01AUTOSAR體系架構

AUTOSAR的主要目標是為汽車電子創建一個開放的、標準化的軟件架構，這個架構有利于車輛電子系統軟件的交換與更新，并為高效管理愈來愈復雜的車輛電子軟件系統提供了一個基礎。此外，AUTOSAR在確保產品及服務質量的同時，提高了產品研發的效率。AUTOSAR定義了設計汽車系統的方法和描述它們的軟件的架構方式。圖 1 展示了AUTOSAR軟件分層體系架構。

圖1AUTOSAR軟件分層體系架構

應用層（application layer）

包含了實現所需功能的軟件組件SWC（SoftWare Component）的規約，它形成了OEM（Original Equipment Manufacturer）廠商之間的競爭基礎。

運行時環境層 RTE（RunTime Environment）

為應用軟件提供了通信服務，它使 AUTOSAR的軟件組件獨立于特定的ECU。RTE是虛擬功能總線VFB（Virtual Function Bus）的一個實現，不指定用來交換數據的通信技術。因此，AUTOSAR可用LIN、CAN、TTCAN或者FlexRay等多種通信平臺。用VFB定義軟件組件的數據交換可使它們獨立于底層的硬件平臺，此外，可以使注意力集中到軟件組件之間的通信而不用關心數據是否在ECU 內部或ECU之間傳輸。

基礎軟件層BSW（Basic SoftWare）

由服務層、ECU抽象層、復雜驅動層和MCU（Micro Controller Unit）抽象層等子層組成。服務層處于基礎軟件層的頂層， 包含了操作系統、汽車網絡通信、管理服務、內存服務和診斷服務。ECU 抽象層包含了輸入輸出（I/O）和通信硬件抽象，它使更高的軟件層獨立于ECU 硬件組件。復雜驅動層是硬件和 RTE 之間的橋梁，它提供與AUTOSAR無關的、專用的功能，如設備驅動等。MCU抽象層處于基礎軟件層的最底層，它包含了直接訪問的微控制器內部設備的驅動和內存映射的微控制器外部設備的驅動。

02AUTOSAR的TTCAN協議

基于AUTOSAR的網絡通信協議位于體系架構的基礎軟件層中，AUTOSAR為其提供接口的規范。TTCAN協議在AUTOSAR基礎軟件層的接口，位于通信硬件抽象層和通信服務層之間，是為上層通信層提供 TTCAN 協議驅動服務的接口。圖 2 是AUTOSAR規范下的 TTCAN協議層次的架構。TTCAN協議接口模塊是CAN接口模塊的擴展，它包含了TTCAN協議所有與硬件獨立的任務。

圖2AUTOSAR規范下的TTCAN協議層次架構

TTCAN協議接口主要完成上層通信層對控制流和數據流的需求，比如：消息傳輸需求、消息傳輸確認、消息接收指示、出錯通知等。TTCAN協議接口的一個典型流程是，接收來自上層通信層的消息請求，通過TTCAN協議驅動傳輸給 TTCAN協議控制器完成消息的傳輸，然后向上層通信層返回消息成功傳輸的確認。TTCAN協議接口為TTCAN協議網絡的控制和服務提供了訪問低層服務的通信抽象，通過接口將TTCAN協議狀態，管理器的狀態變化請求推送到底層的TTCAN協議驅動，然后底層事件再通過接口推送到高層相關的網絡管理模塊。

03基于AUTOSAR的TTCAN協議的形式化建模與分析

AUTOSAR規范下TTCAN協議的抽象主要為三個層次。

一是應用層

，即軟件組件層，包含了各種軟件組件消息傳輸請求的序列，對應于 TTCAN 協議的系統矩陣。

二是運行時環境層

，對上層應用層隱藏了下層的通信細節，實現虛擬功能總線，是對TTCAN協議通信通道的抽象。

三是基礎軟件層

，即TTCAN通信網絡所處位置，完成TTCAN協議基本的通信功能，即節點消息傳輸、總線仲裁和錯誤處理功能。

圖3基于AUTOSAR的TTCAN協議抽象

圖3描述了基于AUTOSAR的TTCAN協議抽象，運行時環境層可以接收來自于軟件組件的任何數據請求，通過內部的接口調用底層基礎軟件的通信功能，完成消息的傳輸。在AUTOSAR軟件體系架構中，位于運行時環境層之下的基礎軟件層對于應用層來說是不可見的，因此，基礎軟件層可采用不同的通信協議來完成通信功能。基于AUTOSAR的TTCAN協議則是在基礎軟件層中采用了TTCAN協議來進行消息的傳輸。

圖4TTCAN協議與基于AUTOSAR的TTCAN協議的關系

圖4簡單描述了這兩者之間的關系。AUTOSAR規范中定義了一系列TTCAN協議的接口，通過對這些接口的實現完成TTCAN協議的各種功能。本文主要研究TTCAN協議中節點消息傳輸、總線仲裁和錯誤處理的功能如何在AUTOSAR規范下實現，并可通過定義的接口進行調用，從而完成消息的傳輸。

對TTCAN協議和基于AUTOSAR的TTCAN協議進行分析、形式化建模和驗證的研究框架如圖 5 所示。該框架主要分為三個階段：

圖5基于AUTOSAR的TTCAN協議建模與分析框架

第一階段

對TTCAN協議的需求進行分析，對于消息傳輸相關的四個主要部分系統矩陣、節點消息傳輸、總線仲裁及錯誤處理進行抽象，并分析這四個部分之間的關系以及消息的傳輸過程。分別對這四個部分進行形式化的描述，以Timed CSP建立模型。同時，在這一階段，分析并提取TTCAN協議中死鎖、安全性、不變性及公平性等相關的性質，以LTL公式及斷言的形式描述并加以文字注釋說明。

第二階段

根據AUTOSAR軟件體系架構和基于AUTOSAR的TTCAN協議規范，在TTCAN模型的基礎上，將其遷移至AUTOSAR，這一過程關鍵之處在于明確TTCAN模型各功能模塊應處于AUTOSAR體系結構的哪一層次。然后在分析的基礎上，以Timed CSP建立基于AUTOSAR的TTCAN層次模型，該模型包含了軟件組件、運行時環境和基礎軟件三個層次。其中，軟件組件實現TTCAN協議模型中系統矩陣的功能，為系統提供消息傳輸請求的列表；運行時環境為上下層之間的通信提供了虛擬功能總線，包含了多種接口以供上層模塊調用底層通信服務，是對TTCAN協議模型通信通道的抽象；基礎軟件包含了TTCAN協議模型中的節點消息傳輸、總線仲裁和錯誤處理模塊，提供消息傳輸的服務。最后對模型進行性質的提取，提取的性質不僅需要滿足TTCAN協議的需求，還要滿足AUTOSAR規范的需求。

第三階段

是模型的實現和性質的驗證階段。模型檢測工具PAT支持并發實時系統建模、模擬以及推理，支持Timed CSP建模語言，同時也支持LTL公式及斷言描述性質。因此，以PAT實現模型，使模型能得到準確的描述。建模實現的同時，對前兩個階段中提取的性質在工具PAT中進行驗證，并對驗證結果進行分析。圖6所示的是在PAT上模型實現的部分代碼，圖7給出了PAT對模型的驗證結果。

圖6模型在PAT中的實現

圖7基于AUTOSAR的TTCAN協議模型性質驗證結果

04小結

AUTOSAR規范的提出為高效管理愈來愈復雜的汽車電子提供了一個基礎。AUTOSAR通信棧位于運行時環境（RTE）與微控制器抽象層（MCAL）之間，其簡化ECU之間的通信服務，實現不同類型或速率總線間的數據交互，并對應用層隱藏了與總線相關的協議和報文的屬性。本文針對AUTOSAR 的TTCAN通信協議進行了研究，實現其形式化建模與分析。

審核編輯黃昊宇