Dependability analysis of logic controller based on formal verification procedures

Dependability of an automation system requires engineers to implement formal verification procedures in order to eliminate the causes of hazardous conditions. These conditions may vary from case to case and will jeopardize the dependability of manufacturing lines and operators. Therefore, dependability analysis of the control systems to check the possibility of state transitions from safe to unsafe states, for instance, is essential. Formal verification by using model checking procedure is proven as an effective method and widely used in practice for automatic verification of correctness properties against a finite model of a system. Therefore, in the present paper, we introduce a novel method of model checking for logic control design. A Binary Decision Diagram (BDD) based model checking method is used to analyze and design a dependable controller that meets the requirement of certain properties, defined by specified predetermined functions