实时信息物理系统的实时性分析与验证

实时信息物理系统的实时性分析与验证

论文摘要

信息物理融合系统(Cyber Physical Systems,CPS)是一种新兴技术,它代表了下一代的核心信息技术,甚至被称为“第三次信息革命”,足见其受重视程度。CPS注重的是现实世界和虚拟计算之间高度集中的通讯技术研究,本质是对时间和空间的控制研究,所以又有“人-机-物”融合系统之称。CPS作为一种时间关键系统,时间是重要的考量因素,一次输入必须在有限的时间内产生有效的输出。一个完整的CPS需要的基础技术有三类:计算理论和技术,主要解决的是虚拟世界和现实空间的融合技术,减少或避免物理世界的不确定性因素在系统中产生的弊端;通信理论和技术,解决的是实现物理对象在网络中存在的表示规约,以及对测试网络通信协议的广域网测试平台;传感网技术,主要用来感知物理对象信息,并以无线传输方式传送到网络中。CPS在时间和空间上与物理世界紧密融合,再加上系统的高复杂性,这些都给CPS的发展带来了巨大挑战,大部分挑战都集中在时间的特性方面。例如计算系统和物理世界交互时,如何将时间分离出来,如何让物理世界中的连续时间离散化;还有当处理器芯片为了性能更好,技术变得更复杂时,会导致实时性行为不准确,同时最坏执行时间的估计也会愈发困难;还有如何保证虚拟和现实世界间依赖工作同步进行等等。利用自动机理论对系统的建模和分析可以在某种程度上分析和解决一些问题,而衡量时间特性建模方法的重要标准是其通用性和规范性,影响准确性和简单行的因素是模型表达能力的大小,为使系统能被正确的建模,并确保其可靠性,形式化方法的使用和描述是必不可少。本文在信息物理融合系统基础上进行的,介绍了概念,分析了时间语义特性,研究了在MARTE中对时间特性的简单建模,总结了时间逻辑的基础理论及其分类,利用混合自动机理论对CPS系统进行建模、分析和验证,随后探讨了在计算系统和物理系统交互时的时钟同步,利用模型检测理论,运用UPPAAL工具对最坏执行时间的分析。然后利用自动机的新变种验证了系统是具有可判定性的。最后,利用连续世界和离散世界的联系理论,通过把离散变量转化为连续变量表示,定义局部变量和全局变量的关系,运用微分方程表示连续变量和离散变量的连接机制,而且当改变初始值的时候,描述了微分方程的变化。实例部分给出了一个铁道路口的简单例子,运用连续变量离散化的理论,对实例系统的需求进行了形式化描述,并且给出了说明和验证。

论文目录

  • 摘要
  • Abstract
  • 目录
  • 第一章 绪论
  • 1.1 课题的背景及意义
  • 1.2 课题国内外相关研究工作
  • 1.3 课题研究主要内容及组织形式
  • 1.3.1 论文的主要内容
  • 1.3.2 论文的组织形式
  • 第二章 背景知识的介绍
  • 2.1 实时信息物理融合系统
  • 2.1.1 信息物理融合系统
  • 2.1.2 实时系统
  • 2.2 相关时间概念
  • 第三章 基于MARTE的时间建模
  • 3.1 MARTE中的时间模型
  • 3.2 MARTE中的分配模型
  • 3.3 精密计时的时钟实例
  • 3.4 小结
  • 第四章 时间逻辑
  • 4.1 经典时钟逻辑
  • 4.2 时钟逻辑基础实体
  • 4.3 区间时序逻辑
  • 4.3.1 命题区间时序逻辑
  • 4.3.2 一阶区间时序逻辑
  • 4.4 时间的通信序列语言(TCSP)
  • 4.4.1 TCSP中的语法
  • 4.4.2 TCSP中的语义和证明规则
  • 第五章 混合自动机
  • 5.1 建模混合系统
  • 5.1.1 混合轨迹
  • 5.1.2 混合自动机
  • 5.1.3 混合系统的实例
  • 5.2 验证过程
  • 5.2.1 验证方法
  • 5.2.2 实例验证
  • 第六章 时钟同步
  • 6.1 时钟内部同步
  • 6.2 时钟外部同步
  • 第七章 最坏执行时间分析
  • 7.1 任务交互
  • 7.1.1 天花板优先协议
  • 7.1.2 即时天花板优先协议ICPP
  • 7.2 最坏情况执行时间
  • 7.2.1 基于测量的方法
  • 7.2.2 静态方法
  • 7.3 静态分析
  • 7.3.1 控制流图CFG
  • 7.3.2 晶格理论
  • 7.3.3 抽象解释
  • 7.4 模型检测
  • 7.4.1 时间自动机
  • 7.4.2 树逻辑的定时计算(TCTL)
  • 7.4.3 TCTL模型检验
  • 7.4.4 UPPAAL中的模型检验
  • 7.5 时序异常
  • 7.5.1 形式化定义
  • 7.5.2 异常减少的方法
  • 7.6 利用UPPAAL进行WCET分析
  • 7.6.1 初始化UPPAAL模型
  • 7.6.2 分离程序和抽象硬件的模型
  • 7.6.3 生成程序模型
  • 第八章 基于自动机的调度分析
  • 8.1 相关的工作
  • 8.2 自动机基本概念
  • 8.2.1 任务模型
  • 8.2.2 外界自动机
  • 8.2.3 动作自动机
  • 8.3 编码调度
  • 8.3.1 任务建模
  • 8.3.2 动作自动机的可判定性
  • 第九章 离散世界和连续世界的联系
  • 9.1 时钟定义
  • 9.1.1 时钟定义
  • 9.1.2 时钟操作
  • 9.2 局部时钟和全局时钟
  • 9.2.1 局部时钟
  • 9.2.2 全局时钟
  • 9.3 离散变量和连续变量
  • 9.3.1 离散变量
  • 9.3.2 连续变量
  • 9.4 连结机制
  • 9.4.1 分配
  • 9.4.2 微分方程
  • 9.4.3 参数的修改
  • 第十章 铁道路口系统例子
  • 10.1 系统需求
  • 10.2 系统描述
  • 10.3 系统验证
  • 总结与展望
  • 参考文献
  • 攻读学位期间发表的论文
  • 致谢
  • 相关论文文献

    • [1].电网信息物理系统网络安全风险分析与防护对策[J]. 通信电源技术 2020(03)
    • [2].混合攻击下时变信息物理系统的有限时域H∞控制(英文)[J]. 控制理论与应用 2020(02)
    • [3].面向综合能源的信息物理系统体系架构及应用[J]. 电力建设 2020(04)
    • [4].电力信息物理系统建模与控制研究综述[J]. 上海电力大学学报 2020(02)
    • [5].考虑可观测性的电力信息物理系统级联故障分析方法[J]. 供用电 2020(04)
    • [6].信息化技术在物理教学中的应用——评《应用信息物理系统》[J]. 中国科技论文 2020(05)
    • [7].信息物理系统软件设计自动化专题前言[J]. 软件学报 2020(06)
    • [8].智能网联汽车信息物理系统参考架构1.0发布[J]. 智能网联汽车 2019(06)
    • [9].电网信息物理系统分析与控制的研究进展与展望[J]. 中国电机工程学报 2020(18)
    • [10].基于信息物理系统的智能焊接系统设计[J]. 机电信息 2020(30)
    • [11].信息物理系统安全威胁与解决措施[J]. 中国新通信 2018(23)
    • [12].信息物理系统在工业4.0中的应用探究[J]. 通讯世界 2019(01)
    • [13].信息物理系统威胁与攻击建模[J]. 自动化博览 2018(S2)
    • [14].信息物理系统——工业4.0时代智能制造的基础[J]. 智慧工厂 2019(01)
    • [15].煤矿信息物理系统场景感知自配置与优化策略研究[J]. 煤炭科学技术 2019(04)
    • [16].“信息物理系统理论、方法及应用”专栏序言[J]. 控制与决策 2019(11)
    • [17].数字孪生与信息物理系统——比较与联系[J]. Engineering 2019(04)
    • [18].信息物理系统安全威胁与防护措施[J]. 科技传播 2018(04)
    • [19].面向智慧城市的数据驱动信息物理系统安全威胁分析模型与方法[J]. 计算机系统应用 2018(07)
    • [20].《信息物理系统发展白皮书》专家研讨会在北京召开[J]. 电信工程技术与标准化 2017(02)
    • [21].《信息物理系统白皮书(2017)》解读(下)[J]. 信息技术与标准化 2017(05)
    • [22].基于社会信息物理系统的智慧制造资源组织模式[J]. 中国科技论坛 2017(07)
    • [23].征稿启事[J]. 电力工程技术 2017(04)
    • [24].“工业4.0”制造模式下面向云服务的信息物理系统参考架构研究[J]. 现代制造工程 2017(08)
    • [25].征稿启事[J]. 电力工程技术 2017(05)
    • [26].特约主编寄语[J]. 中国电机工程学报 2016(06)
    • [27].信息物理系统发展论坛成立[J]. 信息技术与标准化 2016(10)
    • [28].决胜未来,构建“工业4.0”的信息物理系统网络平台[J]. 上海企业 2014(12)
    • [29].信息物理系统和工业4.0[J]. 智能制造 2015(09)
    • [30].浅谈信息物理系统在现实应用中的安全性[J]. 高考 2018(06)

    标签:;  ;  ;  ;  

    实时信息物理系统的实时性分析与验证
    下载Doc文档

    猜你喜欢