Dissertation (Metadata)
Title:Software Verification for Programmable Logic Controllers
 
Author:Ralf Huuck
 
URN:NBN:urn:nbn:de:gbv:8-diss-7260
 
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
 
Documents:
d726.pdf (980 kB)    generate ZIP   details >>