MA建模的概率混成自动机转换方法研究

摘要

Cyber physical system (CPS) is the product of the further development of the Internet of things, which is a complex mixed system that closely involves physical process and cyber compute process.Modelica and AADL belong to modeling languages for embedded system structure which are suitable for cyber physical system.The Modelica-AADL interface is designed for combing Modelica and AADL model.Applying for cyber physical system, Modelica is utilized to implement the physical system model and AADL is taken for cyber system model.Probabilistic hybrid automata is an effective strategy for the formal verification and analysis of CPS.According to the characteristics of Modelica and AADL behavior annex model, the states for one system can be constructed, and a series of rules and definitions are given.Together with the transformation algorithm, the procedure of transformation from MA model to probabilistic hybrid automata is completed in detail so that the system model can be formally described, which is helpful for reliability and security verification of CPS in the further work.%信息物理融合系统 (CPS) 是物联网进一步发展的产物, CPS将物理过程与信息计算过程紧密联系, 是一种复杂的混合系统, Modelica与AADL是适用于信息物理融合系统 (CPS) 的嵌入式系统体系结构建模语言.利用Modelica对物理系统部分建模, AADL对信息系统部分建模, 将信息物理系统的建模分割开来, 设计了Modelica-AADL接口将二者结合起来, 使得物理世界与计算过程相融合.概率混成自动机是对信息物理融合系统验证分析的有效形式化建模方式, Modelia-AADL模型无法进行直接的形式化模型检测工作, 根据Modelica与AADL行为附件各自的特点, 抽象出状态, 定义了一系列规则, 给出转换算法, 完成了MA模型向概率混成自动机的转换, 使得系统模型能够形式化描述, 有助于信息物理融合系统的可靠性与安全性验证.