Formalization of sequential function chart as synchronous model in LUSTRE

Programmable Controllers (PLCs) are being increasingly used in safety-critical systems, which include control systems in Nuclear Power Plants. The reason lies in their ease of programming and configurability. Sequential function chart (SFC) has been adopted as a graphical language in the IEC 61131-3 standard because SFC model of control logic graphically represents the control flow of execution. Use of PLCs in control system performing safety/safety-related functions demands higher level of assurance of the correctness of software in these systems. Such assurance can be derived if there is a rigorous semantics of SFC language. Unfortunately, IEC 61131-3 standard does not provide a rigorous semantics. In this paper, we describe a rigorous semantics of SFC using the synchronous dataflow language LUSTRE. The paper also describes an automated scheme to translate SFC into LUSTRE. This facilitates formal verification of SFC model against its specifications.