基于实体交互模型巷道瓦斯监测WSNs的可用性检验 论文

若煤矿瓦斯监测WSNs(Wireless Sensor Networks)系统的功能设计忽略了被监测实体的交互行为，会造成WSNs本身可靠而被监测实体的安全不满足情况，这在生产安全中是非常危险的。为检验WSNs监测系统功能设计的可靠性和可用性，利用时间自动机模型检验方法建立WSNs监测系统模型，检验WSNs系统的可靠性。然后，根据传感器与环境实体间的交互关系，分析煤矿中多个实体的并发行为，提出了监测WSNs与被监测实体交互并发行为的时间自动机模型和可用性性质描述的建立方法，从监测功能设计角度，将被监测实体的安全并入WSNs监测生产安全的功能性质，然后用模型检验方法进行机器检验，保障了监测系统的可用性。对含有并发结构的实体模型，利用分支行为等价构建并发时间自动机模型，再利用实体间的并发分支汇聚行为互模拟的方法，进行了并发行为模型的状态约减，并通过互模拟等价证明了该方法的正确性。状态约减前后的实验对比表明该方法提高了检验效率。最后，对现行巷道中瓦斯传感器的部署标准，利用该方法对其中的实际部署方案进行建模并检验，在模型中考虑实体的并发行为，发现在并发事件发生时，其中一个含支巷的瓦斯部署模型存《基于实体交互模型巷道瓦斯监测WSNs的可用性检验》这篇论文主要探讨了如何确保煤矿瓦斯监测无线传感器网络（WSNs）系统的可靠性和可用性，特别是在考虑到被监测实体交互行为的情况下。论文指出，如果忽视了这些交互，可能会导致WSNs自身的工作正常，但无法有效保障被监测实体的安全，这在煤矿安全生产中具有重大风险。论文采用时间自动机模型检验方法来建立WSNs监测系统的模型，以此来验证系统的可靠性。通过这种方式，可以检查WSNs在不同工况下的性能和稳定性。接着，作者分析了传感器与环境实体之间的交互关系，特别是煤矿环境中多个实体的并发行为。他们提出了一种新的方法，即利用时间自动机模型来描述监测WSNs与被监测实体交互并发行为，以及建立可用性性质的描述。通过这种方式，可以将被监测实体的安全需求融入到WSNs的监测功能设计中，进一步使用模型检验技术进行机器验证，确保系统的可用性。在处理具有并发结构的实体模型时，论文采用了分支行为等价构建并发时间自动机模型，并利用实体间的并发分支汇聚行为互模拟方法进行状态约减。这种方法能有效地减少模型的复杂性，提高检验效率。通过对比状态约减前后的实验结果，证明了这种方法的有效性。论文针对现有的巷道瓦斯传感器部署标准，运用上述方法对实际部署方案进行建模和检验。通过考虑实体的并发行为，发现了一个潜在的瓦斯泄漏检测问题，即在并发事件发生时，某个包含分支巷的瓦斯部署模型可能存在漏检现象。这强调了在模型建立和检验过程中考虑实体并发行为的重要性。该论文贡献了一种结合实体交互和并发行为的时间自动机模型检验方法，用于提升煤矿瓦斯监测WSNs的可用性和安全性。这种方法不仅能够提高监测系统的效率，还能识别出潜在的安全隐患，对于保障煤矿安全生产具有重要意义。为了进一步提升实用性和自动化程度，作者指出需要开发自动建模机制，以简化模型建立过程。同时，论文的工作也为其他类似环境下的WSNs监测系统提供了借鉴和参考。