若煤矿瓦斯监测WSNs(Wireless Sensor Networks)系统的功能设计忽略了被监测实体的交互行为，会造成WSNs本身可靠而被监测实体的安全不满足情况，这在生产安全中是非常危险的。为检验WSNs监测系统功能设计的可靠性和可用性，利用时间自动机模型检验方法建立WSNs监测系统模型，检验WSNs系统的可靠性。然后，根据传感器与环境实体间的交互关系，分析煤矿中多个实体的并发行为，提出了监测WSNs与被监测实体交互并发行为的时间自动机模型和可用性性质描述的建立方法，从监测功能设计角度，将被监测实体的安全并入WSNs监测生产安全的功能性质，然后用模型检验方法进行机器检验，保障了监测系统的可用性。对含有并发结构的实体模型，利用分支行为等价构建并发时间自动机模型，再利用实体间的并发分支汇聚行为互模拟的方法，进行了并发行为模型的状态约减，并通过互模拟等价证明了该方法的正确性。状态约减前后的实验对比表明该方法提高了检验效率。最后，对现行巷道中瓦斯传感器的部署标准，利用该方法对其中的实际部署方案进行建模并检验，在模型中考虑实体的并发行为，发现在并发事件发生时，其中一个含支巷的瓦斯部署模型存在一个潜在的瓦斯泄露漏检问题。利用实体建模的模型检验方法需要建立自动建模机制，以提高该方法的实用性。

If the functional design of the Wireless Sensor Networks system ignores the interaction behaviors among the WSNs and the monitored entities,it will lead to the situation that a WSNs system itself is reliable but its monitoring en- tity’s safety is not warranted. This situation is very dangerous in industrial production process. In order to verify the re- liability and applicability of the functional design of WSNs monitoring system,the model of WSNs system was estab- lished based on time automaton model to check WSNs reliability. According to the relationship between sensors and mine environmental entities,the authors analyzed the parallel behaviors among the sensors and monitored entities in mine. Then,the authors proposed the timed automata model of the WSNs behaviors interacting with these entities,and established the description method of the applicability properties of the whole system. Based on the model,from the point of view of WSNs’ functional design,combining these interactive entities,the WSNs’ ability of monitoring pro- duction processes was tested to ensure the applicability of the system functions. Because some physical entities contain concurrent structures,the branch behavior equivalence was used to construct the concurrent time automaton models of entities. Moreover,using the method of mutual simulation of the concurrent branch aggregation behavior between enti- ties,the models of entities parallel behaviors were aggregated into one. The correctness of these methods was proved based on the equivalent mutual simulation. Thus,the number of the model states was reduced and the efficiency of the verification process was increased. Finally,aiming to the actual roadway deployment plan of the gas sensor in the cur- rent standards,the method to test gas sensor deployment solutions written in a current standard was used. Considering the entity’s concurrent behaviors,it was found that one of the gas sensor deployment solutions containing branch road- way with a potential missed detection of gas-leak. This checking method combining entities model needs an automatic establishment mechanism to improve its practicability.