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.
Type de document :
Article dans une revue
Journal of Central South University (in Chinese), Central South University, 2011
Liste complète des métadonnées

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

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

204