Specifying and verifying PLC systems with TLA+
Programmable Logic Controllers (PLCs) are widely used in industry for embedded systems. PLCs operate following a so-called scan cycle mechanism that starts with inputting, then performs computations, and finally outputs the results. PLC systems become more and more complex, so formal methods are important to be applied to ensure the correctness. TLA+ is a formal specification language, which was de signed for specifying and reasoning about concurrent and reactive systems. It is based on the Temporal Logic of Actions TLA, a dialect of linear-time temporal logic, and on Zermelo-Frankel set theory for representing data struc tures. TLA+ can formulate both system behaviors and their properties in a single logic formalism. We report on a method for specifying and verifying PLCs in TLA+. Our specification separates the description of the environment from that of the controller itself; its structure is consistent with the PLCs scan cycle mechanism, and specifications can be parameterized. The structuring mechanisms of TLA+ help to obtain clear, well organized, and configurable specifications, finite instances of which can be verified by the TLA+ model checker TLC.
Hehua Zhang Stephan Merz Ming Gu
Dept. CST Tsinghua University Beijing, P.R.China INRIA Nancy-Grand Est & Loria Nancy, France School of Software Key Lab for ISS of MOE Tsinghua University Beijing, P.R.China
国际会议
天津
英文
293-294
2009-07-29（万方平台首次上网日期，不代表论文的发表时间）