[發明專利]一種基于特征配置的系統層綜合模型安全驗證方法

有效

• 申請號: 201710146160.0
• 申請日: 2017-03-13
• 公開（公告）號: CN107038281B
• 公開（公告）日: 2020-06-16
• 發明（設計）人: 魏歐;羅煒麟;李宙州
• 申請（專利權）人: 南京航空航天大學
• 主分類號: G06F30/20
• 分類號: G06F30/20;G06F30/15;G06F111/20
• 代理公司: 南京鐘山專利代理有限公司 32252
• 代理人: 戴朝榮

本發明公開了一種基于特征配置的系統層綜合模型安全驗證方法，將用戶建立的SLIM模型轉換SNIP模型檢測器可以識別的fPromela+TVL模型，然后借助SNIP模型檢測器進行安全性驗證，通過驗證結果找出系統設計問題，基于SLIM語言的特點，主要包含三個步驟：步驟一，標定模型的轉換；步驟二，基于特征配置的故障模型的轉換；步驟三，基于SNIP的SLIM擴展模型的安全性分析。本發明實現了基于軟件產品線特征配置思想的SLIM擴展模型到fPromela+TVL模型的轉化并利用SNIP工具分析系統缺陷。

技術領域

本發明涉及一種模型安全驗證方法，特別是一種基于特征配置的系統層綜合模型安全驗證方法。

背景技術

伴隨著航空航天技術的發展，現代太空任務和諸如航天器這樣的安全關鍵系統的設計正面臨著巨大的挑戰。“基于組件的工程(component-based)”在工程師進行復雜的系統設計中是一個重要且行之有效的典范。在基于組件的工程的設計中，核心思想是組件的行為(組件實現)和單個組件之間的交互需要給予清楚的區分。其中，組件可能是以層次化的結構進行復合組成的可視化模型；而組件實現的內部結構通過分解成更小的子組件、軟硬件綁定和利用端口連接后的交互被指定；組件的行為通常被描述成一種有限狀態機——文本形式的模式遷移圖。

由于安全關鍵系統所涉及的應用場景愈發復雜和多變、系統設計涉及到多樣化的需求(如：功能正確，可靠，可觀測，性能等)，這些需求在開發早期由不同團隊或者領域專家提出，而這些需求提出者之間缺少充分交流，導致需求整合后出現一些問題。面對這些挑戰，由歐洲宇航局(ESA)贊助的COMPASS項目，提出了一個為航空航天領域安全關鍵機載系統量身定制的、綜合的、基于模型的系統開發方法，完成需求分析、系統建模、系統功能正確性和性能分析工作。該方法基于系統層綜合建模語言SLIM(System-Level IntegratedModelling)，為系統工程師提供了簡便的方法，用來描述標定的軟硬件行為以及系統發生(概率)故障、故障傳播所引起的系統退化和故障情況下系統的恢復。這種方法的根本特點是對模型進行擴展：從系統的標定模型和一系列可能的故障出發，擴展操作將兩者結合產生了一個對發生故障后系統行為的描述。

由于SLIM是一種半形式化的建模語言，只是對系統的行為進行了描述，不能對SLIM模型進行非功能屬性進行分析。

發明內容

本發明所要解決的技術問題是提供一種基于特征配置的系統層綜合模型安全驗證方法，它實現了SLIM模型到fPromela模型的轉換，利用集成的SNIP工具完成SLIM模型的檢測，解決了單一SLIM模型不能進行非功能屬性進行分析的缺陷問題。

為解決上述技術問題，本發明所采用的技術方案是：

一種基于特征配置的系統層綜合模型安全驗證方法，其特征在于包含以下步驟：

步驟一：標定模型的轉換，從根組件root開始,每個控制組件c∈component實例被轉換成唯一的進程，從而實現組件的行為；通過”active”申明,一個進程通過SNIP被自動實例化；每個組件都使用一個全局申明的無緩沖通道，用來完成組件和上層組件的同步通信；組件的不同模式m∈mode(c)用程序標簽mode_m表示，并用一個do-loop以實現所有的行為；

步驟二：基于特征配置的故障模型的轉換；在完成標定模型的轉換后，對于指定組件所配置的故障，需要關聯錯誤模型內的信息，將故障信息加入標定模型中以完成轉換，包括：故障原因、故障下的不同系統模式以及組件模式/錯誤狀態的變遷；

步驟三：基于SNIP的SLIM擴展模型的安全性分析，以上兩部分得到了與SLIM擴展模型等價的fPromela+TVL模型，使用線性時序邏輯對安全需求進行規約，從而得到需要驗證的安全性需求LTL公式，并利用軟件產品線模型檢測工具SNIP驗證fPromela+TVL模型是否滿足安全性需求的LTL規約。

進一步地，所述標定模型的轉換具體過程為，