Skip to Main content Skip to Navigation
Journal articles

A Formal Definition Method of Denotational Semantics and Functions for PLC Program Language

Litian Xiao Ming Gu 1 Jiaguang Sun
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 : The correctness verification methods of PLC programs include software model checking and theorem proving, etc. The paper studies the definition of denotational semantics on PLC program language, which is convenient to PLC programs modeling and model checking. The purpose of work is the correctness verification on PLC programs by formal methods. Based on the extended λ-calculus definition, the paper has defined the configuration of PLC program architecture, denotational semantics of PLC programs and functions of denotational semantics. It is the basis of model checking and theorem proving.
Document type :
Journal articles
Complete list of metadata

https://hal.inria.fr/inria-00612407
Contributor : Hehua Zhang <>
Submitted on : Friday, July 29, 2011 - 5:02:02 AM
Last modification on : Monday, December 14, 2020 - 3:30:22 PM

Identifiers

  • HAL Id : inria-00612407, version 1

Collections

Citation

Litian Xiao, Ming Gu, Jiaguang Sun. A Formal Definition Method of Denotational Semantics and Functions for PLC Program Language. Journal of Central South University (in Chinese), Central South University, 2011. ⟨inria-00612407⟩

Share

Metrics

Record views

323