A formal semantics of PLC programs in Coq

International audienceProgrammable 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.Programmable logic Controllers (PLC) sont des systèmes embarqués qui sont largement utilisés dans l'industrie. Nous proposons dans ce papier une sémantique formelle du langage Instruction List (IL), l'un des cinq langages de programmation défini dans la norme IEC 61131-3 pour la programmation des PLC. Cette sémantique prend en charge un sous-ensemble important du langage IL qui comprend les timers on-delay. Nous avons formalisé cette sémantique dans le système Coq et nous l'avons utilisé pour prouver certaines propriétés de sûreté sur un exemple de programme PLC