论文部分内容阅读
信息-物理融合系统(Cyber-Physical Systems,CPS)的概念于2006年由美国国家科学基金会提出。CPS是异构子系统通过网络融合的大型、异构、分布式实时反馈系统,与传统的嵌入式系统相比,CPS强调信息世界与物理世界的有机融合,通过计算单元及物理对象在网络环境下的高度集成和实时交互来提高系统在信息处理、实时通信、精准控制等方面的能力。CPS广泛应用于工控、国防、交通等与国计民生密切相关的安全攸关领域,对相关系统进行有效的分析,从而保障系统安全运营至关重要。常规的系统安全性分析技术,如测试、仿真等无法穷尽地遍历复杂系统所有可能的运行输入和场景,也就不足以保证检测的完备性,这会给系统留下安全隐患。区别于测试等方法,形式化方法通过求解系统模型状态取值范围等方法来确认系统模型中一定不会出现相关错误。因此,形式化方法对于保障安全攸关系统的安全运营具有重要意义。着色时间Petri网适合于对异构、分布式、并行以及实时系统建模,然而着色时间Petri网无法有效描述CPS物理实体与环境之间的事件交互。本文对着色时间Petri网进行扩展,围绕CPS形式化建模与分析展开研究:(1)针对CPS强调信息世界与物理世界的紧密交互并对系统实时性具有严格要求的特点,在引入CPS时空事件的基础上,从事件交互和实时性的角度给出了CPS物理实体的定义;然后对着色时间Petri网进行语法及语义扩展,提出适合描述CPS物理实体与环境之间交互的OCTPN(Open Colored Time Petri Net)的定义,并给出CPS物理实体空间属性建模方法及CPS物理实体与所对应OCTPN模型的关系。(2)针对OCTPN模型分析过程中面临的状态空间爆炸问题,提出OCTPN状态类及状态类图计算方法进行OCTPN模型的状态空间计算,使用有穷的OCTPN状态类空间表示OCTPN模型无穷的状态空间。为了应用时间自动机成熟的模型检测工具,提出OCTPN模型到相应OCTPN状态类时间自动机模型的转换算法,并进一步证明OCTPN状态类时间自动机模型与初始OCTPN模型是互模拟的。最后,使用模型检测工具UPPAAL对系统的行为属性及时间属性进行验证。