面向CPS的混成进程演算建模与基于统计的性能评价

论文摘要

信息物理融合系统(Cyber physical Systems,简称CPS)是软件和硬件设备紧密联系、相互影响相互作用的新一代智能系统。随着自动化、通信以及计算机技术的不断发展,CPS逐渐走向成熟并越来越多的应用到实际生产和生活中。人们对于CPS的要求已经不再局限于系统的功能扩展,CPS的性能指标开始被重视。在保证系统安全性和可靠性的前提下,人们倾向于采用性能更加优秀的系统。目前关于对CPS性能评价相关的形式化方法研究还很少,本次课题在对CPS特征和性能指标相关研究整理和总结的基础上,提出将形式化建模和分析的方法引入到CPS的性能评价中。利用统计模型检测和性能评价语言连续时间随机语言(Continuous Time Stochastic Language,简称CSTL)对基于HPCCS的CPS模型进行性能评价。本文的创新点如下:(1)本文在进程演算TCCS的基础上扩展概率选择和微分方程,提出一种新的信息物理融合系统建模语言HPCCS。体系结构分析与设计语言(Architecture Analysis and Design Language,简称AADL)是一种常用的体系化建模语言,利用AADL可以方便地对大型系统建模,如航电系统、列控系统等。通过扩展AADL随机行为和混成附件,提出用于CPS建模的混成AADL建模规范。由于AADL是半形式化建模语言无法直接对其进行形式化验证,本文提出AADL到HPCCS的模型转换算法,通过对转换后的HPCCS模型检测实现检测AADL模型的目的。(2)信息物理融合系统的性能评价需要一个表达能力足够并且不存二义性的性能评价语言,本文在PLTL和CTL的基础上提出一种性能评价语言CTSL。通过基于实值状态公式的CTSL可以刻画传统时序逻辑无法描述的系统性能指标。文中通过实例说明如何使用CTSL公式描述系统性能指标。(3)为了求解给定HPCCS模型的CTSL公式结果,首先利用离散化算法将模型离散化,然后通过对离散化模型的路径遍历计算出CTSL公式的精确解。由于精确求解算法随着并发进程数的增加面临状态空间爆炸的问题,本文采用贝叶斯统计模型检测算法,将CTSL分为四类公式,根据四类公式的性质分别给出贝叶斯性能评价算法。通过本文提出的贝叶斯性能评价算法,提高CTSL公式计算的效率。同时贝叶斯性能评价算法分析可以提供反例信息,供开发者找到系统的性能瓶颈。

论文目录

• 摘要
• Abstract
• 第一章 绪论
•   1.1 研究背景与意义
•   1.2 国内外研究现状
•     1.2.1 CPS体系结构与建模方法
•     1.2.2 CPS性能评价与模型检测
•   1.3 本文研究内容
•   1.4 论文组织结构
• 第二章 相关概念和预备知识
•   2.1 进程演算
•     2.1.1 进程演算的基本概念
•     2.1.2 CCS的语法和操作语义
•     2.1.3 互模拟
•   2.2 模型检测与性能评价
•     2.2.1 模型检测技术
•     2.2.2 性能评价技术
•   2.3 AADL建模规范
•     2.3.1 AADL简介
•     2.3.2 AADL建模元素
•   2.4 本章小结
• 第三章 随机混成系统建模语言HPCCS
•   3.1 随机混成系统
•   3.2 带数据约束的随机混成系统规范HPCCS
•     3.2.1 HPCCS语法
•     3.2.2 HPCCS操作语义
•   3.3 面向CPS的混成AADL建模与模型转换
•     3.3.1 面向CPS的混成AADL建模规范
•     3.3.2 混成AADL到 HPCCS的转换规则
•     3.3.3 混成AADL建模与模型转换实例
•   3.4 本章小结
• 第四章 利用近似互模拟离散化抽象HPCCS
•   4.1 λ-互模拟
•   4.2 带标记迁移系统上的近似互模拟
•   4.3 离散化HPCCS进程
•     4.3.1 离散化连续过程
•     4.3.2 离散化HPCCS进程
•   4.4 基于离散化HPCCS的 CPS安全性分析
•   4.5 飞行导航系统验证实例
•   4.6 本章总结
• 第五章 基于统计的CPS性能评价
•   5.1 面向CPS的性能评价语言CTSL
•   5.2 面向CTSL的统计模型检测方法
•     5.2.1 CTSL到混成自动机的转换
•     5.2.2 基于自动机的CPS性能评价机制
•   5.3 结合统计模型检测的CPS性能评价框架
•     5.3.1 基于贝叶斯的区间估计
•     5.3.2 基于贝叶斯因子的假设检验
•   5.4 算法实现
•     5.4.1 贝叶斯区间估计（E（φ ≥r））
•     5.4.2 贝叶斯区间估计（E（φ））
•     5.4.3 贝叶斯假设检验（E（φ ≥k） ≥r ）
•     5.4.4 贝叶斯假设检验（E（φ） ≥r）
•   5.5 案例分析
•     5.5.1 机场调度的形式化建模
•     5.5.2 机场调度的性能评价指标
•     5.5.3 实验方法与量化分析
•   5.6 本章小结
• 第六章 总结
•   6.1 论文总结
•   6.2 未来工作展望
• 参考文献
• 致谢
• 在学期间的研究成果及发表的学术论文

文章来源

类型: 硕士论文

作者: 曹雪岳

导师: 曹子宁

关键词: 信息物理融合系统,进程演算,性能评价,统计模型检测,离散化

来源: 南京航空航天大学

年度: 2019

分类: 基础科学,信息科技

专业: 数学,自动化技术

单位: 南京航空航天大学

分类号: TP18;O212.8

DOI: 10.27239/d.cnki.gnhhu.2019.001723

总页数: 94

文件大小: 2733K

下载量: 54