[發明專利]基于汽車開放架構系統到統一軟硬件表示的形式化系統模型轉換和可靠性分析方法

有效

• 申請號: 202010160806.2
• 申請日: 2020-03-10
• 公開（公告）號: CN111400073B
• 公開（公告）日: 2021-08-20
• 發明（設計）人: 晏榮杰;蘇靜;嚴俊;楊俊杰;黃凱
• 申請（專利權）人: 中國科學院軟件研究所
• 主分類號: G06F11/00
• 分類號: G06F11/00;G06F11/26
• 代理公司: 北京君尚知識產權代理有限公司 11200
• 代理人: 邱曉鋒

本發明公開了一種基于汽車開放架構系統到統一軟硬件表示的形式化系統模型轉換和可靠性分析方法。本發明的主要思想是將汽車開放架構的分層結構映射成形式化的系統模型，分別包括具有軟件應用冗余的抽象模塊、硬件抽象模塊、軟件與硬件交互的中間模塊，同時包含軟件的隨機或中斷行為、軟件內部依賴關系、軟件運行于硬件上的約束。該系統模型可以用于形式化分析軟硬件協同系統的實時性，并保證汽車開放系統架構中實際系統安全攸關功能的可靠性。

技術領域

本發明涉及一種將基于汽車開放架構的系統轉換到統一軟硬件表示的形式化系統模型的方法，以及利用該形式化系統模型對自動駕駛系統進行可靠性分析的方法，通過對系統模型的分析與驗證保證實際系統的可靠性，屬于計算機嵌入式系統分析領域。

背景技術

自動駕駛技術蓬勃發展，自動駕駛系統的可靠性是制約著該技術廣泛應用的關鍵因素之一。近期出現的開放式汽車軟件架構，通過對依賴于硬件的軟件、不依賴于硬件的軟件的封裝，便于不同軟件的集成，增加了功能的重用性，提高了軟件質量，提升了系統配置的靈活性。越來越多的廠商與公司使用這種架構，使得它逐漸成為汽車電子/電氣設計的發展方向。

目前，該開放架構的工具鏈尚缺乏形式化分析與驗證環節。然而，確保自動駕駛核心系統功能的正確性、可靠性，將有助于推廣自動駕駛技術的應用。因此，本發明將基于汽車開放架構的系統轉換為統一軟硬件表示的形式化系統模型，通過對系統模型的分析與驗證，保證實際系統功能的可靠性。

發明內容

本發明的目的在于提出一種汽車軟件架構的形式化系統模型，用于安全攸關系統的驗證與確認。該方案不僅考慮了對硬件瞬時故障的容錯，還將基于汽車開放架構的系統轉換為封裝了時序行為和時間約束的形式化系統模型，通過對系統模型的功能驗證與性能分析，保證實際系統的可靠性。

本發明中提出的系統模型是對汽車開放架構的抽象，架構上包含應用模塊、硬件模塊、依賴于硬件的軟件模塊；功能上不僅能夠表示事件觸發的中斷行為，也能表示隨機行為，并具有一定的主動容錯能力。

為了實現本發明的目的，本發明采用的技術方案如下：

一種基于汽車開放架構系統到統一軟硬件表示的形式化系統模型轉換方法，包括以下步驟：

1)建立軟件應用中任務的主動冗余，按照軟件應用中任務的依賴關系將冗余展開；

2)根據展開后的軟件應用中任務的依賴關系、軟件應用到硬件的部署以及汽車開放架構的特征，構建包含軟硬件交互的時序行為和時間約束的形式化系統模型。

進一步地，其中的步驟1)中，采用軟件應用中任務的主動冗余保證硬件出現瞬時故障的可靠性(容錯性)。其中，冗余是指任務的副本，主動冗余是指部署任務的多個副本同時運行，使用少數服從多數的表決器給出輸出結果。這樣個別副本的故障不影響任務的最終輸出結果，可以避免故障的檢測與恢復過程。運行冗余需要保持與其余任務的依賴關系及不同副本之間的同步關系。根據軟件應用中原有任務間依賴關系(若任務b依賴于任務a執行后的結果，簡稱b依賴a，稱a是b的前驅，b是a的后繼)，將冗余展開，具有冗余的任務依賴關系展開過程描述如下：

1-1)遍歷任務之間的依賴關系，確定依賴關系的深度；

1-2)從最深的非空依賴層開始，根據每個任務的副本的個數，加入副本、副本結果表決器，并構造任務、副本、副本與表決器之間的關聯關系，直到遍歷完所有層；其中，依賴層是指依賴于上一層其他任務輸出的任務組成的集合；“副本結果”是指任務副本執行后輸出的結果，表決器收集任務副本的輸出并給出最終的輸出結果，表決器的作用是按照少數服從多數的方式給出任務的輸出結果；

1-3)當所有的任務都被遍歷過后，展開過程終止。

步驟1-1)的具體細節如下：

1-1-1)將不存在任何前驅的任務t加入初始層Q₀層；