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) Seiten 121-126 1998.


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. (gz, 56 KB )

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence