基于体系结构模型检查分布式控制系统

Model Checking Distributed Control Systems Based on Software Architecture

分布控制系统是大量硬件设备通过计算机系统得以控制和协调的高度复杂系统,它们也是任务关键的系统,需要保障其功能的高度正确性和可靠性.分析复杂控制系统的过程包含了证明或验证设计的系统确实满足某种需求.但由于系统的复杂度,有效分析系统是相当困难的.从系统设计和分析的角度看,基于体系结构方法可以运用层次化构造和抽象的方法来减小模型复杂度.模型检查技术是分析复杂系统构造满足正确和可靠性需求的有效方法.结合软件体系结构描述方法和模型检查技术,提出了基于体系结构的分布式控制系统形式分析方法,通过楼宇综合控制系统实例研究,展示了该方法在提高分布式控制系统设计质量方面的效果.

Distributed control systems are a category of high complex systems that include a large number of devices controlled and harmonized by computer systems. Their reliability and functional correctness always need to be guaranteed as their mission-critical feature. The analysis process for complex control systems consists of proving or verifying that the designed system indeed meets certain specifications. However, both the design and analysis may be formidable due to the complexity and magnitude of the system. From an analysis perspective, the complexity of a system can be reduced by imposing a hierarchical structure and abstraction on the architectural design. Currently, model checking is demonstrated by more and more successes. It is an effective way to verify that the construction of a complex system satisfies to the requirements of reliability and correctness. An approach for formally analyzing distributed control systems at architectural level by applying software architecture description and model checking techniques is presented. Through study on a building comprehensive control system, it is shown that the method could improve the quality of design of distributed control systems.