Software Verification for Programmable Logic Controllers

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.