Dissertation (Metadata)
Title:Software Verification for Programmable Logic Controllers
Author:Ralf Huuck
Faculty:Faculty of Engineering
DDC:004 Computer science
Date of thesis defense:2003-04-17
Referent:Prof. Dr. Yassine Lakhnech
second reviewer(s) :Prof. Dr. Willem-Paul de Roever, Dr. habil. Oded Maler, Prof. Dr. Thomas Wilke
Description (original):Programmable logic controllers (PLCs) occupy a big share in automation control. Their programming languages are, however, born out of historical needs and do not comply to state-of-the art programming concepts. Moreover, programming is mostly undertaken by the designers of the control systems. In sum this adds to the creation of erroneous software and, even more, unsafe control systems. In this work we focus on the software verification aspects for PLCs. For two selected programming languages, Sequential Function Charts (SFC) and Instruction List (IL) we discuss semantic issues as well as verification approaches. For SFCs we develop a model checking framework while for IL we suggest static analysis techniques, i.e., a combination of data flow analysis and abstract interpretation. Several case studies corrobate our approach.
(translated):keine dt.-spr. Zusammenfassung
Keywords:Sequential Function Charts ; Model checking ; Instruction List Software Verification, Programmable Logic Controllers, Sequential Function Charts, Instruction List, Model-checking, Abstract interpretation, Data Flow Analysis, Embedded Systems, Control Systems, Semantics
Speicherprogrammierte Steuerung ; Semantik ; Verifikation ; Statische Analyse
d726.pdf (980 kB)    generate ZIP   details >>