| As the core of key infrastructure such as transportation,energy,and advanced manufacturing,the Industrial Control Systems(ICS)are regarded as an important part of the national security strategy.With the in-depth development of national industrial manufacturing intelligence,on the one hand,the increasingly complex functional requirements and interactive environment make the safety of the system more difficult.The failure of ICS can cause serious damage to life,the environment,property,etc.in the physical world.On the other hand,Cyber-Physical Systems,as the core architecture of Industry 4.0,exhibit many advantages such as flexibility,convenience,and efficiency.Therefore,more and more traditional ICS are attracted to join the “Industrial Internet” in order to open up “Information Islands”,increase production capacity,and enhance industry competitiveness.Intuitively,ICS require almost strict behavioral correctness.The increasing complexity of software functions and the transition from a “physically isolated” local environment to an “open” network environment poses enormous challenges to system safety.In the face of the increasingly complex and open system development trend,the traditional testing and simulation approaches to improve the correctness of ICS are not conducive to finding highly concealed defects and may be accompanied by huge economic costs.Therefore,as one of the key technologies for developing high-confidence software,formal methods have received great attention from academia and industry.Most of the existing research studies statically verify the stock code.When the function of the system is complicated,the complexity of the general static method will also increase,and there is a lack of mechanical support for decomposing complex systems,so it brings a large economic cost.At the same time,for coded programs,finding major flaws late in development is likely to result in high repair costs and even forced abandonment of the system.From the perspective of deployment,if there are situations in the production environment that conflict with the correctness assumptions in the model,such as malicious attacks,it is difficult to provide effective protection.However,in the existing research on runtime verification,external monitoring is mainly used,and the real-time performance and self-healing capability are inevitably restricted by many factors such as communication environment,synchronization mechanism,and electrical characteristics.Therefore,this paper focuses on the ICS following the IEC 61131 international specification,and it studies the system safety assurance covering the stages of design,development,test verification,and field running.It mainly includes model design and verification,code generation,property mining,and runtime verification.First,based on the formal language supporting the refined relationship,a model construction and verification approach related to the ICS domain is proposed,which effectively ensures the consistency of the design model and the requirements specification.Then,the corresponding industrial control program code is generated from the refined specific model,so as to avoid errors that may be introduced in the manual coding process and improve the development efficiency.Next,based on the static verification technology acting on the source code,a program property mining method is proposed,which can further guide us to analyze,repair,iterate,and strengthen the system software.Finally,in order to ensure system safety in the production environment,a non-intrusive runtime dynamic verification method is proposed,and the code-insensitive,localized,and incremental verification mechanism is used to improve its universality,real-time,and efficiency.It aims to enhance the key capabilities of the operating system,such as monitoring and diagnosis,real-time protection,and self-healing.The main contributions of this paper are as follows:· Corresponding to the design and development stage of the software life cycle,based on the Event-B formal language and refinement characteristics,a modeling and verification method for ICS is proposed,which provides a general-purpose model framework that supports discrete-time properties and includes firmware layer,configuration layer,and business layer.On the one hand,the refinement mechanism is used to decompose the complex system,making it suitable for modeling complex functions.On the other hand,through the consistency verification of the design model and the requirement specification,the correctness of the system design process can be effectively guaranteed,so as to detect system defects as early as possible and reduce the risk of repairing major problems later.· After constructing the concrete business layer model,an automatic method is proposed to generate code from the model.The generated industrial control program conforms to the IEC 61131-3 international standard.Using the method of code generation can better ensure the consistency of the model and the program,so as to avoid errors that may be introduced in the manual coding process,and improve the development efficiency.· Corresponding to the testing and verification stage,a property mining method for industrial control program code is proposed.This method uses the cycle invariant,satisfiability modulo theory,classical machine learning algorithm,and refined relationship to statically verify user properties and try to further explore stronger property descriptions,which are used to guide the further process of the system,such as analysis,repair,iteration,and reinforcement.· Corresponding to the running stage in the production environment,a non-intrusive method of runtime verification of ICS is proposed.On the one hand,it provides a specific language for describing the nature specifications of the industrial control field.On the other hand,it implements a code-insensitive,localized,and incremental verification mechanism to improve universality,real-time,and efficiency,thereby enhancing the system's important capabilities in real-time safety protection and dynamic repair. |
PDF Full Text Request