基于可能性时空混成自动机的CPS软件建模.docxVIP

基于可能性时空混成自动机的CPS软件建模 　　摘 要： 信息物理融合系统对复杂系统的建模与验证是当前控制研究领域的一个热点问题。考虑不确定环境因素对CPS系统的影响，结合可能性测度与时空模型，给出一种可能性时空混成自动机的信息物理融合系统的建模方法。以时空混成自动机为建模工具，通过分析CPS的体系结构，讨论衡量不确定性的可能性对CPS软件运行时的时空动态影响，给出一个可能性时空CPS系统架构。通过理论证明和实例分析在不确定环境下可能性时空混成自动机为CPS软件系统建模的可行性。　　关键词： CPS； 不确定性； 可能性时空混成自动机； 控制系统； 建模； 属性验证　　中图分类号： TN876?34； TP391 文献标识码： A 文章编号： 1004?373X05?0173?05　　Abstract： The complex system modeling and validation by means of the cyber?physical system is a hotspot issue of the current control study field. Considering the influence of the uncertain environment on CPS， the possibility measurement and spatio?temporal model are combined to give a modeling method of CPS based on possibility spatio?temporal hybrid automata. Taking the spatio?temporal hybrid automata as the modeling tool， analyzing the architecture of the CPS， and discussing the influence of nondeterminacy′s possibility on the spatio?temporal dynamic behavior when the CPS software is running， an architecture of the possibility spatio?temporal CPS is given. The theory verification and instance analysis results show that the CPS software modeling based on possibility spatio?temporal hybrid automata is feasible in uncertain environment.　　Keywords： cyber?physical system； indeterminacy； possibility spatio?temporal hybrid automata； control system； modeling； property verification　　0 引 言　　信息物理融合系统是一种融合计算进程与物理进程的复杂嵌入式网络系统[1]，并且已经在很多领域广泛应用。实现的反馈控制既安全又可靠，还可以有效实现人与现实世界的交互。该领域研究的一个热点问题是CPS系统的建模及其验证。CPS体系中各组件具备自治性、异构性、并发性等特性，相对于传统的嵌入式系统，CPS软件与硬件高度融合，各组件并非完全孤立，而是彼此关联的一个整体，拥有离散与连续动态变化的行为，使得利用传统方式对CPS软件建模具有挑战性。混成自动机既能描述真实世界的变化状况，又能刻画系统的状态转移关系，因此该模型成为研究CPS系统的重要基础[2?5]。更多地，文献[6]提出一种异构模型，引入行为关系以表达系统之间不同的模型语义，实现对系统属性的形式化验证；文献[7]提出具有位置驱动特点的时空自动机；文献[8]根据混成自动机与HP模型之间的转换规则提出一种CPS软件模型与属性验证框架。这些都是经典的一些CPS软件模型与属性验证框架。　　在实际系统中，由于CPS所处的环境具有不确定性，而这些不确定性对CPS是否能正确运行在一定程度上起着至关重要的作用。通常经典的模型和检测方法不能处理实际系统中的这些不确定的建模与属性验证问题。可能性测度是模糊集理论的一个分支，是对概率测度的推广，可能性测度不满足可加性。文献[9?11]将可能性测度模糊数学与模型检测技术相结合，提出基于可能性测度的模型检测方法。为复杂系统的不确定性验证提供了较好的理论基础。　　本文考虑不确定环境对CPS系统的影响，提出