基于混成自动机的事件驱动的CPS系统监控方法研究

论文摘要

信息物理融合系统(CPS系统)被认为是下一代嵌入式系统,具有广阔的应用前景。CPS系统涉及信息、物理等多方面,本身复杂度高,而且CPS系统往往运行于不确定的物理环境中,这使得应用传统的形式验证技术去验证完全的系统行为变得不实际。因而,运行时监控作为一种轻量级的验证技术,为监控和验证系统运行时的动态行为提供了一种切实可行的方法。在深入学习研究CPS系统和软件运行时监控相关理论和技术的基础上,本文面向CPS系统的监控问题主要展开了以下工作:1、对CPS系统的理论基础及现有研究成果,以及软件运行时监控相关技术和方法进行深入学习研究,分析CPS系统监控问题的主要困难。2、基于混成自动机模型,论文提出了一个事件驱动的CPS系统性质监控理论框架,该框架结合基于模型的设计和形式分析于一体,能够对由时序逻辑MEDL表达的安全性质进行有效的监控。3、针对工业界广泛使用的CPS系统建模平台——Simulink/Stateflow,论文随后提出了由PEDL/MEDL规约生成监控器模型的方法,设计了由PEDL/MEDL向Stateflow状态图转换的规则,并实现了PEDL/MEDL——Stateflow状态图的自动转换工具。4、论文以交通CPS系统领域典型的应用案例——CACC系统为应用背景,展示了如何利用对本框架对系统模型注入监控能力,在系统运行过程中,监控其动态行为,证实了本文所提出和设计的监控框架的有效性。

论文目录

• 摘要
• ABSTRACT
• 第一章 绪论
• 1.1 课题研究背景和意义
• 1.2 论文研究内容
• 1.3 主要的创新点
• 1.4 论文结构
• 第二章 相关工作
• 2.1 CPS 系统模型
• 2.1.1 CPS 抽象模型
• 2.1.2 CPS 系统建模工具
• 2.2 软件运行时监控技术
• 2.3 小结
• 第三章 事件驱动的 CPS 系统监控框架
• 3.1 框架介绍
• 3.2 基于混成自动机的模型构造
• 3.3 基于 PEDL/MEDL 的监控需求表达
• 3.3.1 事件与条件逻辑
• 3.3.2 PEDL——原子事件定义语言
• 3.3.3 MEDL——性质规约定义语言
• 3.3.4 MEDL 语义扩展
• 3.4 监控能力形成
• 3.4.1 模型插装
• 3.4.2 生成监控自动机
• 3.4.3 监控实施
• 3.5 小结
• 第四章 基于 Simulink/Stateflow 的 CPS 系统监控框架实现
• 4.1 基于 Simulink/Stateflow 的 CPS 系统监控框架介绍
• 4.2 基于 Simulink/Stateflow 的 CPS 系统建模
• 4.3 PEDL/MEDL 到 Stateflow 状态图生成规则
• 4.3.1 Stateflow 相关语法概念
• 4.3.2 生成规则
• 4.4 面向 Stateflow 的监控器生成
• 4.4.1 基本思想
• 4.4.2 PEDL/MEDL 脚本生成 Stateflow 状态图算法
• 4.5 小结
• 第五章 汽车协同自适应巡航控制案例分析
• 5.1 汽车协同自适应巡航控制（CACC）系统描述
• 5.1.1 CACC
• 5.1.2 CACC 工作模式
• 5.2 基于 Simulink/Stateflow 的 CACC 系统模型构建
• 5.2.1 汽车物理模型
• 5.2.2 CACC 控制器
• 5.3 CACC 监控需求
• 5.3.1 PEDL/MEDL 安全规约表达
• 5.3.2 生成的观察状态图和监控器状态图
• 5.4 CACC 系统模型监控仿真实验
• 5.4.1 情景描述及参数设置
• 5.4.2 仿真监控结果
• 5.5 小结
• 第六章 结 束 语
• 6.1 全文工作总结
• 6.2 研究工作展望
• 致谢
• 参考文献
• 作者在学期间取得的学术成果
• 附录 A PEDL BNF 语法
• 附录 B MEDL BNF 语法