基于Modelica-AADL的信息物理系统形式化建模与性能评价

发布时间：2021-11-09 16:38

　　信息物理融合系统（CPS）是物联网进一步发展的产物,CPS将物理过程与信息计算过程紧密联系,是一种复杂的混合系统,Modelica与AADL是适合用以信息物理融合系统的嵌入式系统体系结构建模语言,本文基于Modelica-AADL的建模方式,制定了适用于CPS的形式化性能评价语言及算法,完成系统的性能需求的规约,进一步分析与评价信息物理融合系统的相关性能。首先,应用两种不相关的建模语言Modelica与AADL为CPS建模,构建一种组合式建模方式Modelica-AADL,其中,Modelica应用于物理系统的建模,AADL应用于信息系统的建模,并对Modelica进行了相关的概率扩展,设计了接口将两种建模方式组合。同时,将Z语言引入到Modelica-AADL模型中,用以描述系统中的数据约束。为了进行系统分析评价工作,制定了相关规则与算法将非形式化的Modelica-AADL描述转换成形式化的概率混成自动机模型。之后定义面向CPS的形式化性能评价语言CTEL,结合相关具有统计意义的评价量计算方式,计算出性能评价的值,利用CTEL对系统的性能性质进行描述,得到分析结果。最后,结合统计方... 

【文章来源】：南京航空航天大学江苏省 211工程院校

【文章页数】：85 页

【学位级别】：硕士

【部分图文】：

智慧城市架构案例CPS在生活中应用场景越来越广，人们对于相应系统的质量需求快速提升

图 1.3 CPS 的结构实例CPS 软件的形式化建模是CPS软件属性验证的前提和基础。关于CPS软件的形式化可以归纳分为如下几类：形式化推理方法推理证明需要数学逻辑描述系统方面的特征，逻辑形式由公理和推论组成的规则定理证明器的支撑。常用的检验证明器包括 HOL、Coq、LCF 和 LEGO[5]；复合证 PVS[6]、Analytica（将符号代数与定理证明整合）和 Step（将决策过程与交互式推合），用户推演推算工具包括 RRL、LP、ACL2、Eves 等[7]。Petri 网建模Petri 网是应用广泛的计算机领域传统的模型分析及验证方法，适用于描述系统中步行为。通常，为了增强能力，将扩展信息引入Petri 网，不会破坏Petri 网结构的步和并发的表达。基于Petri 网的验证工具目前比较通用的是EXSPECT。自动机建模

图 3.1 简单电路举例p)表示电流从电源 VS 进入电阻 R，系统状态由表示电流从电阻 R 流到电容 C，系统状态由1s)表示电流从电容 C 流到电源 VS 的另一极，系统可以表示为1 230 1 2 3c ccs s s s，其中是变量 v，i 和一些常量 c，r 等的具体值状态 中引入概率因子物理事件进行响应，而现实中的物理事件常常很有必要。性有助于我们将概率因子引入其中。Modelic者事件的发生。可以模拟事件的瞬时发生，改为。理事件行为产生的系统响应建立 Modelica 对 CPS 中通常需要传感器来监测物理环境中的

【参考文献】：
期刊论文
[1]信息物理融合系统概述[J]. 姜宏.  电脑知识与技术. 2011(35)
[2]信息物理融合系统研究综述[J]. 王中杰,谢璐璐.  自动化学报. 2011(10)
[3]信息物理融合系统（CPS）研究综述[J]. 黎作鹏,张天驰,张菁.  计算机科学. 2011(09)
[4]基于时间自动机的物联网服务建模和验证[J]. 李力行,金芝,李戈.  计算机学报. 2011(08)
[5]复杂嵌入式实时系统体系结构设计与分析语言:AADL[J]. 杨志斌,皮磊,胡凯,顾宗华,马殿富.  软件学报. 2010(05)



本文编号：3485707