Skip to Main content Skip to Navigation
Journal articles

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

Litian Xiao 1 Ming Gu 2 Jiaguang Sun 3
2 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.
Document type :
Journal articles
Complete list of metadata
Contributor : Hehua Zhang <>
Submitted on : Friday, July 29, 2011 - 5:17:58 AM
Last modification on : Wednesday, June 2, 2021 - 3:39:58 AM


  • HAL Id : inria-00612409, version 1



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⟩



Record views