Verification and validation of logic control systems by model checking

From a simple electronic devices to replace sophisticated electro-mechanical relays, nowadays PLCs are extensively used in industrial automation field and they are integrated into much larger environment, capable of almost any type of control applications, including motion control and instrumentation. It is well known that PLC related processes in manufacturing lines are safety-critical systems because of the increasing number of embedded functions and features. These are beneficial for engineers since they can design and develop sophisticated and complex control programs up to the best of their knowledge and capabilities. On the other hand, this introduces a potential safety risk; thus, their effects on system reliability need to be investigated more thoroughly. Moreover, any failure of these control systems might not only result in a significant financial loss but lead to casualties as well. Hence, their actual programming and the correctness of the programs play a vital role. Manufacturing automation is facing strong demands for high reliability of process control systems. These include the flexibility and safety requirements in order to improve the performance of machines and equipments in manufacturing lines. For example, prior to the commissioning of new machines or production lines, it is necessary to ensure that the designed control programs will not violate any previously determined control specifications. In other words, appropriate preventive actions should be taken in advance so that the process runs in a safe system configuration; thus, avoiding additional corrective procedures due to unsafe or failures of operations. Formal verification of correctness of a property (i. e. deadlock freeness) in a system follows the steps which are; identify the properties that need to be verified, build an abstract model of the system (including the surrounding environment), identify the parts of the systems that are interesting, and mathematically show that the property always holds in the region of interest. Even more interesting is that when having all this information, beside verification one can even compute a correct "solution". The formal verification process is nowadays plays an important role in industrial automation complex problem solving. Implementation of verification procedures is required to eliminate design errors that decrease the safety of automation systems. Design errors may vary from case to case but will certainly jeopardize the safety of manufacturing lines and operators. Therefore, checking the possibility of state transitions in the control systems from safe to unsafe states is essential. Formal verification via model checking procedures has proven to be efficient and is widely used. System finite element models are employed to automatically verify certain correctness properties. In this study, we propose a novel method of model checking for logic control design. A checking procedure based on Gr ? bner bases (GB) model is used to analyze and design a controller that meets the requirements defined by a predetermined safety function. We compare the proposed method with symbolic computation tree logic (CTL) model checking based on binary decision diagrams. A crane system is used as a case study. In addition, we compare the computational efficiency of the methods and present counterexamples by unsafe conditions. Our works presented in the thesis deal with safety design and verification and validation (V&V) of logic control systems that are widely used in manufacturing processes. Two methods, one is a proposed method of Gr ? bner bases computation and the other is conventional BDD-based model checking, are used to verify the safety of the designed controller, by using predetermined safety properties based on known hazardous states of a logic control system. The model checking based on Gr ? bner bases computation is our novel work that uses algebraic approach, compare to BDD-based model checking that proposes symbolic computations. We also carry out verification of other temporal properties, such as reachability, liveness and fairness evaluation by using the BDD-based model checking approach. We perform a number of experiments to validate the safety of designed controllers using an arm pick-and-place model, considered as two types of control systems, which are a two cranes system and a nondeterministic arm pick-and-place system. Performance analysis on computational complexity between both verification methods is also thoroughly discussed. Furthermore, we introduce a formal modeling and verification of PLC nondeterministic behavior with ladder diagram (LD) implementation. We provide an illustrative example by using an arm pick-and-place model and design the LD program for the arm, with application of a timer ON and timer OFF function blocks. The nondeterministic behaviors are configured from an arm grip condition and also from the logical formalism of both timers properties. By applying several logical properties to the arm model, we verify the deterministic and nondeterministic behaviors and illustrate experimental results for validation of arm safe operation. This work contributes to safety verification and validation of an arm pick-and-place operationa model nondeterministic behaviors, model verification using logical properties with inclusion of nondeterministic behaviors from state operation and timer function, and application of the timer OFF function block for safety experiments and implementation liveness property check