Translation-based model checking for PLC programs

Min Zhou 1 Fei He 1, 2 Ming Gu 1, 2 Xiaoyu Song 3
2 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
Abstract : In this paper, we focus on modeling and verification of PLC systems, which are widespread in industry and manufacture. Our approach is based on a translation procedure from PLC programs to timed automata. The resulting model consists of several kinds of modules. Besides of the main module which depicts the behaviors of the PLC programs, a dedicated module is constructed to be accord with the cyclical running mode of PLC systems, and another module is involved for specifying the environment behaviors. After all modules constructed, the model checker Uppaal is adapted to perform the model checking. Experimental results show promising performance of our approach. Comparing to existing approaches, extensive instructions are supported in this paper, including not only the time-related instructions, such as timer and counter, but also the subroutine and interruption instructions. In addition, the structure of whole model is more compact, and the translation procedure is more efficient, which results in a reduced verification model.
Type de document :
Communication dans un congrès
33rd Annual IEEE International Computer Software and Applications Conference, Jul 2010, Seattle, Washington, United States. 2009
Liste complète des métadonnées

https://hal.inria.fr/inria-00497123
Contributeur : Fei He <>
Soumis le : vendredi 2 juillet 2010 - 14:53:38
Dernière modification le : jeudi 11 janvier 2018 - 06:22:29

Identifiants

  • HAL Id : inria-00497123, version 1

Collections

Citation

Min Zhou, Fei He, Ming Gu, Xiaoyu Song. Translation-based model checking for PLC programs. 33rd Annual IEEE International Computer Software and Applications Conference, Jul 2010, Seattle, Washington, United States. 2009. 〈inria-00497123〉

Partager

Métriques

Consultations de la notice

196