DocumentCode
3480292
Title
A Formal Semantics of PLC Programs in Coq
Author
Biha, Sidi Ould
Author_Institution
INRIA, Tsinghua Univ., Beijing, China
fYear
2011
fDate
18-22 July 2011
Firstpage
118
Lastpage
127
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Computer Software and Applications Conference (COMPSAC), 2011 IEEE 35th Annual
Conference_Location
Munich
ISSN
0730-3157
Print_ISBN
978-1-4577-0544-1
Electronic_ISBN
0730-3157
Type
conf
DOI
10.1109/COMPSAC.2011.23
Filename
6032332
Link To Document