Research On Verification Of Industrial Control Programs Written In IEC 61131-3 Structured Text Language

With the development of automation technology,Industrial Control System(ICS)has been widely used in industry,energy,transportation,water conservancy,etc.It plays an important role in national infrastructures that are directly related to people's daily life,especially in safetycritical areas such as nuclear facilities,the aerospace industry.The control software for ICS has to undergo rigorous testing to ensure its quality and safety.However,the increased scale and complexity of the software make testing more difficult.Moreover,the limitations of testing(such as it cannot guarantee to detect all hidden bugs nor to reveal the error of logic)make it not ideal for safety-critical areas.Rather,formal verification like model checking can prove the correctness of the implementation.It thus has become a popular choice for verifying software amongst safety-critical areas.IEC 61131-3 is an international standard for programming languages of ICS's control software.Structured Text(ST)is a textual high-level programming language provided by IEC61131-3.It allows developers to use a rich set of data structures like arrays and structs,and of control structures like branches,loops and subroutine calls.It is thus widely used in developing control programs with complex logic or algorithms.With the deep integration of industrialization and informatization,ST is required more and more.Therefore the verification of ST programs matters.To meet the growing demand,in this paper,we propose a model checking based verification approach for ST programs.Firstly we define a formal model(called BM,Behavior Model)to describe the run-time behaviors of ST programs including the cyclic scanning execution.Then we give a formal modelling method on source code level,which can model an ST program to a BM.And we design an algorithm to check linear temporal logic properties on BM.To improve the efficiency of modelling,we define the formal operational semantics of ST and thus have achieved the automation of the modelling and verifying processes.Finally,we implement a prototype verification tool based on the proposed approach.The availability of the tool has been shown by the verification of a real-world industrial application.