Title :
A Formal Semantics of PLC Programs in Coq
Author_Institution :
INRIA, Tsinghua Univ., Beijing, China
Abstract :
Programmable logic Controllers (PLC) are embedded systems that are widely used in industry. We propose a formal semantics of the Instruction List (IL) language, one of the five programing languages defined in the IEC 61131-3 standard for PLC programing. This semantics support a significant subset of the IL language that includes on-delay timers. We formalized this semantics in the proof assistant Coq and used it to prove some safety properties on an example of PLC program.
Keywords :
embedded systems; instruction sets; programmable controllers; programming language semantics; set theory; theorem proving; Coq; IEC 61131-3 standard; PLC programs; embedded systems; formal semantics; instruction list language; programing languages; programmable logic controllers; proof assistant; safety properties; subset; Delay; IEC standards; Industries; Registers; Safety; Semantics; Strontium; Coq; Instruction List; PLC; SSReflect; formal semantics;
Conference_Titel :
Computer Software and Applications Conference (COMPSAC), 2011 IEEE 35th Annual
Conference_Location :
Munich
Print_ISBN :
978-1-4577-0544-1
Electronic_ISBN :
0730-3157
DOI :
10.1109/COMPSAC.2011.23
