Research On Modeling, Decomposition, And Verification Techniques For Collaborative Industrial Control Systems

With the deepening of the country's industrialization development process,Industrial Control Systems,as a kind of process control systems,have been more and more widely used in all walks of life.Since an industrial control system can have a direct influence on the physical world through various actuators,its wrong operation may lead to serious safety accidents,resulting in great economic losses,casualties,and even major environmental disasters.Therefore,their functional correctness,safety,and reliability must be strictly guaranteed before they are formally put into operation.In the current work of ensuring the functional correctness of industrial control systems,the methods of simulation at the design stage and testing after implementation are mainly adopted.However,using simulation and testing methods can hardly conduct an in-depth and comprehensive investigation of system behaviors,especially for systems with complex behaviors,it is difficult to provide a complete and strict guarantee.Therefore,some researchers try to introduce formal verification technology.However,due to the high application threshold of formal verification technology,its practical application is not extensive.Moreover,due to some deficiencies in the current formal verification technology,most of the existing work only focuses on the verification of a single functional module or program,rather than the verification of the entire industrial control system with multiple tasks.Moreover,with the development of controller technology and network technology,the industrial control systems have gradually developed from simple single-controller control systems to multi-controller distributed industrial control systems,field bus industrial control systems,and even collaborative industrial control systems based on industrial Ethernet.Their complexity is increasing day by day,and their functional correctness assurance will face greater challenges.The past methods will become more difficult to apply.Therefore,in order to improve the capability of ensuring the functional correctness of modern industrial control systems,this thesis proposes two functional safety assurance methods for collaborative industrial control systems from the aspects of design methods and verification methods.Firstly,a set of modeling and decomposition methods are proposed to support centralized modeling of control functions of complex industrial control systems and automatic decomposition under specific resource constraints,so as to help users design collaborative industrial control systems with complex interaction relationships from a global perspective,thus avoiding errors that may be introduced in the manual design process.Secondly,a user-friendly lightweight formal property verification method is proposed to facilitate users to quickly inspect the properties of the implemented industrial control system.In particular,it has unique advantages in the verification of complex control systems because it works based on system operation logs.With the assistance of the functional correctness assurance methods in these two aspects,engineers can develop reliable collaborative industrial control systems more efficiently.In terms of innovative work,it specifically includes the following four parts:1.A modeling language named CICSML supporting the description of the collaborative relationship and the equipment resource constraint relationship isproposed to support the unified abstract modeling of control functions of collaborative industrial control systems.This language takes into account thecharacteristics of industrial controller software described in the IEC 61131-3standard and draws lessons from the syntax of structured text programminglanguage.It has a direct correspondence with the software implementationof the industrial control system and can be easily converted into specificimplementation codes.2.On the basis of the modeling language,a model decomposition method under specific equipment resource constraints is proposed.This decomposition method can automatically decompose a single controller complex systemmodel into a set of subsystem models of multiple controllers according to equipment resource constraints.These subsystem models collaborate throughautomatically generated interaction mechanisms and share given equipment resources,thus forming a multicontroller collaborative industrial controlsystem.3.A lightweight verification method for formal properties of collaborative industrial control systems is proposed,which mainly combines simulation technology of industrial control programs and specification mining technology tochange the verification process of formal properties from active to passive,thus greatly reducing the threshold for formal verification of complex industrial control systems.4.In addition,a linear temporal logic with past specification mining method isproposed to improve the expressiveness of the target property specificationand further enhance the lightweight property verification method.