球友会qy

近期，中国科研实验室软件研究所天基综合信息系统全国重点实验室针对信息物理融合系统（CPS）的形式化建模与验证，提出了一种基于扩展体系结构分析与设计语言（AADL）的建模与验证方法，为航空航天、高速列车、车联网等安全攸关系统的设计与验证给予了新的思路。相关论文Modeling and Verification of Hybrid Systems by Extending AADL被软件工程领域顶级期刊ACM TOSEM接收，第一作者为助理研究员徐雄。

安全攸关信息物理融合系统（Cyber-Physical Systems, CPSs）是一类复杂的嵌入式系统，在航空航天、高速列车等安全攸关领域发挥着关键作用。传统的建模方法往往难以同时兼顾软件功能、物理环境和系统架构这三个关键维度，导致系统设计存在潜在风险。在众多架构型建模语言中，AADL（体系结构分析与设计语言）表现最为出色。然而，AADL虽然擅长描述系统架构和硬件平台，却难以准确描述系统的软件功能和物理环境。

因此，研究团队为实现CPS“物理-软件-硬件”三层架构的统一建模，对广泛应用于实时嵌入式系统的AADL进行了扩展，设计了Hybrid Annex附件，使AADL能够准确描述离散的软件功能、陆续在的物理变化以及二者的交互过程；还建立了从扩展AADL模型到形式化模型HCSP（混成通信顺序进程）的自动转换框架，支持在形式模型层面对CPS进行仿真与验证。

研究团队采用扩展的AADL为一个汽车自动巡航系统建模，顺利获得构建包含物理行为层、软件功能层和硬件平台层的三层模型，可以实现系统行为的仿真和验证。实验结果表明，该方法能够有效观察不同总线配置下的系统行为差异，为系统优化给予了重要依据。此外，研究团队还利用基于混成霍尔逻辑（HHL）的定理证明工具，验证了系统中紧急控制组件的安全性。

汽车自动巡航控制系统的扩展AADL架构图

汽车在不同总线配置下的行车差异对比

论文链接：http://dl.acm.org/doi/10.1145/3737698