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.
https://hal.inria.fr/inria-00516014 Contributor : Hai WanConnect 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
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⟩