Research On Safety Verification Techniques For Logic Control

Computers are used more and more widely in industrial production. Particularly DCS and PLC control systems are becoming more and more commonly used. Computer control systems are used in the control of high temperature and pressure. The safety of computer control system is attracting more and more attention. Logic control program, which tend to involve errors in its designing process, is one of the most important issues in safety assurance. Software must be analyzed and tested to ensure the safety of the control software before a computer control system being used in a production process. Traditional manual safety testing methods, which are based on verifying safety conditions manually, is both time-and resource-consuming, and their test results can not guarantee covering all the system conditions. The control software safety issue is attracting more and more attention in the literature, but there hasn’t being mature and practical approach to solve the problem. It is of practical importance to conduct research on test technologies of control software safety.Model checking is a formal method verification technology. It is widely used in the design of sequential circuit and the verification of communication protocol. Model checking technology is efficient, automatic and complete. This paper introduce the study on control software safety tests based on formal model checking, and completes the following work:1. Illustrate the background and application of formal model checking. Proposed a framework of the logic control safety based on model checking.2. Illustrate the modelling process of logic control software for safety verification. Propose the principles and methods of discrete model for continuous variables.3. Illustrate the formal description of safety specification. Propose the formal description of safety specification for control logic.4. Select the appropriate logic control software model checking tool. Symbolic model checking tool SMV is chosen to verify the safety of a process with continuous variables in it. Timed automata model checking tool UPPAAL is chosen to verify safety of the process with time constraints. 5. Time-constraints and None-constraints experiments on verifying safety of logic control software are carried out respectively.Model checking of logic control includes state-wide coverage and fully automated search process, and both of them is to ensure complete coverage of control software testing to identify small errors. The verification is an automatic verification process, which greatly reduces the consumed manpower and material resources. Finally, experiments on verifying safety of logic control software are carried out respectively, and the results show that the two verification methods can be used to verify the safety of logic control. If model checking technology is used in the verification and safety analysis of logic control, then the detection of logic control software in the safety analysis may have good prospects for development.