基于实体交互模型巷道瓦斯监测WSNs的可用性检验
鲍宇1
赵亮2
陈树召2
陆翔2
朱紫维3
1.中国矿业大学计算机科学与技术学院,江苏徐州221116;矿山数字化教育部工程中心,江苏徐州2211162.中国矿业大学矿业工程学院,江苏徐州2211163.中国矿业大学计算机科学与技术学院,江苏徐州221116
摘要：若煤矿瓦斯监测WSNs(Wireless Sensor Networks)系统的功能设计忽略了被监测实体的交互行为,会造成WSNs本身可靠而被监测实体的安全不满足情况,这在生产安全中是非常危险的.为检验WSNs监测系统功能设计的可靠性和可用性,利用时间自动机模型检验方法建立WSNs监测系统模型,检验WSNs系统的可靠性.然后,根据传感器与环境实体间的交互关系,分析煤矿中多个实体的并发行为,提出了监测WSNs与被监测实体交互并发行为的时间自动机模型和可用性性质描述的建立方法,从监测功能设计角度,将被监测实体的安全并入WSNs监测生产安全的功能性质,然后用模型检验方法进行机器检验,保障了监测系统的可用性.对含有并发结构的实体模型,利用分支行为等价构建并发时间自动机模型,再利用实体间的并发分支汇聚行为互模拟的方法,进行了并发行为模型的状态约减,并通过互模拟等价证明了该方法的正确性.状态约减前后的实验对比表明该方法提高了检验效率.最后,对现行巷道中瓦斯传感器的部署标准,利用该方法对其中的实际部署方案进行建模并检验,在模型中考虑实体的并发行为,发现在并发事件发生时,其中一个含支巷的瓦斯部署模型存在一个潜在的瓦斯泄露漏检问题.利用实体建模的模型检验方法需要建立自动建模机制,以提高该方法的实用性.
关键词：无线传感器网络模型检测时间自动机瓦斯传感器部署UPPAAL
分类号：TD76(矿山安全与劳动保护)TP39(计算技术、计算机技术)
资助基金：国家自然科学基金(51204185)国家自然科学基金(51574222)基础研究项目(KC17073)
论文发表日期：2020-02-28
在线出版日期：2025-08-15（本平台首次上网日期，不代表文献的发表时间）
页数：9( 836-844 )
英文信息