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

彭姣+耿生玲+童英华+宫海彦

摘 要： 信息物理融合系统（CPS）对复杂系统的建模与验证是当前控制研究领域的一个热点问题。考虑不确定环境因素对CPS系统的影响，结合可能性测度与时空模型，给出一种可能性时空混成自动机的信息物理融合系统的建模方法。以时空混成自动机为建模工具，通过分析CPS的体系结构，讨论衡量不确定性的可能性对CPS软件运行时的时空动态影响，给出一个可能性时空CPS系统架构。通过理论证明和实例分析在不确定环境下可能性时空混成自动机为CPS软件系统建模的可行性。

关键词： CPS； 不确定性； 可能性时空混成自动机； 控制系统； 建模； 属性验证

中图分类号： TN876?34； TP391 文献标识码： A 文章编号： 1004?373X（2018）05?0173?05

Abstract： The complex system modeling and validation by means of the cyber?physical system （CPS） 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 引 言

信息物理融合系统（Cyber?Physical Systems，CPS）是一种融合计算进程与物理进程的复杂嵌入式网络系统[1]，并且已经在很多领域广泛应用。实现的反馈控制既安全又可靠，还可以有效实现人与现实世界的交互。该领域研究的一个热点问题是CPS系统的建模及其验证。CPS体系中各组件具备自治性、异构性、并发性等特性，相对于传统的嵌入式系统，CPS软件与硬件高度融合，各组件并非完全孤立，而是彼此关联的一个整体，拥有离散与连续动态变化的行为，使得利用传统方式对CPS软件建模具有挑战性。混成自动机既能描述真实世界的变化状况，又能刻画系统的状态转移关系，因此该模型成为研究CPS系统的重要基础[2?5]。更多地，文献[6]提出一种异构模型，引入行为关系以表达系统之间不同的模型语义，实现对系统属性的形式化验证；文献[7]提出具有位置驱动特点的时空自动机；文献[8]根据混成自动机与HP模型之间的转换规则提出一种CPS软件模型与属性验证框架。这些都是经典的一些CPS软件模型与属性验证框架。

在实际系统中，由于CPS所处的环境具有不确定性，而这些不确定性对CPS是否能正确运行在一定程度上起着至关重要的作用。通常经典的模型和检测方法不能处理实际系统中的这些不确定的建模与属性验证问题。可能性测度是模糊集理论的一个分支，是对概率测度的推广，可能性测度不满足可加性。文献[9?11]将可能性测度模糊数学与模型检测技术相结合，提出基于可能性测度的模型检测方法。为复杂系统的不确定性验证提供了较好的理论基础。

本文考虑不确定环境对CPS系统的影响，提出一种基于可能性时空混成自动机模型，给出CPS系统建模和可能性时空CPS的描述语言。从理论和实例两方面验证基于该模型为不确定环境下CPS系统建模和属性验证度量方法的有效性，从而为复杂CPS系统的智能控制与优化提供理论依据。

1 基本概念

定义1[12]：设是一个非空集合，是由的子集构成的集合（包含空集），且对集合的补运算和可数任意并运算封闭，则称是一个代数，为可测空间。映射表示代数上的可能性测度，且满足以下性质：

定义2[13]：混成自动机为六元组：

其中：Loc为控制模式的集合；为边的有限集合，即表示转换关系。对于其中为源位置，为目标位置，为保卫条件，为同步标签，为变量的更新关系；为实值变量的有限集，即称为自动机的维度；Lab为同步标签的集合，同步标签也叫做事件；Act为活动标记函数，以此来表示混成自动机每个位置标识的一系列活动，通常用变量对时间的微分方程表示；Inv为不变式标记函数，赋予每个位置一个不变式。endprint

CPS具有离散与连续动态变化的行为，它既能描述真实世界的变化状况，又能刻画系统的状态转移关系。所以，混成自动机成为研究CPS系统至关重要的基础。

2 可能性时空混成自动机

在实际系统中，由于环境的不确定性对CPS正确运行在一定程度上产生一定影响。因此，在研究混成自动机的基础上，本文引入可能性测度和时空逻辑，给出具有描述位置或者空间行为信息的不确定性CPS软件的建模。

定义3：可能性时空混成自动机用八元组表示，其中：

1）是一个离散状态集或者控制模式集；

2）是可能性时空混成自动机的连续状态空间，通常情况下，是一个?维分支；

3）是标签有限集，用来标记状态转换的边的标签集合；

4）是变量的集合，这些变量存在于每个模式中，并由所在的模式惟一决定。这个变量包含离散变量的集合dVar、 连续变量的集合cVar、 时钟变量的集合ckVar和空间变量集合sVar；

5）是控制图中边的集合，称为迁移。每个边可以定义为四元组： ，其中： ，是可能性转移函数； ，是警卫条件，它可以描述从跳转的条件；是迁移发生时将要发生的动作。对于，，都有；

6） Inv是模式中必须满足的条件，称为不变式。具体来说，就是每个模式对应的一个子集；

7） Act表示模式的标记函数，它表达为一些微分方程的合取式。每个模式都对应一个模式活动Act，它描述在模式中连续变量随时间变化的情况；

8） 是可能性初始分布函数，对于，都有。

在以上可能性时空混成自动机的定义中，对于 当满足条件，一个从的迁移就会发生，同时，离散变量跳转到一个新值记为对于有：

表明一个迁移有效，当且仅当满足如下条件：

下面为列车控制系统的一个制动行为可能性时空混成自动机模型实例，如圖1所示。

用表示第一辆车的安全距离，表示第一辆车的紧急制动距离，表示第二辆车的安全距离，表示第二辆车的紧急制动距离，根据关系知，表示相离，表示相交。其模型为其中：

{Initinal，BarkingNoRequired，Barkingrequird，Initinal1，EmergeBarkingRequired，NormalBarkingRequired，Initinal2，Wating，Barking}；

在可能性时空混成自动机模型的迁移系统中，为了简便，系统的时空状态表示为，其中为标签，表示当前的状态， 表示其控制模式，表示在状态停留的时间，表示在状态时的位置，表示对应位置的速度。

3 可能性时空CPS软件模型

基于可能性时空混成自动机的CPS结构称为可能性时空CPS模型，其体系结构可由三层组成，即设备服务层、服务接口层和高级应用层，如图2所示。服务接口层的功能体现系统与环境之间相互影响，CPS软件涉及离散过程和连续过程的交互，通过已定义的明确端口与外界进行通信等。

1） 设备类：DC=，其中Id为设备类别的惟一标识符；Att为设备类的相关属性的有限集合； Dom：Att→DataType表示设备属性到数据类型的一个映射，DataType表示传送数据的类型，如integer，boolean，float和用户自定义的数据类型。

2） 设备实体：DE=，其中DId是设备实体的惟一标识符；DC是设备实体所属的设备类； DH是描述设备实体动态行为的可能性时空混成自动机。

3） 原子服务，其中sId是CPS软件服务的惟一标识符；dSet为设备实体类的集合；SH是描述服务动态行为的可能性时空混成自动机。

可能性时空CPS模型的迁移系统中，无穷路径表示为：有穷路径表示为：。用Paths表示中无穷路径的集合，Pathsfin表示有穷路径的集合。

中状态的前驱Pre表示为：

后继Post表示为：

而对于如果定义可得扩张映射， 则称映射Po是上的时空可能性测度。其中，表示状态的前驱状态。

定理1：设为可能性时空CPS模型，则称为上由生成的代数。

定理2：设是可能性时空CPS模型，则从初始状态出发的路径的可能性为：

4 实例分析

以ETCS两辆列车智能控制CPS系统的应用场景为例，考虑环境的不确定性对列车运行时速度和距离的影响。如图3所示，两辆列车在列车自我防护（ATP）子系统监控下行驶，从而避免列车超速，防止列车碰撞。运用可能性时空混成自动机建模方法对ATP子系统进行分析建模。

1） 执行层建模

创建ATP类、制动类和ATP服务、制动服务。

ATP类，其中，sensor是传感器，Cmd是命令端口。

ATP服务：ATPService=（ATPService，{ATP}，AtpHA），AtpHA是描述监测距离服务或者速度监测服务的可能性时空混成自动机，如图4a），图4b）所示。

2） 感知层建模

速度感知服务：SpeedService=（speedService，{Trains}，SH），SH是描述列车速度动态变化的可能性时空混成自动机，如图4c）所示。

距离感知服务：DistService=（distService，{Trains}，SSH），SSH是描述列车距离动态变化的可能性时空混成自动机，如图4d）所示。

3） 控制层建模

ATP控制服务：ContrService=（contrService，{ATP，Train，Speed}，Cmd，TCSH），TCSH是描述ATP控制行为的可能性时空混成自动机，如图4e）所示。

5 结 语

基于CPS软件的不确定性，结合可能混成自动机模型给出软件定义CPS形式的时空建模工具和形式化描述语言，描述CPS的体系结构模型及动态行为，利用列车控制系统模型阐明该方法的有效性。下一步将继续对可能性CPS软件属性进行动态验证分析和不确定性时空模型下的智能控制方法进行研究，并将其应用于机器人工业、汽车电子、智能电网、智能家居、医疗卫生等应用领域，为复杂CPS系统的智能控制与优化提供更多理论依据。

参考文献

[1] LEE E A. Cyber physical system： designer challenges [C]// Proceeding of the 11th IEEE International Symposium on Object Oriented Computing. Orlando： IEEE， 2008： 363?369.

[2] THOMAS A H. The theory of hybrid automata [C]// Proceedings of 1996 LICS. [S.l.： s.n.]， 1996： 278?292.

[3] RAJEEV A， COSTAS C， THOMAS A H， et al. Hybrid automata： an algorithmic approach to the specification and verification of hybrid system [J]. Hybrid systems， 1993， 736： 209?229.

[4] THOMAS A H， PETER W K， PURI A， et al. What′s deci?dable about hybrid automata [J]. Journal of computer and system sciences， 1998， 57（1）： 373?382.

[5] FENG Y， YANG Xia， SHEN Zhaoxiang， et al. Modeling computation entity of CPS based on dynamic behavior [J]. Journal of system simulation， 2016， 28（5）： 1003?1016.

[6] AKSHAY R， BRUCE H K. Heterogeneous verification of cyber?physical system using behavior relation [C]// Proceedings of the 15th ACM International Conference on Hybrid System： Computation and Control. [S.l.： s.n.]， 2012： 35?44.

[7] ZHAO Wenming， CHEN Yixiang， ZHANG Min. Modeling and verification of CPS based on spatial hybrid automata [J]. Bulletin of science and technology， 2015， 31（1）： 94?99.

[8] TIAN Mingfu， ZHANG Xingshe， LIN Jialin， et al. Behavior modeling and attribute validation of cyber?physical system （CPS） based on hybrid automata [J]. Journal of Air Force Engineering University （natural science edition）， 2016， 17（3）： 40?44.

[9] LI Lijun， LI Yongming. Model?checking of linear?time properties in possibilistic Kripke structure [C]// Proceedings of the 2012 QL&SC. [S.l.]： World Scientific， 2012： 2870?2894.

[10] 李永明.可能LTL模型检测的两种方法[J].陕西师范大学学报（自然科学版），2014，42 （6）：21?25.

LI Yongming. Two methods for possibilistic linear temporal logic model checking [J]. Journal of Shaanxi Normal University （natural science edition）， 2014， 42（6）： 21?25.

[11] LI Yongming， LI Lijun. Model checking of linear?time properties based on possibility measure [J]. IEEE transactions on fuzzy systems， 2013， 21（5）： 842?854.

[12] 李丽君.基于可能性测度的LTL模型检测[D].西安：陕西师范大学，2012.

LI Lijun. LTL modeling checking based on possibility measure [D]. Xian： Shaanxi Normal University， 2012.

[13] 张建宁.基于混成自动机的CPS构建服务组合建模与验证[D].苏州：苏州大学，2014.

ZHANG Jianning. Modeling verifying of CPS component service composition based on hybrid automata [D]. Suzhou： Soochow University， 2014.endprint