摘要

信息物理融合系统(CPS)是物联网进一步发展的产物,CPS将物理过程与信息计算过程紧密联系,是一种复杂的混合系统,Modelica与AADL是适用于信息物理融合系统(CPS)的嵌入式系统体系结构建模语言。利用Modelica对物理系统部分建模,AADL对信息系统部分建模,将信息物理系统的建模分割开来,设计了Modelica-AADL接口将二者结合起来,使得物理世界与计算过程相融合。概率混成自动机是对信息物理融合系统验证分析的有效形式化建模方式,Modelia-AADL模型无法进行直接的形式化模型检测工作,根据Modelica与AADL行为附件各自的特点,抽象出状态,定义了一系列规则,给出转换算法,完成了MA模型向概率混成自动机的转换,使得系统模型能够形式化描述,有助于信息物理融合系统的可靠性与安全性验证。