Safety Property Comparison Between Grobner Bases and BDD-based Model Checking Method

Implementation of verification procedures is required to eliminate design errors that decrease the safety of an automation system. 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 paper, we introduce a method of model checking technique for logic control design. A checking procedure based on Grobner bases (GB) model is used to analyze and design a controller that meets the requirements defined by a predetermined safety function. We compare our proposed method with symbolic computation tree logic (CTL) model checking based on binary decision diagrams (BDDs). We implemented this technique to a case study by using a crane system.