Publication
Modular Verification of Programmable Logic Controllers with TLA
Andreas Wolpers; Werner Stephan
In: Gérard Morel; Francois B. Vernadat (Hrsg.). INCOM '98 Workshop on Formal verification for Automation Engineering. IFAC Symposium on Information Control in Manufacturing (INCOM), Pages 121-126, 1998.
Abstract
With the increasing use of computers in manufacturing, the quality of the production
process becomes increasingly dependent on the software used in these systems.
This paper describes the use of Lamport’s Temporal Logic of Actions (TLA) for the modular
verification of programmable logic controllers (PLCs). First, a way to formulate abstract
specifications for function blocks as defined in IEC 1131 is suggested. Based on these abstract
specifications, the verification of systems consisting of many function blocks in a modular
way is explained.