Formalization and Verification of PLC Timers in Coq

Author

Wan, Hai ; Chen, Gang ; Song, Xiaoyu ; Gu, Ming

Author_Institution

Key Lab. for ISS of MOE, Tsinghua Univ., Beijing, China

Volume

1

fYear

2009

fDate

20-24 July 2009

Firstpage

315

Lastpage

323

Abstract

Programmable logic controllers (PLCs) are widely used in embedded systems. A timer plays a pivotal role in PLC real-time applications.The paper presents a formalization of TON-timers of PLC programs in the theorem proving system Coq. The behavior of a timer is characterized by a set of axioms at an abstract level. PLC programs with timers are modeled in Coq. As a case study, the quiz machine problem with timer is investigated. Relevant timing properties of practical interests are proposed and proven in Coq. This work unveils the hardness of timer modeling in embedded systems. It is an attempt of formally proving the correctness of PLC programs with timer control.

Keywords

programmable controllers; Coq; PLC timers; TON-timers; programmable logic controllers; quiz machine problem; Application software; Automata; Embedded software; Embedded system; Information science; Laboratories; Programmable control; Real time systems; Timing; USA Councils; Coq; Modeling; PLC; TON-Timer;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Software and Applications Conference, 2009. COMPSAC '09. 33rd Annual IEEE International

Conference_Location

Seattle, WA

ISSN

0730-3157

Print_ISBN

978-0-7695-3726-9

Type

conf

DOI

10.1109/COMPSAC.2009.49

Filename

5254244