Verification of Sequential Function Charts Using SMV.
Sébastien Bornot, Ralf Huuck, Ben Lukoschus · 2000
Sequential function charts (SFCs) are defined as a modeling language in the IEC 1131-3 standard [1] and can be used to structure and drive programmable logic controllers (PLCs). It includes interesting concepts as hierarchy, history variables and priority. As the typical application area of this language is the control of industrial processes, it is obvious that safety and reliability is a crucial goal for systems using SFCs. In this work we give an abstract formal model for SFCs and present a method to automatically verify properties concerning the safety of such systems using the model checking tool SMV (Symbolic Model Verifier) [2, 3]. Keywords: programmable logic controllers, sequential function charts, hierarchy, model checking, SMV 1 Introduction The market for industrial process control and instrumentation has been continuously and rapidly growing within the last ten years and is expected to grow further in the future. Programmable logic controllers (PLCs) are the backbone of...