Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

H. Zhang, S. Merz, and M. Gu, Specifying and Verifying PLC Systems with TLA+, 2009 Third IEEE International Symposium on Theoretical Aspects of Software Engineering, pp.293-294, 2009.
DOI : 10.1109/TASE.2009.43
URL : https://hal.archives-ouvertes.fr/hal-00516785

H. Wan, G. Chen, X. Song, and M. Gu, Formalization and Verification of PLC Timers in Coq, 2009 33rd Annual IEEE International Computer Software and Applications Conference, 2009.
DOI : 10.1109/COMPSAC.2009.49
URL : https://hal.archives-ouvertes.fr/inria-00516011

A. Mader, A Classification of PLC Models and Applications, WODES 2000: 5th Workshop on Discrete Event Systems, pp.21-23, 2000.
DOI : 10.1007/978-1-4615-4493-7_24

G. Frey and L. Litz, Formal methods in PLC programming, SMC 2000 Conference Proceedings. 2000 IEEE International Conference on Systems, Man and Cybernetics. 'Cybernetics Evolving to Systems, Humans, Organizations, and their Complex Interactions' (Cat. No.00CH37166), pp.2431-2436, 2000.
DOI : 10.1109/ICSMC.2000.884356

M. Younis and G. Frey, Formalization of existing PLC programs: A survey, Proceedings of CESA, pp.234-0239, 2003.

N. Vöker and B. J. Kräer, Automated verification of function blockbased industrial control systems, Science of Computer Programming, vol.42, issue.1, pp.101-113, 2002.

B. J. Krämer and N. Völker, A Highly Dependable Computing Architecture for Safety-Critical Control Applications, Real-Time Systems, vol.13, issue.3, pp.237-251, 1997.
DOI : 10.1007/978-1-4757-6463-5_2

B. Lukoschus, Compositional verification of industrial control systems , methods and case studies, 2005.

A. Wolpers and W. Stephan, Modular verification of programmable logic controllers with TLA, " in INCOM '98 Workshop on Formal verification for Automation Engineering, G. Model and ois B. Vernadat Franc, pp.121-126, 1998.