A Novel Approach Of Groebner Bases Computation For Safety Analysis Of Distributed Discrete Controllers

It is well known that Programmable Logic Controller (PLC) related processes in manufacturing lines are safety-critical systems because of the increasing number of embedded functions and features. Any failure of these process control systems might not only result in a significant financial loss but also lead to casualties as well. Therefore, it is essential to determine control system safety in advance by verifying the possibility of state transitions from safe to unsafe states at the design and development stage. To overcome these issues, many researchers and engineers have been involved in formal methods research. One of the favorite topic is the formal verification via model checking, which is to verify whether a mathematical model of a system meets the formal specification that describes the property to be checked. In this research, our main objective is to generate a new model checking computation method based on Groebner bases algorithm for safety property analysis of distributed discrete controllers. There are several phase involved to achieve the objective, including fundamental study of distributed discrete model, system modeling based on Finite State Machine (FSM) requirement, and also the development of model checking computation tool. Model checking procedure will be conducted by simulation and experiment and the results will be analyzed and evaluated. Several performance comparison with other conventional model checking tools also will be conducted to evaluate its computational efficiency. This research also proposes the improvement of mean time to failure (MTTF) by using the new model checking method. At the end of this research, a complete tool of model checking method based on Groebner bases algorithm for safety verification will be produced. The new model checking tool is expected to significantly reduce labor and maintenance cost of manufacturing companies, thus improves productivity