论文部分内容阅读
随着计算机越来越多的应用于工业生产中,尤其是以DCS和PLC控制系统为代表的计算机控制系统的广泛应用。而且计算机控制系统常用于高温高压等临界控制当中。那么计算机控制系统的安全性就越来越引起人们的注意,在这其中逻辑控制因为其在设计过程中极有可能存在错误,所以更加是保证安全的重中之重。在计算机控制系统正式应用于生产过程前,必须要做安全分析和安全测试,保证逻辑控制的安全性。传统的人工安全测试方法,根据安全条件逐条设计试验,十分消耗时间和资源,而且测试结果也不能保证覆盖了所有的工况下的安全性。所以虽然逻辑控制安全问题在世界范围内越来越受到重视,但是目前并没有成熟和实用的方法。因此,开展逻辑控制的安全测试技术的研究具有重要的实用意义。模型检测技术是一种形式化验证技术,该技术在时序电路设计和通讯协议设计的验证领域得到了广泛的应用。模型检测技术能够高效、自动并完全地对软件进行安全性分析。因此针对逻辑控制的安全性检测的问题,本文主要对基于形式化模型检测技术的逻辑控制的安全性检验进行研究,完成了以下工作：1.首先说明了形式化模型检测的应用背景以及发展状况,提出了基于模型检测的逻辑控制安全性检验的一般应用框架。2.说明逻辑控制进行安全检验前的建模过程,提出了针对控制对象中包含连续变量而采取的离散建模的原则和方法。3.说明了形式化描述安全性质的方法,提出针对逻辑控制的安全属性描述方法。4.选取适合于逻辑控制的模型检测工具。针对带连续变量的过程,采用了符号化模型检测工具SMV对其安全性分析；对于含有时间约束的控制过程,采用了自动机模型检测工具UPPAAL对其安全性分析。5.对有无时间约束的逻辑控制的安全检验分别举例验证。模型检测方法对逻辑控制的状态全覆盖,完全自动搜索的过程,既保证了逻辑控制的全覆盖检测避免微小错误存在,又是自动检测过程大大减少了人力物力的消耗。本文最后使用这两种检测工具分别进行的实例检测过程,结果证明这两种检测方法适用于逻辑控制的安全性检测。如果将模型检测技术应用于逻辑控制的验证和安全性分析,那么检测技术在逻辑控制安全性分析方面必会有良好的发展前景。