The Denotational Semantics Definition of PLC Programs Based on Extended λ-Calculus

Litian Xiao Ming Gu 1 Jiaguang Sun 2
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 : PLC is widely used in the field of automatic control. The correctness verification methods of PLC programs include software model checking and theorem proving, etc. To use formal methods verifying the correctness of PLC programs, denotational semantics needs to define and then PLC programs can be modeled, model checking and verified. Based on the extended λ-calculus definition, the paper has researched and defined the architecture and denotational semantics of PLC programs. The work is the basis of model checking and theorem proving for correctness verification on PLC programs.
Type de document :
Article dans une revue
Communications in Computer and Information Science, Springer Verlag, 2011, Advanced Research on Computer Education, Simulation and Modeling, 176(II) (40-46)
Liste complète des métadonnées

https://hal.inria.fr/inria-00612409
Contributeur : Hehua Zhang <>
Soumis le : vendredi 29 juillet 2011 - 05:17:58
Dernière modification le : vendredi 25 mai 2018 - 12:02:06

Identifiants

  • HAL Id : inria-00612409, version 1

Collections

Citation

Litian Xiao, Ming Gu, Jiaguang Sun. The Denotational Semantics Definition of PLC Programs Based on Extended λ-Calculus. Communications in Computer and Information Science, Springer Verlag, 2011, Advanced Research on Computer Education, Simulation and Modeling, 176(II) (40-46). 〈inria-00612409〉

Partager

Métriques

Consultations de la notice

185