信息物理融合系统的形式化建模与讨论

发布时间：2024-03-17 09:43

　　信息物理融合系统(Cyber-Physical System, CPS)基于计算机互联网,在物与物互联的基础上,将计算(computation)、通信(communication)、控制(control)3C技术融合在一起,强调对物实时、动态的信息控制与信息服务,是国内外信息技术领域研究的一类重要系统。如何对CPS系统进行建模,以及验证模型中的性质以确保CPS系统的保真性、可靠性等特点是一个重要的研究问题。 本文主要采用微分动态逻辑(Differential Dynamic Logic, dL)、结构分析与设计语言(Architecture Analysis and Design Language, AADL)和时钟理论(Clock Theory)分别对不同的CPS应用场景进行建模分析并验证了其安全性性质。 利用微分动态逻辑对CPS系统铁路道口控制进行形式化建模与分析。从火车发送接近信号到进入道口的运动过程中,针对火车到达道口的时间要求,将火车速度控制问题抽象成一个混成系统的安全性性质,用微分动态逻辑来描述,并使用混成系统证明工具KeYmaera对系统的安全性进行了验证,实现对火车进入...

【文章页数】：66 页

【学位级别】：硕士

【文章目录】：
摘要
Abstract
第一章 绪论
    1.1 研究背景
        1.1.1 物联网和信息物理融合系统
        1.1.2 混成系统
            1.1.2.1 混成系统定义
            1.1.2.2 混成系统案例
    1.2 国内外研究现状
    1.3 研究内容和方法
    1.4 文章结构
    1.5 本章小结
第二章 微分动态逻辑对CPS的建模
    2.1 概述
    2.2 混成程序
        2.2.1 混成程序介绍
        2.2.2 混成程序的语法语义
    2.3 dL模型在形式化验证中的优势
    2.4 微分动态逻辑的推理演算法则
    2.5 铁路道口控制系统分析与建模
        2.5.1 铁路道口控制系统分析
        2.5.2 铁路道口控制系统建模
    2.6 本章小结
第三章 结构分析与设计语言对CPS的建模
    3.1 结构设计与分析语言介绍
        3.1.1 AADL概念
        3.1.2 AADL组件
    3.2 温度无线传感器网络模型
        3.2.1 温度无线传感器网络
        3.2.2 模型的建立
    3.3 本章小结
第四章 时钟理论对CPS的建模
    4.1 时钟理论的基本概念
    4.2 时钟理论的建模
        4.2.1 温度控制系统的时钟理论建模
        4.2.2 铁路道口控制的时钟理论建模
    4.3 本章小结
第五章 建模与验证的工具
    5.1 基于微分动态逻辑模型的工具KeYmaera
    5.2 基于KeYmaera的性质验证
    5.3 AADL建模工具
    5.4 本章小结
第六章 总结与展望
    6.1 总结
    6.2 展望
附录A
    A.1 火车道口控制系统安全性验证的KeYmaera程序
    A.2 AADL文本形式建模代码
参考文献
攻读硕士学位期间发表论文和参与科研项目情况
致谢



本文编号：3930836