Formalization of sequential function chart as synchronous model in LUSTRE
Emerging Trends and Applications in Computer Science（2012）
摘要
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.
更多查看译文
关键词
IEC standards,control engineering computing,parallel languages,program verification,programmable controllers,programming language semantics,safety-critical software,visual languages,IEC 61131-3 standard,LUSTRE,PLC,SFC language,SFC model,configurability,control logic,control system,execution control flow,formal verification,formalization,graphical language,nuclear power plant,programmable controller,programming,safety-critical system,safety-related functions,semantics,sequential function chart,software correctness,synchronous dataflow language,synchronous model,Formalization,IEC 61131-3 Language,PLC formal verification,Sequential Function Chart,Synchronous model,
AI 理解论文
溯源树
样例
生成溯源树，研究论文发展脉络
Chat Paper
正在生成论文摘要