监测WSNs系统具有便于部署、可移动性强、可回收再利用等显著特点，是煤矿生产安全保障的一个重要应用。瓦斯监测WSNs系统是基于WSNs，对煤矿巷道气体等对象状态的数据收集并预警的系统。WSNs监测数据与生产安全紧密结合，甚至，WSNs安全问题往往就是生产安全问题的表现[1]。例如，“监测岩土状况(使用岩土应力和位移监测来预警冒落)的无线节点失效”可能就表示“冒落”已经发生。因此，实体与WSNs监测的交互行为需要联合进行安全检验，以保障WSNs系统功能的可用性。瓦斯监测WSNs系统是煤矿生产安全的重要一环，对其进行安全可行性检验是保障煤矿生产安全的一种新方法。
对生产安全监测WSNs的可用性验证，是利用WSNs本身和生产安全中产生的、可描述系统状态的数据，通过统计分析，利用模型检测方法，检测系统可能存在的异常状态，保障系统正确运行的测试技术。煤矿瓦斯WSNs监测系统验证包括:对采集气体数据的传感器元件的安全、嵌入式设备的预设报警功能、网络协议和生产安全预警疏散功能的验证。
借鉴软件可靠性验证思想，监测WSNs模型验证是将可靠性和可用性定量描述，利用逻辑、概率等方法量化系统的当前状态，预测系统的未来效果[3-4]。如马尔科夫过程模型、贝叶斯可靠性模型、seeding模型、输入域模型等[5]，依靠大量数据的仿真，利用概率和统计方法来发现系统异常。例如，LO将传感器失效与读取错误模型转换为LER(Large Empty Rectangle)问题，孤立了具有非线性特征的错误[6]。OZDEMIR保证了中间节点对转发数据完整性，减少了传输错误[7]。IHSAN比较LEACH协议及其扩展LEACH-C和LEACH-F，验证了各个簇能量的可持续能力[8]。SOUZA验证了IEC 61850标准发送和接收，证明了按区域使用不同节点密度WSN的技术可行性[9]。JIN系统地结合局部监测、位置估计和节点协作数据，提出两个节点链接故障检测方案[10]。上述的仿真验证大多针对WSNs某一项功能进行检验。由于利用统计验证方法不易建立大的规则集，这些方法不易预检WSNs的未知错误，要其它方法补充。
形式化方法通过逻辑证明，在故障发生前给出是否会发生的结论，非常适合系统设计的预检和维护。在无线系统中，该方法对协议验证有非常好的效果。例如，利用分支时序逻辑，GHASSEMI检验了multi-hop协议在底层拓扑连通性变化时的效应和时序行为，保证了路径更新的正确性[11]。冯晓宁描述了无线传感器节点的广播与单播通信行为，通过结构同余进行了多节点的等价检验[12]。通过模型和验证语义转换，模型检验可以简化检验问题。OLVECZKY通过利用Maude module和成员等价逻辑，将密度问题转换为性质验证问题，发现NS2模拟缺少时间延迟[13]。通过基于UML的RWSN元模型来描述系统的区域结构，GRICHI提出了优化分布式重分配协议,建立了RWSN元模型和区域多代理体系结构来处理网络重构[14]。
相应的形式化验证工具也被开发和应用，如TOSSIM，TOSSF(TinyOS Scalable Simulation Framework)，SNIF(Scent-based Navigation and Information Foraging),WSNSim,UPPAAL,SPIN，RWSN等检测工具[3,14-15]。李戈引入环境实体以刻画物体的属性和行为，利用UPPAAL将物联网及其监测的实体变化进行联合检验[15]。文献[16]从节点位置的角度进行建模，检验节点通信的安全性。CHEN从QoS角度用UPPAAL建模，检验时间传输的QoS稳定性[17]。这些研究从不同角度显示了形式化验证的有效性，但鲜有涉及研究节点移动特征和被监测环境实体的生产安全功能设计的检验。
笔者针对感知数据描述的生产安全规则，提出WSNs与被监测实体间并发交互功能模型的建立方法，实现监测WSNs安全与生产安全同时检验，进行生产安全保障功能可用性的验证;并针对交互行为形成的并发模型，建立环境实体模型的并发分支与融汇的基本规则，约减模型的状态数量，给出了可行的检验方法。最后，利用该方法，对国标《AQ1029—2007》[2]中的瓦斯监测模型进行检验，发现在某些条件下，其中一个瓦斯部署模型设计的不足。
1 生产安全监测WSNs交互行为的时间自动机模型及其互模拟约简
1.1 实体及其行为并发的时间自动机
时间自动机[18]是一种用于描述、分析实时系统行为的形式化模型。同Petri网相比，容易描述不同实体间的并发行为。结合UPPAAL工具，本文中主要符号含义见表1。
表1 本文涉及的符号[19]
Table 1 Symbols involved in this paper[19]
符号含义Chan所有信道名的集合P命题的集合Act所有动作的集合,a为其中的变量,包含输入、输出和内部(τ)3类动作,Act={a?| a∈Chan}∪{a!| a∈Chan}∪{τ}Clock所有的时钟变量集合Var所有的数据变量集合Guard在时钟变量C和数据变量v∈Var上建立的迁移约束条件,称为保卫公式(guards),记Φ(C,Var)id实体的身份标识S自动机的状态,S0为初始状态,Si为一个状态Φ自动机约束公式集R行为互模拟等价关系t行为迹,由状态、动作和迁移时间组成
在时钟变量和数据变量的集合上，取值的约束条件，即保卫公式(guards)，记为Φ(C,Var)。
定义1:时间自动机[19]。一个时间自动机可以定义为一个元组TA=(S,S0,A,C,V,I,E),其中，S为有限状态集;S0为初始状态;A⊆Act为动作集;C⊆Clock为时钟变量集;V:S→2P为命题赋值函数，将状态设置为原子命题集合;I:S→Φ(C,Var)为对状态进行约束的函数，称为状态的不变量;E:S×Φ(C,Var)×A×2C×S为自动机有向边集合，元组<s,g,a,r,s’>∈E表示在约束g下，时钟r重置并执行行为a时，状态s到状态s’的有向边。
定义2:实体类自动机。一个实体类可标识为O=<Oid,Attr,TA,F>。其中Oid为实体类的惟一标志;Attr为实体类属性集合;TA为时间自动机，TA.S为实体状态，TA.A为实体类行为集合，TA.E为实体行为引发的实体自身变化;F:Attr→2P是实体类属性刻画自动机状态的函数。
当多个实体进行共同活动时，实体并发行为会互相影响。实体行为并发过程如定义3。
定义3:行为并发。假设有n个实体{O1,…,On}，其中，对i ∈[1,n],Oi=(Oid,i,Attri,TAi,Fi)，则n个实体行为并发过程为O1‖f1O2,……‖fn-1On，其中fi,i∈[1,n]为自动机并发过程的约束。
1.2 实体及其交互行为的建模与性质检验
检验模型建立的核心是实体状态集及其上迁移矩阵的建立。在时间自动机中，不同时段的属性值反映了系统的不同状态。选取状态迁移中发生变化的属性来区分不同状态。
以矿山瓦斯监测为例。模型检验要将矿山监测中实体元素抽象到自动机描述中。涉及的实体包括:瓦斯传感器与预警装置，信号中继，巷道等。将实体分为3类:WSNs、人员和其他被监测实体。根据实体行为，确定实体模型不同的状态。例如，传感器实体具有感知(Sensing)、传输和应答(Send and Ack)、预警(Alarming)、休眠(Wait)等引发迁移的行为，找到相应变化的属性集，建立如图1所示模型。网络自检测是通过节点之间交互发现fault状态的，由ack状态转移，进入mending状态。
在WSNs行为集中，预警与感知是与矿山环境交互的行为。如图1所示，sensor对生产安全的感知和反馈体现在sensing和alarming上。由于各个实体间的独立性，交互行为需同时映射到多个实体自动机的操作语义上。图1中的alarm就是传感器与所监测实体的并发行为。人员的行为与alarm行为交互，如图2所示，时间t的单位为s。当sensor的alarm的行为发生时，人员将被动发生并发的alarm行为，形成二者行为并发。除与alarm发生交互产生的逃避状态外，人员模型还有进入监控区域(movein)、移动(moving)和走出监控区域(moveout)的状态。
图1 传感器实体的时间自动机模型(alarming状态 表示发送alarm消息)
Fig.1 Timed automata model of sensor entity (alarming status means to send alarm msg)
图2 人员的时间自动机模型
Fig.2 Timed automata model of worker
瓦斯监测WSNs系统的可用性验证是检测WSNs系统监测实体安全的功能是否可满足，其表现是涉及的被监测实体安全状态可被保障。在自动机上，可用性的验证是在多个实体模型组成的集合上，进行可用性性质描述的状态可满足性验证。
安全性质的描述要考虑WSNs系统和实体安全两个方面。因此，图1中，安全性质包括两个部分:sensor可用和人员安全状态。本文采用UPPAAL的时序逻辑语言描述。Sensor可用性的性质描述是:
gas.density>threshold→sensor.alarm
(1)
被保障的人员实体的安全性质描述为
people.getalarm→people.moveout
(2)
系统对人员安全的性质可描述为
gas.density>threshold→people.moveout
(3)
式(3)的检验过程将先在sensor模型上检验式(1)，然后由alarm并发引动人员模型对式(2)检验，最终完成式(3)的检验。
上述检验过程可以看出，可用性性质的逻辑描述由WSNs自身与被监测实体安全两部分融合形成。经分析，瓦斯监测WSNs系统的可用性性质建立可利用模型检验安全性质的建立方法。利用方法如下:① 利用可达性(reachability)描述WSNs安全监测功能的必备条件。例如，瓦斯监测报警状态功能满足，其逻辑公式表示为:∃◇sensor.alarm。② 利用安全性(safety)描述实体安全事故状态的规避与监测可靠性。例如，WSNs监测系统运行不出现死锁，可表示为∀□no deadlock。③ 利用活性(liveness)描述实体发生交互行为的安全状态。例如，发现气体浓度高于阈值，人员立即获得预警信息，可以表示为gas.density>threshold→people.getalarm and time<1 s。④ 通过时钟和行为的约束，描述可用性中的时效约束。例如，瓦斯浓度超限或通风机停止运行时间不超过1 min，进行零级报警，可表示为:gas.density>threshold
Main Ventilation.stopclock <60 s→sensor.alarm0。
在检验过程中，当实体具有并行结构时，若并行结构之间互相影响，实体本身将具备并发行为。类似的实体有MIMO(Multi-In-Multi-Out)模块、含分支的管道等。如果具有并发特征的实体(Concurrently-action Object,CaO)的并发行为同其他多个实体同时存在交互，则CaO各分支并发行为的状态迁移需要同时被执行。下文将利用等价模型分析该问题。
1.3 并发行为时空关系的互模拟等价约简
如果为CaO实体的每个并发交互过程建立模型，则实体模型将被拆分成很多个模块，导致检验模型过多，引发空间爆炸问题。若将位置和时间建立直接联系，将其等价为域自动机[20]，又会失去模型的时间独立性并存在状态爆炸问题。上述两种建模方法实用价值很小。本文利用域限定思想，根据位置与时间的关系，将位置信息转换为时间约束，构建并发行为的互模拟等价来简化模型。
定义4:行为互模拟。两个实体模型Ok=<Oid,k,Attrk,TAk,Fk>，k∈{1,2}，Attr1=Attr2且F1=F2。如果存在关系R⊆ TA1.S×TA2.S，满足:① 如果对任何状态存在
则有
反之亦然;② 对加入时间约束的迁移关系，形成的迹有τ(TA1.S1,TA1.S2,t)=τ(TA2.S1,TA2.S2,t);则称关系R是实体上的行为互模拟，记为～。
命题1：～是等价关系。
证明:根据自动机和关系R的定义，R是对称和自反的。设存在～1和～2为互模拟关系，使得实体O1～1O2，O2～2O3，则:①有且有
反之亦然;② 因为对O2状态迁移 TA2.S1→ TA2.S2，分别有τ1(TA1.S1,TA1.S2,t)=τ1(TA2.S1,TA2.S2,t)，τ2(TA2.S1,TA2.S2,t)=τ2(TA3.S1,TA3.S2,t)，且τ1(TA2.S1,TA2.S2,t)=τ2(TA2.S1,TA2.S2,t)。因此，～是传递的。命题得证。证毕。
针对CaO实体模型的建立问题，利用时空之间关系，对巷道等实体模型进行互模拟转换，减少空间结构不同形成的同类模型的数量。根据命题1，对空间地理位置，利用被监测实体位置移动前后属于同类的特点，对固定移动轨迹的实体进行简化，形成如下命题。
命题2:状态模拟等价合并。
一个实体模型O=<Oid,Attr,TA,F>，有2个状态
表示S1执行Act经过时间t迁移至S2且S1出度和S2入度均为1，位置LOC1∈ S1，LOC2∈ S2，若Act行为使得LOC属性发生变化，且LOC1≠LOC2时，S1.Attr=S2.Attr，则状态S1,S2可合并为一个新状态
有一个执行时间为t的内部动作Act的自环边，属性约束为
新状态的自动机O′≅ O。
证明:令τ=Si…S1S2 …Sj是经过状态S1S2的迹，并使得
存在一条迹τ′=Si…S1′…Sj经过状态S1′，由于除LOC1≠LOC2外S1.Attr=S2.Attr，τ经由S1S2时，S1输入与S2输出和S1′与S2′相同且Act执行时间相同，因此τ与τ′的耗费时间一致，则
反之亦成立。对于不经过状态S1S2的迹，模型O与O′是相同的。因此，两个模型的行为互模拟等价。证毕。
命题2减少了有空间特征模型的状态数量。例如，巷道内的人员移动行为，如图3(a)所示，根据人员在巷道出入口的位置和速度属性，可将中间状态等价描述为一个Moving状态。图3(b)中Moving状态利用speed将LOC间的距离变成时间信息，让人员移动变为一种含内部动作的状态，Enter和Exit状态间的距离信息约简为时间信息。
图3 利用时间约束简化含有空间属性的模型
Fig.3 Simplified model with spatial attributes by timed constraints
结合文献[21]中互模拟等价与内部动作，命题2推广至实体模型，则有命题3。
命题3:实体模拟等价合并。两个实体模型Ok=<Oid,k,Attrk,TAk,Fk>，k∈{1,2}。若存在双射FS使得TA1.Ei
TA2.Ei，对
有t1=t2;且当
差集Pk1⊆TA1.S2 且Pk1⊆TA1.S1，Pk2 ⊆TA2.S2 且Pk2⊄TA2.S1，有Pk1=Pk2;则2个模型可模拟等价合并为O′=<Oid′,Attr′,TA′,F′>，其中Attr′=Attr1∪Attr2，TA′.Si=TA1.Si∪TA2.Si。
证明:令τ=Si…Sq…Sj是经过状态TAk的任一条迹，并使得如果τ中Act
TA1.A∩TA2.A，则根据FS函数选取TA′.S中的对应状态组成路径τ′，Act行为将不影响TAl，k≠l，属于中的状态属性，因此，τ′与τ可以互模拟;若Act∈ TA1.A∩ TA2.A，该行为将引发2个实体的共享信道并发运行，由于自动机TA1与TA2状态迁移的差集Pk1=Pk2，因此状态
中状态改变与
相同,τ′与τ可以互模拟。综上，Ok≅O′。证毕。
命题3从总体上减少了自动机的叉积运算，为联系紧密的实体模型合并提供依据，对管道和流体等共同工作的自动机模型进行合并。命题2描述的迹是一种线性时间序列，当存在并发分支时，命题2中实体的Act执行与发生位置LOC有关，时序关系在同一时间自动机模型中不易描述。为解决该问题，对此类实体模型拆分，将行为互模拟扩充至群体中，形成定义5。
定义5:集体行为互模拟。实体模型Ok=<Oid,k,Attrk,TAk,Fk>组成两个集合{Oi}{Om}，i,j ∈{1,2,…,k}，∪iAttri=∪jAttrjV且∪iFi=∪jFj。如果存在关系RU⊆∪iTAi.S×∪jTAj.S，满足①若存在
则
反之亦然;② 加入时间约束的关系τU(TAi.S1,TAi.S2,t)=τU(TAj.S1,TAj.S2,t);则称关系RU是实体上的行为互模拟，记为～U。
命题4:～U是等价关系。
证明:根据自动机和关系RU的定义，RU是对称和自反的。设存在～U1和～U2为互模拟关系，使得实体集合{Oi}～U1{Oj}，{Oj}～U2{Ol}，则:
(1)如果行为不是并发的，则有且有
反之也成立。
(2)如果存在并发行为，TAi1.
则在t时刻，将有对应的行为TAj1.
和TAj2.
它们也将同时发生;且有τU1(TAi.S1,TAi.S2,t)=τU1(TAj.S1,TAj.S2,t)=τU2(TAj.S1,TAj.S2,t)=τU2(TAl.S1,TAl.S2,t)。因此，～U是传递的。命题得证。证毕。
在定义5的基础上，命题5利用等价模型进行实体模型的拆解。
命题5:并发分支等价。
一个实体模型O=<Oid,Attr,TA,F>，状态集合TA.S存在一个划分{Sj}∪{Sk}，j,k∈[1,n]且j≠k。状态S1∈{Sj}，在某时刻
且
该TA可拆分为2个并发时间自动机模型TA=TA1||TA2，其中{Sj}⊆TA1.S，{S1}∪{Sk}⊆TA2.S，则{O}～U{O1}∪{O2}，其中O1=<Oid,1,Attr,TA1,F>,O2=<Oid,2,Attr,TA2,F>。
证明:构造实体集合{O}和{O1,O2}，满足TA.S={Sj}∪{Sk}，其中j,k∈[1,n]且j≠k，状态S1∈{Sj}，{Sj}⊆TA1.S，{S1}∪{Sk}⊆TA2.S。建立双射关系PBR:① TA.Si
TA1.Si,if Si∈TA1.S/S1;② TA.SiTA2.Si,if Si∈TA2.S/S1;③ TA.SiTA1.Si∪ TA2.Si,TA.act=TA1.act‖TA2.act，if Si∈TA1.S1。对情形①由于状态和动作相同，对任一迁移有
必然有
反之亦然;因此，① 中PBR是互模拟等价的。同理，② 中PBR也是互模拟等价的。对情形③，根据前面的假设关系，如果有
必然有
由于TA1.S1=TA2.S1=TA.S1，TA.S2=TA1.S2∪ TA2.S2,行为Act和时间约束相同，因此TA可被TA1∪ TA2行为模拟;反之亦然。因此，PBR是互模拟等价的。证毕。
命题6:利用汇聚过程重新构建并发模型，减少模型数量。
命题6(并发汇聚等价)两个实体模型Ok=<Oid,k,Attr,TAk,F>，k∈{1,2}。有状态S1′,S2′∈TA1;S1″,S2″ ∈TA2，在某时刻t，分别同时从S1′,S1″迁移至TA1,TA2的状态S2′,S2″，迁移过程为
和
如果有属性差集Pk1⊆TA1.S2′ 且Pk1⊄TA1.S1′，Pk2 ⊆ TA2.S2′′，且Pk2⊄TA2.S1′，有Pk1=Pk2，则两个实体模型可合并状态S2=S2′∪ S2″，组成O=<Oid,Attr,TA,F>，其中TA=TA1‖TA2，则{O}～U{O1}∪{O2}。证明略。
2 矿山生产安全的WSNs监测系统检验样例
对煤矿生产安全标准《AQ1029—2007》，选择矿山巷道瓦斯部署的模型检验作为矿山生产安全检验的样例。
2.1 标准《AQ1029—2007》的分析与检验目标
在上述标准中，对其中所有瓦斯监测WSNs部署的模型进行了检验，发现如图4所示的瓦斯传感器安装规范存在不足。该样例中，矿山安全瓦斯监测的巷道存在空气并发流动的情况，需检验矿山传感器安装位置是否满足报警后人员安全逃入避难硐室(Refuge)这一设计。在支巷中设置如图4所示的两个传感器，假设巷道宽度小于3 m，各巷道布局如图4所示。
图4 巷道瓦斯检测示意
Fig.4 Gas detection in tunnels
矿山WSNs监测生产安全的缺陷反映为预警失效或误报。因此，图4中瓦斯监测WSNs可用性检验目标设定为:传感器报警后，人员是否能够在限定时间内进入避难硐室。
2.2 实体类模型与实体的创建
上述矿山生产安全监测场景涉及的实体包括巷道、空气、瓦斯传感器、人员和WSNs。其中，巷道存在分支结构且不同分支与不同实体交互，属于CaO。根据命题2，将巷道中的空气模型合并入巷道模型。所涉及的实体类模型包含:
传感器模型。每类传感器建立一个类模型。如图5所示，瓦斯传感器类表示为GAS=<Sid,{location,gasdensity,energy,threshold,alartime},TASensor,{gasdensity→ alarm_level {0,1} }>，其中gasdensity为传感器对瓦斯气体的感知值，energy为电量，threshold为阈值，alarm_level为预警等级，此处只假设有预警和不预警两种选择，将维护工作并入模型为传感器被维护状态。行为描述TASensor包括等待、监测、报警、上传和被维护;并发行为为:从monitor信道获得监测信息，从broad信道送出数据信息，alarm信道用于发送预警信息。整个过程形成的8种状态，其中unalarm指数据错误状态，Fault状态表示硬件错误，Mengding为维修状态。
图5 瓦斯传感器时间自动机模型
Fig.5 Timed automata model of gas sensor
中继设备模型。类定义为Relay=<Rid,{energy,delaytime},TARelay,{delaytime→clocktime}>，其中，delaytime为信号传输延迟时间。如图6所示，行为描述TARelay包括等待、转发、检测数据和被维护，并发行为为:从broad共享信道获取信息，tr为重试次数，用front函数传输并计算能量。
图6 中继器时间自动机模型
Fig.6 Timed automata model of relays
人员模型。人员配备的一个随身传感设备，用于获得矿山工作人员移动过程中的位置和速度、健康状态等信息。类定义为Miner=
巷道与空气模型。根据命题3，空气模型并入巷道模型类，瓦斯浓度作为巷道的属性。类定义为Tunnels=<Tid,{windspeed,alartime,airgasdensity},TATunnels,{windspeed→clocktime}>，其中，windspeed为空气流动速度,airgasdensity为瓦斯浓度。根据命题5，巷道并行模型TATunnels拆成2个等价模型，如图7所示，wind为共享信道，表示空气流动的并发。根据命题6，在S2状态处进行共享变量汇聚。两个巷道模型同时接收monitor信道，接收传感器信道的感知数据。block用于标注该位置是否阻塞，检验阻塞后果。
图7 巷道与空气时间自动机模型
Fig.7 Timed automata model of tunnel and air flow
上述模型中的空间位置，通过气体和人员的移动速度转换为时间标签。
2.3 安全监测WSNs设计的检验与分析
对上述场景建立模型的数量为:瓦斯传感器模型2个，中继模型1个，人员模型1个，巷道分支模型2个。实体模型组合成一个整体自动机模型:GAS||Relay||Miner|| Tunnels.
首先，保障监测系统的可用特性:整个系统不出现死锁，表示为:□not deadlock。验证结果满足，说明上述模型可以正常运行。其次，检验数据传输、节点故障和人员安全等其他功能的可用特性，见表2。对比巷道模型约简方法使用前后的检验时间，在相同机器情况下，约简后模型的检验时间节省约20%左右，与状态数目约简比例正相关。
表2结果显示在正常状态下，标准中的WSNs监测模型所设定的功能是满足的。但是，事故的发生会对并发行为造成影响。本文发现在发生巷道堵塞(灾难)时，上述性质可满足性存在疑问。图3中，针对不同的位置增加s1，s2，s4，s5进行标记，分别对应图7中的不同状态。在原有模型中，对位置s1，s2，s4，s5增加block事件，依次进行检验表2中的性质，发现性质3不满足。
跟踪系统检测过程，WSNs部署模型的设计不满足场景如下:当s5位置堵塞时，空气流发生堵塞，若s4位置发生瓦斯泄漏，传感器不报警，人员不能做到及时撤离，造成状态不满足。说明在此种情形下，标准中的瓦斯传感器部署设计有缺陷，是由于瓦斯传感器无法反映巷道中分支气流变化造成的。根据传感器的特性，在s4或s5位置增设瓦斯预警传感器可解决该问题。更好的方法是在模型中增设气体流量传感器[22]，用于探测堵塞事件。修正后的模型在瓦斯传感器附近增设风速fluency传感器，如图8所示。此时，堵塞事件的发生可以被风速传感器模型检测出来。
表2 实例模型的性质检验结果
Table 2 Property checking results of the case entity model
序号检验目的性质描述未约简检验耗时/s约简后检验耗时/s(节省时间比/%)检验结果1网络功能:单传感器失效时,监测是否可靠E<>GasSensor(i).alarming→GasSensor(1).alarm1.811.47(23)satisfied2网络功能:瓦斯数据是否能被转发E<> Relay.Receive1.611.35(19)satisfied3生产安全:瓦斯浓度大于阈值时能否保证工人安全A[] Tunnel22.s(i)->Miners(i).Moveout5.174.21(22)satisfied4系统安全:系统是否存在死锁□not deadlock5.574.60(21)satisfied
图8 根据检验结果修正后的模型
Fig.8 Mending model based on checking result
由于模拟仿真的方法对位置感知不易表示，不易发现这种因为交互实体并发行为造成的错误。对比WSNs仿真器，如NS2，上述环境改变造成的WSNs系统功能的缺漏不能得到反映。
3 结 语
形式化验证已经在芯片设计、火车并发检验等实际工作中大量应用。将其引入煤矿监测安全设计检验是智慧矿山提供机器智能检验的重要一步。针对生产安全中WSNs监测系统设计的正确性检验，本文以时间自动机为工具，通过时间自动机组合来刻画被监测环境中的实体并发行为和交互行为，构造并发结构模型，形成对生产安全监测功能的可用性机器验证方法。据此发现了实际标准中存在的，在含分支巷道的情况下，瓦斯监控传感器部署设计上的个别缺陷，证明了该方法对WSNs安全和生产安全的联合验证的有效性。在下一步工作，将刻画被监测环境中实体的原子模型，提高生产安全设计检测的灵活性，进一步提高该方法在现场的实际应用能力。
[1] LI M,LIU Y.Underground coal mine monitoring with wireless sensor networks[J].ACM Transaction on Sensor Networks,2009,5(2):Article 10.
[2] 中国国家煤炭安全监察局.煤矿安全监控系统及检测仪器使用管理规范(AQ1029—2007)[S].2007.
[3] TESTA A,CORONATO A.A review of the methods for the dependability assessment of WSNs:Towards a new approach[J].Adhoc & Sensor Wireless Networks,2016,33(15):223-252.
[4] LYU M R.Handbook of software reliability engineering[M].NewYork:Graw2Hill,1996.
[5] SALAYMA M,AL-DUBAI A.Wireless body area network (WBAN):A survey on reliability,fault tolerance,and technologies coexistence[J].ACM Computing Surveys (CSUR),2017,50(1):3.
[6] LO C,LYNCH J P,LIU M.Distributed model-based nonlinear sensor fault diagnosis in wireless sensor networks[J].Mechanical Systems and Signal Processing,2016,30(1):470-484.
[7] OZDEMIR S,CAM H.Integration of false data detection with data aggregation and confidential transmission in wireless sensor networks[J].IEEE Transactions on Networking,2010,18(3):736-750.
[8] IHSAN A,SAGHAR K,FATIMA T,et al.Formal comparison of LEACH and its extensions[J].Computer Standards & Interface,2019,62(2):119-127.
[9] SOUZA R,MOREIRA,L R,RODRIGUES J,et al.Deploying wireless sensor networks-based smart grid for smart meters monitoring and control[J].International Journal of Communication Systems,2018,31(10):e3557.
[10] JIN R,WANG B,WEI W,et al.Detecting node failures in mobile wireless networks:A probabilistic approach[J].IEEE Transactions on Mobile Computing,2016,15(7):1647-1660.
[11] GHASSEMI F,FOKKINK W.Model checking mobile ad hoc networks[J].Formal Methods In System Design,2016,49(3):159-189.
[12] 冯晓宁,王卓,张旭.基于L-π演算的WSN路由协议形式化方法[J].吉林大学学报,2015(5):1565-1571.
FENG Xiaoning,WANG Zhuo,ZHANG Xu.Formal method for routing protocol of WSN based on L-π calculus[J].Journal of Jilin University,2015(5):1565-1571.
[13] OLVECZKY P C,THORVALDSEN S.Formal modeling,performance estimation,and model checking of wireless sensor network algorithms in real-time maude[J].Theoretical Computer Science,2009,410(2-3):254-280.
[14] GRICHI H,MOSBAHI O,KHALGUI M,et al.RWiN:New methodology for the development of reconfigurable WSN[J].IEEE Transactions on Automation Science and Engineering,2016,14(1):109-125.
[15] 李戈,魏强，李力行,等.物联网服务建模:一种基于环境建模的方法[J].中国科学:信息科学,2013(10):1198-1218.
LI Ge,WEI Qiang,LI Lixing,et al.Environment based modeling approach for services in the internet of things[J].China Science:Information Sciences,2013(10):1198-1218.
[16] CHEN T,YU Z,LI S,et al.From wireless sensor networks to wireless body area networks:Formal modeling and verification on security using PAT2[J].Journal of Sensors,2016,8797568.
[17] CHEN Z,PENG Y,YUE W.Model-checking driven design of qos-based routing protocol for wireless sensor networks[J].Journal of Sensors,2015(6):1-7.
[18] ALUR R,DILL D L.A theory of timed automata[J].Theoretical Computer Science,1994,126(2):183-235.
[19] KIM G L,PETTERSSON P,MARTINELLI F.UPPAAL[Online].http://www.uppaal.org/,2017-09.
[20] ALUR R,CORCOUETIS C,DILL D.Model checking in dense real-time[J].Information and Computation,1993,104(1):2-34.
[21] LAROUSSINIE F.CHRISTEL B,JOOST PIETER K.Principles of model checking[J].Computer Journal,2010,53(5):615-616.
[22] ZHOU Lihong,YUAN Liming,THOMAS R,et al.Determination of velocity correction factors for real-time air velocity monitoring in underground mines[J].International Journal of Coal Science & Technology,2017,4(4):322-332.
