近日，中國科學院軟件研究所科研人員針對信息物理融合系統的形式化建模和驗證，提出了基于擴展體系結構分析與設計語言的建模與驗證方法，為高速列車、車聯網等安全攸關系統的設計與驗證提供了新思路。
安全攸關信息物理融合系統是復雜的嵌入式系統。傳統的建模方法往往難以同時兼顧軟件功能、物理環境和系統架構三個維度，導致系統設計存在潛在風險。在眾多架構型建模語言中，體系結構分析與設計語言表現得最為出色。然而，體系結構分析與設計語言擅長描述系統架構和硬件平臺，卻難以準確描述系統的軟件功能和物理環境。
該研究為實現信息物理融合系統“物理-軟件-硬件”三層架構的統一建模，擴展了應用于實時嵌入式系統的體系結構分析與設計語言，設計了Hybrid Annex附件，使體系結構分析與設計語言能夠準確描述離散的軟件功能、連續的物理變化及二者的交互過程；建立了從擴展體系結構分析與設計語言模型到形式化模型混成通信順序進程的自動轉換框架，支持在形式模型層面對信息物理融合系統進行仿真與驗證。
進一步，該研究采用擴展的體系結構分析與設計語言為一個汽車自動巡航系統建模，通過構建包含物理行為層、軟件功能層和硬件平臺層的三層模型，可實現系統行為的仿真和驗證。實驗表明，該方法能夠有效觀察不同總線配置下的系統行為差異，為系統優化提供依據。同時，研究還利用基于混成霍爾邏輯的定理證明工具，驗證了系統中緊急控制組件的安全性。
相關研究成果發表在ACM TOSEM上。