Verification of PLC Programs
Richard Šusta
Doctoral Dissertation Submitted to the Department of Cybernetics, Revised Edition - June 2003
View or download:
sustathesis.pdf (2 MB) Gzipped-Postscript sustathesis.ps.gz (1.6 MB) Zipped-Postscript sustathesis.ps.zip (1.6 MB) Abstract:
The main contributions are abstract PLC machine for modeling a wide range of binary PLCs (Programmable Logic Controllers), the new theory of transfer sets, and APLCTRANS algorithm that converts abstract PLC programs to logical formulas. The conversion runs in linear time in the size of PLC source code, at the most cases, though the converted program has an exponential complexity of its execution time. The completeness proof for modeling an abstract PLC by a Mealy's automaton is presented and APLCTRANS possibilities are demonstrate by the parallel decomposition of PLC program, by verifying absence of relay races in PLC, and by modeling PLC as a timed automata.BibTeX entry:
Text = Susta, R.: Verification of PLC Programs. PhD thesis, Revised edition, CTU-FEE Prague 2003.@phdthesis{RSustaVerification:2003,
Author = "Richard {\v S}usta",
Title = "Verification of {PLC} Programs",
School = "CTU-FEE Prague",
Pages = "151",
Note = "Revised edition",
Text = "{\v S}usta, R.: Verification of PLC Programs. PhD thesis, Revised edition, CTU-FEE Prague 2003.",
Year = "2003"
url = "http://dce.felk.cvut.cz/susta/publications/thesis.htm"
}