物联网服务的π-演算建模与验证

李文翔

(福建商学院 信息工程学院，福建 福州 350012)

物联网服务建模是物联网研究领域的一个分支，相比较于传统的服务，物联网服务具有实时性、资源约束性、位置相关性等性质。在物联网服务建模研究中，国内外学者做了大量的相关研究：李戈等[1]和李力行等[2]采用时间自动机理论建模物联网服务以及物理环境，并将用户期望的服务特性描述为时序逻辑公式，从而验证物联网服务运行于特定环境下能够满足期望的性质；针对基于自动机、Petri网等模型的状态空间爆炸问题，叶林等[3]提出使用微分动态逻辑和定量微分动态逻辑对物联网服务建模与验证；韩乔等[4]针对语义物联网服务的正确性验证问题，提出基于时态描述逻辑ALC-μ的语义物联网服务验证方法；马莉等[5]提出一种面向资源的物联网系统形式化建模与验证方法，使用通信顺序进程CSP对物联网系统的动态行为进行建模，利用线性时序逻辑LTL刻画待验证的性质；Yen等[6-7]扩展了现有OWL-S表达功能，将其用于对物联网服务的描述，并以此为基础讨论了物联网服务的组合问题；De等[8]基于本体语言分别对实体、资源和物联网服务进行语义建模；Sivrikaya等[9]针对智慧城市的具体应用，提出了一个服务识别和组合的分布式框架ISCO(intelligent framework for service discovery and composition)，在基于语义网的物联网服务和物理设备统一模型的基础上，使用OWL-S描述服务；为高效地获取物联网的各项资源(物理设备、物联网服务等)，Gomes等[10]提出了一个基于语义的资源识别服务QoDisco，该服务主要用于识别基于本体论进行语义描述的物联网各项资源。这些学者分别从不同的角度阐述物联网服务形式化建模与验证的机制，为本文提供了参考。

为此，本文以描述物联网服务间的动态交互问题为出发点，提出基于环境的物联网服务π-演算[11]建模方法以及使用μ-演算[12]描述物联网服务所具备的性质。针对特定实例场景，使用π-演算定义物联网服务和环境实体，利用μ-演算对物联网服务能力进行描述，最后使用模型检测工具MWB(mobile workbench)进行验证。

1 基于π-演算的物联网服务建模

文献[1]提出的基于环境的物联网服务建模框架，将建模过程分成环境实体建模和物联网服务建模两个部分。依据π-演算的特点，结合基于环境的物联网服务建模框架[1]，可以使用π-演算语法从动态行为角度描述环境实体和物联网服务。

1.1 环境实体建模

环境实体是指物联网系统运行环境下的一组实体，例如光照、温度、空调等，其可分为被感知型环境实体和受控型环境实体。

1) 被感知型环境实体。此类环境实体具有被感知的属性以及属性的获取操作，例如光照、温度等。建模时采用π-演算的输出动作作为被感知属性的获取操作。被感知属性通过输出动作传递，以便其他环境实体或物联网服务交互获取。

定义1 一个抽象的被感知型环境实体可描述为

(1)

定义1给出了环境实体一种抽象的形式。但在实际应用场景中，被感知属性存在多种属性值。例如光照属性可取的属性值集合为{bright,dark,normal}。为此在定义1的基础上给出一个具体的被感知型环境实体的形式化定义。

定义2 一个具体的被感知型环境实体对象可描述为

(2)

2) 受控型环境实体。相比较于被感知型环境实体，此类环境实体除了受控操作外，还有状态的获取操作。这里使用输入动作表示受控操作，输出动作作为状态获取操作，以实现其他服务或环境实体获取当前操作状态。

定义3 一个受控型环境实体可以描述为

(3)

定义3给出的受控型环境实体，输入动作clopi完成后，环境实体被设置为对应的状态。

1.2 物联网服务建模

1.2.1 原子服务建模

物联网服务的功能通过其与环境实体之间的交互体现，服务通过交互感知到环境的状态，及时地实施对环境的控制，实现改变环境状态的目的[2]。依据服务的类型，原子服务可细分为感知型服务、控制型服务和业务逻辑型服务。

1) 感知型服务。此类服务的主要功能在于定时获取某一类环境实体的状态或感知属性，然后依据状态或感知属性的值做相应的处理。其感知操作可以表示为一个输入动作。使用输出动作表示下一步将要处理的操作，以便与其他服务交互。

定义4 一个时钟变量Clocki(i是时钟数且为大于等于0的正整数)可以表示为

(4)

定义4给出的时钟变量起定时作用。tick为1个时钟，输出动作start表示启动操作。当要表示5个时钟内启动某个操作P，采用π演算的并行操作可将进程进一步书写为Clock5|start.P,那么感知型服务的形式化定义如下。

定义5 一个感知型服务SA可以定义为

(5)

式中：m为大于等于1的正整数；输入动作Attri表示获取被感知型环境实体的第i个属性xi；Vali表示第i个属性可取的属性值；输出动作op表示感知服务以便与其他服务交互的操作。

2) 控制型服务。通过输入动作获取其他服务发来的控制指令，再依据指令类型由输出动作向受控型环境实体发送控制操作，控制型服务的形式化定义如下。

定义6 一个控制型服务CA可以定义为

(6)

式中：输入动作getcodei表示获取其他服务发来的控制指令ci；ti则表示控制指令的某种类型；输出动作clopi表示向受控型环境实体发送控制操作。

3) 业务逻辑型服务。此类服务通过输入动作获取感知型服务传来的信息或受控型环境实体的状态，然后根据传来的信息或状态做相应的逻辑处理，比如再次查询受控型环境实体的状态等，最后使用输出动作传递控制指令。业务逻辑型服务的形式化定义如下。

定义7 一个业务逻辑型服务LA可描述为

(7)

式中动作π可以是输入动作、输出动作或者空动作。

1.2.2 组合服务建模

以原子服务为基础，使用π-演算的并行操作可以得到多个组合服务。组合服务的形式化定义如下。

定义8 一个组合服务ZHA可以定义为

ZHA=SA|LA|CA。

(8)

1.3 建模方法特点

物联网系统是一个并发的交互式系统，是物联网服务与环境实体之间交互的具体表现。基于π-演算和μ-演算相结合的建模方法，对物联网服务、环境实体和物联网服务能力三方面内容进行建模与分析，具有以下几个特点：

1)整个建模方法不依赖任何特定的物联网系统，使用严格的数学定义进行系统建模，具有高度的抽象性。

2)整个建模方法侧重于物联网服务与环境实体之间的交互行为。

3)使用π-演算对物联网服务和环境实体进行行为建模，可以更为抽象地表示物联网服务与环境实体之间的行为交互，建模过程主要以功能行为的描述为主。

4)使用μ-演算公式表示物联网服务能力，本质上将物联网服务具有的性质描述成动态行为的执行路径，只关注服务功能需求问题。

5)行为间交互传递的是消息，结合π-演算描述能力以及名字的概念[11]，将连续型数值属性进行离散化表示。

2 物联网服务验证

本文将物联网服务和环境实体视为进程实体，二者的并行交互形成了一个完整的物联网系统。通过使用π-演算的反应规则[11]可以确定物联网系统的事件发生序列，即物联网服务和环境实体之间的动态行为交互过程。为此对物联网服务的正确性验证就可以看成物联网服务和环境实体之间的动态交互序列的正确性验证，可分解为以下三类性质，并统一采用μ-演算公式来表述。

1)安全性，表示服务交互过程中不期望发生的事件或行为不会被执行。

2) 活性，表示服务交互过程中期望发生的事件或行为最终能执行。

3) 时间约束，表示服务交互过程中某些事件或行为的执行时间要求。

3 实例

本文以智能会议室应用场景为例，用π-演算对环境实体和物联网服务建模，将服务的正确性表述为μ-演算公式，最后使用MWB工具进一步验证物联网服务的正确性。

一个智能会议室场景为：会议室中装有一盏日光灯和一台投影仪。当投影仪开启时，日光灯自动关闭。当投影仪关闭时，环境光线由亮变暗时，日光灯在2 s将会自动启动；当环境光线由暗变亮时，日光灯在2 s内自动关闭。其建模如下：

1)被感知型环境实体

在本实例中，环境光被识别为被感知型环境实体。环境光通过输出动作getint向感知服务输出光线的明亮程度int。其中int∈{da,br}，da表示暗光，br表示强光。为此环境光类可以定义为

(9)

那么环境光实体可以定义为

Enls=Enl+Enl
。

(10)

2)受控型环境实体

投影仪实体具有3个动作：向外提供投影仪当前状态ps的输出动作getps、打开投影仪输入动作pon以及关闭投影仪输入动作poff。投影仪则定义为

(11)

日光灯实体除了和投影仪实体具有类似的3个动作，还使用时钟算子表示开或关的时延性。日光灯则定义为

(12)

3) 感知型服务

感光服务SA先通过输入动作getint获取环境光线的明亮程度int，然后根据明亮程度，分别通过输出动作isda和isbr与业务逻辑服务通信。

(13)

4) 业务逻辑型服务

业务逻辑服务P1，在使用输入动作getps获取投影仪的当前状态后，依据当前状态是否为开启状态，通过输出动作lampcode发出关闭指令off。

P1=getps(ps).([ps=

(14)

业务逻辑服务P2，可通过输入动作isbr与感光服务SA通信，然后通过输出动作lampcode发出关闭指令off；又或者通过输入动作isda与感光服务SA通信，而后使用输入动作getps获取投影仪状态，依据投影仪是否关闭，通过输出动作lampcode发出开启指令。

(15)

5) 控制型服务

控制型服务Lcon，用来控制日光灯的开启或关闭。首先通过输入动作lampcode获取指令code，依据指令的类型，向日光灯实体发出开启lon或关闭loff的动作。

(16)

为验证服务的正确性，需要将上述模块进行组合计算，因此一个智能会议室场景可以描述为

(17)

那么该智能会议室场景可满足的三类性质，描述如下：

(1)当投影仪打开时，日光灯关闭，如式(18)所示。

true。

(18)

(2) 当投影仪关闭时，环境光线昏暗情况下，日光灯打开，如式(19)所示。

(19)

(3) 日光灯2 s内启动

该性质可分为投影仪开启后日光灯2 s内关闭(如式(20)所示)和投影仪关闭后日光灯2 s内开启(如式(21)所示)。

(20)

(21)

(4) 当投影仪打开后，环境光线昏暗情况下，日光灯不会打开,如式(22)所示。

(22)

其中式(18)和式(19)表示的是活性，时间约束性质由式(20)和式(21)表示，而式(22)则表示安全性。

将本文所描述的环境实体和物联网服务以及式(18)—式(22)使用MWB工具进行描述，并使用prove命令可以得到所设计的物联网服务建模满足式(18)—式(22)所代表的性质，其在MWB工具上的运行效果如图1—图5所示。这验证了所设计的物联网服务建模的正确性。

图1 式(18)的验证结果Fig.1 The verification result of the formula (18)

图2 式(19)的验证结果Fig.2 The verification result of the formula (19)

图3 式(20)的验证结果Fig.3 The verification result of the formula (20)

图4 式(21)的验证结果Fig.4 The verification result of the formula (21)

图5 式(22)的验证结果Fig.5 The verification result of the formula (22)

4 结束语

本文针对基于环境建模的物联网服务框架，从动态行为交互建模的角度出发，提出了一种基于π-演算和μ-演算相结合的物联网服务建模方法，并给出智能会议室应用场景实例说明此方法的具体应用。首先通过使用π-演算分别对环境实体和物联网服务进行行为建模，然后使用μ-演算将物联网服务具有的性质描述成动态行为的执行路径，最后采用MWB模型检测工具，对智能会议室实例的性质进行了验证，通过验证该模型满足安全性、活性和时间约束三个性质，进一步说明了此方法的正确性和可行性，为物联网服务建模研究提供了参考。

本文研究的是物联网服务动态行为建模，其服务组合方式以并行组合为主，下一步将对环境实体状态的自主变化、连续型数值的表示以及服务的其他组合方式等问题进行建模描述，同时也需要解决在实验验证过程中出现的状态空间爆炸问题。