随着国家在工业化发展进程上的不断深入,工业控制系统作为一种过程控制系统,被越来越广泛地应用于各行各业之中。由于工业控制系统通过各类执行机构能够对物理世界产生直接影响,其错误的运行将可能导致严重的安全事故,继而造成较大的经济损失、人员伤亡乃至重大的环境灾难。因此,在正式投入运行之前,其功能正确性、安全性及可靠性必须得到严格的保障。在当前的工业控制系统功能正确性保障工作中,主要采用的还是在设计阶段进行仿真以及在实现后进行测试的方法,但仿真与测试方法难以对系统行为进行深入而全面的考察,尤其对于具备复杂行为的系统,很难提供完备而严格的保障。因此,部分学者尝试引入形式化验证技术。但由于形式化验证技术具有较高的使用门槛,其实际应用并不广泛。且由于目前形式化验证技术存在一定的不足,大多数的现有工作都只关注了单个功能模块或程序的验证,而无法对多个任务协同的工业控制系统整体进行验证。而且,伴随着控制器技术、网络技术的发展,工业控制系统逐步从简单的单控制器控制系统发展为多控制器的分布式工业控制系统、现场总线工业控制系统乃至基于工业以太网的协作式工业控制系统,其复杂性日益提升,其功能正确性保障工作将面临更大的挑战,过去的方法将变得更加难以适用。因此,为了提高现代工业控制系统的功能正确性保障能力,本论文针对协作式工业控制系统,从设计方法及验证方法两方面,提出了两项功能安全性保障方法。首先提出了一套建模、分解方法,支持复杂工业控制系统的控制功能集中建模与特定资源约束条件下的自动分解,帮助用户以全局视角设计具备复杂交互关系的协作式工业控制系统,从而避免人为设计过程中可能引入的错误;其次提出了一种用户友好的轻量级形式化性质验证方法,从而方便用户对实现后的协作式工业控制系统进行快速性质考察;特别地,由于其基于系统运行日志的工作特性,在复杂控制系统的验证方面具有独特的优势。通过这两方面的功能正确性保障方法的辅助,工程师可以更加高效地开发出可靠的协作式工业控制系统。在创新性工作方面,具体包括了以下四个部分:1.提出了一种支持协作关系描述以及设备资源约束关系描述的建模语言CICSML,以支持协作式工业控制系统控制功能的统一抽象建模。该语言考虑了IEC 61131-3标准中描述的工业控制器软件特性,借鉴了结构化文本编程语言的语法,与工业控制系统软件实现存在较为直接的对应关系,可以轻松地转换为具体的实现代码。2.在建模语言的基础之上,提出了一种特定设备资源约束下的模型分解方法。该分解方法能够将单控制器复杂系统模型,按照给定设备资源约束,自动分解为多控制器的简单子系统模型集合。这些子系统模型通过自动生成的交互机制进行协作,共享给定的设备资源,从而形成多控制器协同的协作式工业控制系统。3.提出了一套轻量级的协作式工业控制系统形式化性质验证方法,主要结合工业控制程序仿真技术及规范挖掘技术,将形式化性质的验证过程从主动变为被动,从而极大地降低了复杂工业控制系统形式化性质验证的门槛。4.另外,提出了一种带过去时态的线性时态逻辑规范挖掘方法,改善了目标性质规范的表达能力,进一步增强了该轻量级性质验证方法。