基于时空π-演算的信息物理融合系统组件可替换性判定

王 鹏 向 阳 宗宇伟 张 骐

①(同济大学电子与信息工程学院 上海 201804)

②(上海计算机软件技术开发中心 上海 201112)

③(神华和利时信息技术有限公司 北京 100011)

1 引言

信息物理融合系统(Cyber Physical System,CPS)是近几年出现的一个新概念。CPS[1,2]是一种计算、通信与控制融合的新型复杂嵌入式系统，由计算单元、控制单元、执行器节点和传感器节点构成。系统中计算过程和物理过程在开放环境下持续交互、深度融合与相互作用，一体化地实现开放嵌入式计算、网络化实时通信与远程精确控制等先进功能。CPS已引起许多国家学术界和工业界的高度重视。美国总统科学与技术顾问委员会(PCAST)于2007年7月把CPS作为网络与信息技术领域的第一优先发展方向，由此引起美国多个政府机构、高校和企业数亿美元以及大量人力物力的投入。欧盟FP7的Artemis项目(2008-2017)计划投入27亿欧元开展嵌入式计算与CPS相关技术的研发。日本、韩国等也已在近年先后设立了针对 CPS的研究计划。我国也相当重视CPS的研究工作，国家高技术研究发展计划(863计划)课题“面向信息-物理融合的系统平台”已于2011年底正式启动。

当构成CPS的组件升级或者发生故障时，需要被新的组件替换，替换后的系统能否正常运行是一个非常值得研究的问题。要从理论上判定CPS组件的可替换性，CPS体系结构是首先要解决的问题。目前国内外在这方面的研究还处于起步阶段，文献[3]从CPS特征角度提出一种体系结构原型，但并未详细介绍如何实现。文献[4]提出一种多模式复合框架，但不适用于拥有多个并发处理单元的CPS。文献[5]提出一种面向服务的中间件模型，偏重于从中间件角度设计CPS的体系结构。本文提出一种面向服务的CPS体系结构，把CPS中的各种不同操作系统、中间件、编程语言的异构软硬件资源结合在一起封装成服务，将 CPS组件的可替换性等价为CPS服务的可替换性，便于进行统一的形式化分析与判定。针对CPS领域的形式化验证方法，已有众多研究成果[6]，包括基于Petri网[7]、有限状态机[8]、进程代数[9]等。Petri网和有限状态机所采用的图形方式较为直观，但当交互过程变得复杂时，这种图形刻画的方式容易出现状态空间爆炸，计算、验证和判定的复杂度也随即增加。进程代数中的π-演算专门用于描述移动进程和结构不断变化，可自行重配置的网络，采用π-演算是web服务可替换性判定的一种常见方法[10]。但是，与传统的web软件相比，CPS包含传感器、控制器等物理部件，受到时间和空间条件的约束，具有时空特性，而经典π-演算缺乏支持时空特性的语法和语义。本文对经典π-演算进行扩充，引入时间和空间算子，提出时空π-演算理论，对CPS服务进行形式化建模。从服务可替换性和兼容性的关系[11,12]入手，基于π-演算的弱互模拟理论，提出一种CPS服务可替换性判定方法，从而在设计阶段就能发现CPS组件的替换是否正确，避免后期付出更大的代价，减少不必要的开销。

本文第2节给出CPS服务的定义；第3节提出时空π-演算理论，进而对 CPS服务形式化建模，结合服务可替换性和兼容性的关系，给出CPS服务可替换性判定方法；第4节通过电子围栏案例，说明如何判定CPS组件的可替换性；最后是结束语。

2 CPS 服务

本节采用面向服务[13]的体系结构设计分布式、开放性的CPS，把复杂的CPS看作一系列封装好的CPS服务按照一定的业务逻辑和业务流程组合而成。该体系结构框架如图1所示，框架将CPS系统分为4层：应用层、业务流程层、服务抽象层和服务实现层。CPS服务包括服务实现和服务抽象两部分。因本文重点在CPS组件的可替换性研究，以下仅介绍 CPS服务，其余分层的详细构成可联系作者。

图1 面向服务的CPS体系结构框图

CPS服务实现包含感执单元、通信单元和计算与控制单元。CPS服务通过感执单元实时感知物理世界的变化，将感知信息通过通信单元传给计算单元，计算单元根据认知和规则做出决策并将结果交给控制单元，控制单元通过通信单元向感执单元发出指令，实现对物理世界的控制，整个过程是闭环的。各单元的具体描述如下：(1)感执单元包括传感器、执行器和终端计算模块。传感器用于获取物理实体和物理环境的信息；执行器用于实施对物理实体的具体操作；终端计算模块包含基本的执行器执行规则，并具备小容量的实时数据存储能力。(2)通信单元通过融合2G, 3G, 4G等各种异构网络提供泛在的互联通信机制。(3)计算单元能够实现离散域和连续域交叉运算，控制单元能够对时间和空间实施严格管理。

CPS服务抽象(也称接口)运用组件技术实现，描述了自身的接口特性、操作的可用性、参数、数据类型及访问协议。服务使用者可以确定该服务能做什么，如何查找，如何与该服务进行信息交换，如何调用该服务所提供的功能，可能返回的结果等。但是，CPS服务的实现细节是隐藏的，不同的服务提供者可以使用不同的技术和标准实现同一个服务接口。CPS服务提供了接口供外部调用，从而完成消息的接收和发送；同时，CPS服务根据一定的业务过程在消息收发动作的触发下，从起始状态经过一系列的迁移到达结束状态；此外，消息的收发动作需要耗费一定的时间和能量。由此给出CPS服务视图的定义。

3 基于时空π-演算的CPS服务可替换性判定方法

3.1 时空π-演算

在CPS中，时间的相对精确性足以满足系统服务质量的要求，因此可采用离散时间域对π-演算进行时间特性的扩充。定义离散时间域T，有如下性质：

(1)∀t∈T,t≠0⇒t＞0；

(2)∀t∈T,t≠∞⇒ ∞＞t；

(3)∀t,t′∈T,t＞t′ ⇔ ∃Δt＞0 且t′+Δt=t；

(4)∀t,t′∈T,(t＞0)∧(t′≠∞)⇒t′+t＞t′；

(5)∀t∈T,t+0=t,t+∞=∞；

(6)∀t1,t2∈T且t1＞t2， 则{t|t1≤t≤t2} 记 [t1,t2]为一个时间区间；

(7)∀t2,t3∈T,∀[t1,t4], ∃t′,t′∈T且t2≤t′≤t4，则t′∈[t1,t2]。

定义2时间约束算子Int(tr,Δt),tr为基准时刻，t≥0, Int(tr,Δt)P表示当且仅当t∈[tr,tr+Δt]时启动进程P。定义2表示进程在满足一定的时间区间的条件下才能启动。

支持 CPS物理部件正常工作的一切可观测的能量信息称为CPS的能量信息。能量信息包括很多种，如电能、热能等，可以消耗和补充。设进程P中包含n个物理部件，Ei表示其中第i个物理部件的能量信息，Eimax表示该物理部件所能达到的最大能量信息，则 ∃mi∈[0,100]，当且仅当Ei≥(Eimax·mi%)时，该物理部件方能正常工作。令M={m1,m2,…,mn}。

定义5时空π-演算的语法定义：

0是空进程；ax.P,a(x).P,τ.P是输出前缀、输入前缀和哑前缀表达式；P+Q是和表达式；P|Q是并行表达式；(x)P是限制表达式；[x=y]P是匹配表达式；!P是重复表达式。以上9个进程表达式的详细语法定义参见文献[16]，Int(tr, Δt)P, Pos[S]P,Ene[M]P参见定义2，定义3，定义4。

定义6时空π-演算的操作语义：

(1)时间约束算子(其中α∈{τ,a(x),ax}，下文中的α与此相同)：

(2)位置约束算子：

(3)能量约束算子：

PREFIX, SUM, PAR, COM, MATCH, RES,OPEN等语义规则参见文献[16]。

CPS服务与时空π-演算中的进程有较一致的对应关系。CPS服务的操作、接收(或发出)的消息、状态迁移与进程的通道、在通道上接收(或发送)的消息、迁移相对应；CPS服务基本的组合方式，如顺序、选择、并行、迭代结构等，可用时空π-演算中的进程、和式、并行和重复表达式表示。时空π-演算只对经典π-演算扩展了描述时空特性的能力，并没有对经典π-演算的基本性质进行更改，所以它继承了经典π-演算的弱模拟特性。

定义7弱模拟/弱互模拟关系：设R是进程空间K的上二元关系，∀二元组PRQ，若下列条件成立，则称Q弱模拟P：

(1)若P→P'，那么存在Q'∈K满足Q⇒Q'且P'RQ'成立；

(2)若PP'，那么存在Q'∈K满足QQ'且P'RQ'成立。

若R和R的逆都是弱模拟的，则称P和Q是弱互模拟的，记做P≈Q。弱互模拟的性质参见文献[16]。弱互模拟主要用于描述具有不同内部结构和内部行为，但从外部看起来是等价的情况。本文主要采用π-演算的弱互模拟理论。

3.2 CPS 服务可替换性判定方法

服务可替换性依赖于服务的兼容性[11]。将若干CPS服务组合在一起完成复杂的任务，需要保证这些服务之间能够协同工作，称为CPS服务能够相互兼容。兼容性分为静态兼容和动态兼容。静态兼容是指CPS服务之间在语义和语法形式上是兼容的。将CPS服务发送或接收信息的动作称为CPS服务的行为。动态兼容是指CPS服务之间的行为是兼容的，即相互传递的消息序列是匹配的，不存在死锁和活锁的情况，也不会发送对方不能接收的消息。

定义8CPS服务相兼容：CPS服务A和B是静态兼容的，A发送请求的集合是B响应集合的子集，即A部分或全部使用B接收信息的接口，若此时A和B仍能正常交互，则称A和B相兼容。

定义9CPS服务对偶服务：CPS服务S的对偶服务，指将S发送(和接收)消息的行为替换为接收(和发送)消息。

结合国内外研究成果[11,12]，本文提出CPS服务可替换的充分条件：如果存在一个CPS服务S'同任何与CPS服务S相兼容的服务相兼容，同时S发送和接收消息的集合是S'的子集，且S'能够满足系统的时空约束条件，那么S'可以替换S。

设 CPS服务S'的服务视图为CPSVS′,S'与系统有n次交互，Tr={tr1,tr2,…,trn}表示每次交互的基准时刻，ΔT={Δt1, Δt2,…, Δtn}表示每次交互的时间延迟约束条件。用进程PS′表示S',PM表示M中每个服务的对偶服务集合，QF表示S'所能达到的所有结束状态的集合，α表示状态迁移包含的内部和外部动作。用emi(S)表示S发送消息的名称的集合，rec(S)表示S接受消息的名称的集合。

定理 1CPS服务可替换性判定定理已知一个 CPS服务S，系统中与之相兼容的服务集M={S1,S2,S3,…,Sn}，当满足以下条件时，S'可以替换S。

(2)S'与M是静态兼容的；

(4)emi(S)⊆emi(S'), rec(S)⊆r ec(S')。

证明若条件(1)成立，根据定义2,3,4，可知S'满足系统的时空约束条件；若条件(2)，条件(3)成立，根据定义7，定义8和弱互模拟的性质，可知S'与M相兼容；又因条件(4)成立，可知CPS服务可替换的充分条件满足，因此S'可以替换S。 证毕

在定理1实际应用时，条件(1)，条件(3)的判定，可利用时空π-演算对CPS服务进行形式化建模，结合系统的时空约束条件，对合成服务的进程表达式进行形式化推演，判断是否可以迁移到结束状态。

4 应用案例

本节通过上海交通运输集团危险化学品车辆运控 CPS1)该系统由本文作者所在的项目组设计开发，现已交付使用。上海交通运输集团是上海市交管局确认的可从事1-9类危险化学品的两家运输企业之一，拥有240辆危险化学品运输车辆。电子围栏案例，说明如何运用定理 1判定CPS组件的可替换性，以保障升级后的系统仍能正常运行。

4.1 问题描述

业务场景描述如下：当运送危险化学品的槽罐车发生交通事故后，若车载传感器监控到车辆运行状态异常，向呼叫中心报警。中心接警后，利用车载摄像头和温湿度、液位、压力、气体等多个传感器远程监测罐体温度、气体泄漏浓度、罐体压力、罐体液位、仓门开关、位置移动等各种参数，进行远程实时诊断，判断事故是否达到设置电子围栏的级别。若需设置，则运用北斗高精度定位技术，根据车辆位置设置围栏区域，并周期性的发送给其他危险化学品车辆。对于围栏内的车辆，通过车载终端预警；对于围栏外的车辆，通过车载终端告知。

采用本文第2节的模型进行业务建模，该流程由车辆报警，远程诊断，电子围栏设置，事故预警，事故告知5个CPS服务合成，如图2所示，每个CPS服务发送和接收的消息均在图2中表示。因用户需求变动，进行系统升级，添加一个交通事故处理平台(交警系统)代理。在车辆远程诊断后，需将交通事故信息上报给该代理；在电子围栏设置完成后，需将电子围栏信息上报给该代理。如图3所示，升级后，增加一个CPS服务：交通事故处理平台(交警)代理，“远程诊断”和“电子围栏设置”2个CPS服务都有变化，其余3个不变。

本节要解决的问题描述为：原有系统中的S是否可以被新系统中的S'替换掉(S和S'如图所示)。为使替换具有普遍性，“电子围栏设置”保持不变，只考虑S的替换，即“电子围栏设置”不会升级到如图3所示，不能发送电子围栏消息给交通事故处理平台代理。若全面升级，升级部分与其他CPS服务的消息接口并无变化，这种替换较理想化，不具备普遍性。

4.2 问题建模

图2中的CPS服务用进程Pva,Prd,Pef,Pew,Pat表示，通道名和消息名如图2中表示。位置约束条件方面，设基准区域为电子围栏区域，“事故预警”在基准区域内，即Sew={{sin},{sin},…,{sin}}；“事故告知”在电子围栏区域外，即Sat={{sd},{sd},…, {sd}}；其余3个CPS服务无位置约束，即Sva=Srd=Sef={Spos,Spos, …,Spos}。能量约束条件方面，表示为Mva,Mrd,Mef,Mew,Mat。时间约束条件将在服务建模时详述。详细建模过程如下：

(1)车辆报警：事故发生后t0+1(以下时间单位均为s)内发出报警信息，信息提交后t1+60内须得到回应。

(2)远程诊断：收到报警信息后t2+30内做出诊断并回应。若确认达到相应事故级别，回应后t3+1内提交电子围栏设置申请，提交后t4+60内须得到确认。

图2 原有的电子围栏业务流程图

图3 升级后的电子围栏业务流程图

(3)电子围栏设置：收到电子围栏设置申请后t5+30内完成设置并确认。设置成功后，周期性的在 [t6,t6+3 0](t6=t6+3 0是不断递增的)内向不同区域的车辆(本文仅以围栏内车辆A和围栏外车辆B为例，其他车辆与之类似)发送电子围栏信息。信息发出后，以车辆A为例，须在tAe+3 0(tAe是每次发出电子围栏消息的时刻)内收到A的确认信息。

(4)事故预警和事故告知：不与S直接交互，可看作内部服务，对替换没有影响，因此Pew和Pat的建模过程略。

(1)远程诊断：确认达到事故级别后t3+1内，将事故信息发送给交通事故处理平台代理，其他流程不变。

(2)电子围栏设置：确认电子围栏设置完成后t6+1内，将电子围栏设置信息发送给交通事故处理平台代理，其他流程不变。

(3)交通事故处理平台(交警)代理：

根据以上分析结果，可知

4.3 可替换性判定

判断S'是否可以替换掉S，只要判断S'是否满足定理1中的4个条件即可。

(1)对于条件(1)，将实际系统的相应软硬件特征参数带入PS′中，进行形式化推演，判定S'是否能迁移至结束状态。若可以，则S'满足条件(1)。

(2)对于条件(2)，设与S相兼容的服务集为M={车辆报警，电子围栏设置}，由图3很容易看出，S'与“车辆报警”和“电子围栏设置”都是静态兼容的，条件(2)满足。

(3)对于条件(3)，假定S'已满足条件(1)，则有

(4)对于条件(4)，由图2，图3可知：

显然有emi(S)⊆emi(S'), rec(S)⊆r ec(S')，条件(4)满足。

综上，只要S'满足条件(1)，S'完全可以在原有系统中直接替换S。

在实际系统中，经多轮测试和90天的试运行，替换后的电子围栏模块运行正常，充分验证了以上分析结果。本案例说明，本文提出的CPS可替换性判定方法能够辅助用户在动态开放、复杂异构的CPS中正确完成组件替换，从而保证了升级后系统正常、可靠的运行。

5 结束语

本文围绕CPS组件可替换性问题展开研究，将其等价为CPS服务的可替换性判定问题，提出一种基于时空π-演算理论的 CPS服务可替换性判定定理；该定理在电子围栏案例中的实际应用，验证了其合理性和可行性。本文提出的模型和方法具有一定的创新性和实用性。

未来的研究工作包括两个方面：(1)进一步研究和细化 CPS服务中的动作时间函数和动作能量函数，构造CPS服务的时间和能量成本状态空间，进而能够在成本状态空间中寻找最优的服务合成方案，为服务替换的最优化选择提供参考依据；(2)对于与原有系统不兼容的CPS服务，研究通过增加适配进程的方法实现服务可替换，从而增加可替换服务的选样空间和实施方式。

[1]Lee E A. CPS foundations[C]. Proceedings of the 47th Design Automation Conference, New York, USA, 2010: 737-742.

[2]Marwedel P. Embedded System Design: Embedded Systems Foundations of Cyber-Physical Systems[M]. 2nd Edition,Dordrecht Heidelberg, London, New York, Springer, 2011:4-9.

[3]Rajkumar R R, Lee I, Sha L,et al.. Cyber-physical systems:the next computing revolution[C]. Proceedings of the 47th Design Automation Conference, New York, USA, 2010:731-736.

[4]Phan L T X and Lee I. Towards a compositional multi-modal framework for adaptive cyber-physical systems[C].Proceedings of the 17th International Conference on Embedded and Real-Time Computing Systems and Applications, Toyama, 2011: 67-73.

[5]Hoang D D, Paik H Y, and Kim C K. Service-oriented middleware architectures for cyber-physical systems[J].International Journal of Computer Science and Network Security, 2012, 12(1): 79-87.

[6]Derler P, Lee E A, and Vincentelli A S. Modeling cyberphysical systems[J].Proceedings of the IEEE, 2012, 100(1):13-28.

[7]Thacker R A, Jones K R, Myers C J,et al.. Automatic abstraction for verification of cyber-physical systems[C].Proceedings of the 1st ACM/IEEE International Conference on Cyber-Physical Systems, New York, USA, 2010: 12-21.

[8]Lee E A and Tripakis S. Modal models in ptolemy[C].Proceedings of the 3rd International Workshop Equation-Based Object-Oriented Model, Lang, Tools, Oslo, Norway,2010: 11-21.

[9]Akella R and McMillin B M. Model-checking BNDC properties in cyber-physical systems[C]. Computer Software and Applications Conference, Seattle, WA, 2009: 660-663.

[10]Kuang L, Xia Y, Deng S G,et al.. Analyzing behavioral substitution of web services based onπ-calculus[C].Proceedings of International Conference on Web Services,Miami, FL, 2010: 441-448.

[11]Bordeaux L, Salaün G, Berardi D,et al.. When are two web services compatible?[C]. Proceedings of the 5th International Workshop on Technologies for E-Services, Toronto, Canada,2005: 15-28.

[12]Brogi A, Canal C, Pimentel E,et al.. Formalizing web services choreographies[J].Electronic Notes in Theoretical Computer Science, 2004, 105: 73-94.

[13]Erl T. Service-Oriented Architecture: Concepts, Technology,and Design[M]. Upper Saddle River, NJ, USA, Prentice Hall PTR, 2005: 21-46.

[14]OPEN GIS CONSORTIUM. OpenGIS geography markup language(GML)encoding standard[S]. Version 3.3, www.opengeospatial.org/standards/gml/, 2007.

[15]Egenhofer M J and Herring J R. A mathematical framework for the definition of topological relationships[C]. Proceedings of the 4th International Symposium on Spatial Data Handling, Zurich, 1990: 803-813.

[16]Milner R. Communicating and Mobile Systems: Theπ-calculus[M]. Cambridge, UK, Cambridge University Press,1999: 12-35.