Verification of PLC Properties Based on Formal Semantics in Coq

Jan Olaf Blech Sidi Ould Biha 1
1 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
Abstract : Programmable Logic Controllers (PLC) are widely used in embedded systems for the industrial automation domain. We propose a formal semantics of two languages defined in the IEC 61131-3 standard for PLC programming. The first one is the Instruction List (IL) language, an assembly like language. The second one is the Sequential Function Charts (SFC) language, a graphical high-level language that allows to describe the main control-flow of the system. A PLC system description may comprise SFC and IL code. We formalized the semantics in the proof assistant Coq. Furthermore, we present an associated tool for automatically generating SFC representations from a graphical description - the text based IL code can be handled in Coq directly - and its usage for verification purposes. We demonstrate our approach to prove safety properties of a PLC in a real industrial demonstrator.
Type de document :
Communication dans un congrès
International Conference on Software Engineering and Formal Methods, SEFM 2011, Nov 2011, Montevideo, Uruguay. 2011
Liste complète des métadonnées

https://hal.inria.fr/inria-00601907
Contributeur : Sidi Ould Biha <>
Soumis le : mardi 21 juin 2011 - 08:16:28
Dernière modification le : mercredi 10 octobre 2018 - 14:28:09

Identifiants

  • HAL Id : inria-00601907, version 1

Collections

Citation

Jan Olaf Blech, Sidi Ould Biha. Verification of PLC Properties Based on Formal Semantics in Coq. International Conference on Software Engineering and Formal Methods, SEFM 2011, Nov 2011, Montevideo, Uruguay. 2011. 〈inria-00601907〉

Partager

Métriques

Consultations de la notice

298