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.
Type de document :
Communication dans un congrès
The 10th International Conference on Quality Software, Jul 2010, Zhangjiajie, Hunan, China. 2010
https://hal.inria.fr/inria-00516014
Contributeur : Hai Wan
<>
Soumis le : mardi 8 mars 2011 - 07:00:23
Dernière modification le : mardi 17 avril 2018 - 11:30:09
Document(s) archivé(s) le : jeudi 9 juin 2011 - 02:17:26
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. 2010. 〈inria-00516014〉
