A formal semantics of PLC programs in Coq

Sidi Ould Biha 1, *
* Auteur correspondant
1 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
Résumé : 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.
Type de document :
Communication dans un congrès
IEEE. IEEE Computer Software and Applications, COMPSAC'11, Jul 2011, Munich, Germany. 2011
Liste complète des métadonnées

Littérature citée [11 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00601906
Contributeur : Sidi Ould Biha <>
Soumis le : mardi 21 juin 2011 - 08:05:59
Dernière modification le : jeudi 11 janvier 2018 - 06:22:29
Document(s) archivé(s) le : vendredi 9 novembre 2012 - 16:45:30

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00601906, version 1

Collections

Citation

Sidi Ould Biha. A formal semantics of PLC programs in Coq. IEEE. IEEE Computer Software and Applications, COMPSAC'11, Jul 2011, Munich, Germany. 2011. 〈inria-00601906〉

Partager

Métriques

Consultations de la notice

148

Téléchargements de fichiers

390