Skip to Main content Skip to Navigation
Conference papers

A Refinement-Based Validation Method for Programmable Logic Controllers

Hai Wan 1 Xiaoyu Song 1 Gang Chen 2 Ming Gu 1 
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 : Programmable logic controllers (PLCs) are widely used in computer-based industrial applications. Timers play a pivotal role in PLC real-time embedded system applications. The paper addresses the formal validation of PLC systems with timers in the theorem proving system Coq. The timer behavior is characterized formally. A refinement validation methodology is presented in terms of an abstract model and a concrete model. The refinement is calibrated by a mapping relation. The soundness of the methodology is shown in the proving system. An illustrative case study demonstrates the eectiveness of the approach.
Document type :
Conference papers
Complete list of metadata

Cited literature [8 references]  Display  Hide  Download
Contributor : Hai Wan Connect in order to contact the contributor
Submitted on : Tuesday, March 8, 2011 - 7:00:23 AM
Last modification on : Friday, February 4, 2022 - 3:08:27 AM
Long-term archiving on: : Thursday, June 9, 2011 - 2:17:26 AM


Files produced by the author(s)


  • HAL Id : inria-00516014, version 1



Hai Wan, Xiaoyu Song, Gang Chen, Ming Gu. A Refinement-Based Validation Method for Programmable Logic Controllers. The 10th International Conference on Quality Software, Jul 2010, Zhangjiajie, Hunan, China. ⟨inria-00516014⟩



Record views


Files downloads