基于时间自动机的时序约束活动异常监测系统形式化验证

摘要

物联网被认为是继计算机、互联网和移动通信网络之后的第三次信息产业浪潮。物联网通过传感设备获取“物”信息，并通过网络实现信息交换，以实现智能化识别、定位、跟踪监控和管理的目的。基于物联网的车间生产过程异常状态监控系统越来越多，这类系统通过采集生产车间的数据并进行分析处理，以实现车间智能化管理从而提高企业的经济利益。但在生产车间监控系统中，参与信息交互的对象包含人、机、物等不同类型对象，系统需要处理的是大量结构异质的信息，同时随着车间规模的扩大，监控也变得更加复杂，无法保证监控系统投入运行之前完全符合设计要求。因此，提出一种车间生产监控系统建模和验证方法，在系统实施之前使用形式化方法对生产车间监控系统建模并验证，尽早发现系统设计的不合理和不正确之处，显得尤为必要。
　　本文以物联网环境下离散生产车间异常监测系统为研究背景，研究了基于时间自动机的时序约束活动异常监测系统形式化验证方法，利用时间自动机验证方面的优势验证监测系统设计的有效性和完备性。本文首先综述了复杂事件检测的国内外研究现状；分析了生产车间现场的若干特征，定义了基于时间自动机的生产车间现场模型，用状态不变式中的时间约束刻画操作人员等的自主随机性，用状态和变迁分别刻画不同类型的活动，同时对生产对象的感知行为抽象表示；然后说明了不同的事件使用策略和消耗策略建模方法，分析了事件和事件约束模型构造方法，并提出了复合事件模式采用若干时序相关事件操作符的时间自动机模型构造方法，其中提出了控制模型时间自动机建模方法，控制模型减小了一个事件模式对应自动机模型的规模；接着为了简化异常监测时间自动机模型性质验证，建立了包含正常生产情况的辅助生产过程自动机模型；针对生产车间异常监控系统的特点，提出从系统功能性、实时性、冗余性及未定义的异常行为四个方面验证系统设计的正确性和完备性；最后使用时间自动机验证工具UPPAAL，以粘合加工车间异常监测为例，对提出的方法进行了验证。
　　本文的研究表明：时间自动机形式化方法能够较好刻画生产车间异常监测系统的相关特性。利用时间自动机形式化建模及验证方法，能够有效发现监测系统潜在的问题，并在一定程度上辅助监测系统的开发设计，并为相关人员提供有效改进依据。实验结果证明本文提出的方法有一定应用价值和参考意义。

目录

声明

1 绪论

1.1 研究背景

1.2 问题及研究现状

1.3 研究目的和意义

1.4 论文的组织结构

2 生产车间的时间自动机模型

2.1 时间自动机理论及UPPAAL介绍

2.2 生产车间特征分析

2.3 基于时间自动机的生产车间模型

2.4 本章小结

3 基于时间自动机的异常监测系统建模

3.1 复杂事件处理

3.2 事件操作符及事件使用策略

3.3 原子事件建模

3.4 复合事件建模

3.5 本章小结

4 异常监测事件模式验证

4.1 仿真分析

4.2 辅助生产过程模型构建

4.3 异常监测时间模式形式化验证

4.4 本章小结

5 生产车间案例研究

5.1 案例介绍

5.2 案例时间自动机模型构建

5.3 案例模型验证及结果分析

5.4 本章小结

结论

参考文献

攻读硕士学位期间发表学术论文情况

致谢