Development of Automatic Program Verification for Continuous Function Chart based on Model Checking

The objective of this work is to develop the methods and a tool of automatic program verification for automation system by using the verification method that is widely used in computer science, i.e. model checking. As model checking is a formal method, it is necessary to have formal descriptions of the programs and the specifications. Therefore, the first approach of this work is to develop the formal descriptions regarding the programs and the specifications. Due to the major problem in model checking, which is the state-space explosion problem, the formalization of the programs and the specifications are strongly restricted. The second approach of this work is to develop the methods and a tool to generate the reasonable formal models and formal specifications to enable model checking as program verification method. In industrial plants such as refinery plant, power plant, or petrochemical plant, the implemented programs that represent plant’s operation procedures
are complex. To observe the applicability in an industrial context, the third approach of this work is to evaluate the pplicability of the methods and a tool of automatic program verification in industrial context. This is done by implementing the developed methods and a tool in a few of industrial case studies.