148 articles – 163 Notices  [english version]

inria-00612409, version 1

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

Litian Xiao, Ming Gu a, 1, Jiaguang Sun a, 2

Communications in Computer and Information Science 176(II), 40-46 (2011)

Résumé : 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.

  • a –  Tsinghua University / Beijing
  • 1 :  FORMES (LIAMA)
  • INRIA – Tsinghua University / Beijing – LIAMA
  • 2 :  School of Software (THSS)
  • Tsinghua University
  • Domaine : Informatique/Génie logiciel
 
  • inria-00612409, version 1
  • http://hal.inria.fr/inria-00612409
  • oai:hal.inria.fr:inria-00612409
  • Contributeur : Hehua Zhang <>
  • Soumis le : Vendredi 29 Juillet 2011, 05:17:58
  • Dernière modification le : Mercredi 10 Août 2011, 06:00:07