Shop : Details
Shop
Details
48,80 €ISBN 978-3-8440-4711-0Softcover166 pages226 g21 x 14,8 cmEnglishThesis
October 2016
Sebastian Biallas
Verification of Programmable Logic Controller Code using Model Checking and Static Analysis
This dissertation studies the formal methods model checking and static analysis to prove the correctness of Programmable Logic Controller (PLC) programs. For this, we developed the tool Arcade.PLC, which allow the automatic application of these methods to PLC programs written for different vendors. It extracts a model from the program by abstract simulation, which over-approximates the possible program behavior. The user is then able to verify whether the model obeys a specification, which can be written in the logic CTL or using automata.
For applying model checking, we demonstrate how the model can be extracted automatically, such that the approach scales to industrial size programs. For this, we develop different abstraction techniques. Further, we introduce a simplified formalism to write specifications, which is influenced by an automata-based language established in industry. We implement an algorithm to check programs using this formalism and show that this technique is even able to detect errors in the specification. Finally, we detail how counterexamples generated by the model checker can be analyzed automatically to locate the actual erroneous line in the program.
The static analysis we developed is able to detect program errors in a fully automatic way. We detect typical errors such as division by zero and illegal array accesses, but also PLC specific errors, e. g., during a restart. The analysis is based on a value-set analysis, which determines the values of all program variables in each program location. These sets are then verified against the predefined checks or user-provided annotations. We show how to implement this analysis such that it scales to industrial size programs. The approach is evaluated on an industrial case study.
For applying model checking, we demonstrate how the model can be extracted automatically, such that the approach scales to industrial size programs. For this, we develop different abstraction techniques. Further, we introduce a simplified formalism to write specifications, which is influenced by an automata-based language established in industry. We implement an algorithm to check programs using this formalism and show that this technique is even able to detect errors in the specification. Finally, we detail how counterexamples generated by the model checker can be analyzed automatically to locate the actual erroneous line in the program.
The static analysis we developed is able to detect program errors in a fully automatic way. We detect typical errors such as division by zero and illegal array accesses, but also PLC specific errors, e. g., during a restart. The analysis is based on a value-set analysis, which determines the values of all program variables in each program location. These sets are then verified against the predefined checks or user-provided annotations. We show how to implement this analysis such that it scales to industrial size programs. The approach is evaluated on an industrial case study.
Keywords: Formel Verification; Programmable Logic Controller; Model Checking; Static Analysis
Available online documents for this title
You need Adobe Reader, to view these files. Here you will find a little help and information for downloading the PDF files.
Please note that the online documents cannot be printed or edited.
Please also see further information at: Help and Information.
Please also see further information at: Help and Information.
| Document |  | Document | ||
| Type |  | |||
| Costs |  | 36,60 € | ||
| Action |  | Purchase in obligation and download the file | ||
| Document |  | Table of contents | ||
| Type | | |||
| Costs |  | free | ||
| Action |  | Download the file | ||
User settings for registered online customers (online documents)
You can change your address details here and access documents you have already ordered.
User
Not logged in
Shaker Verlag GmbH
Am Langen Graben 15a
52353 Düren
Germany
Am Langen Graben 15a
52353 Düren
Germany
Mon. - Thurs. 8:00 a.m. to 4:00 p.m.
Fri. 8:00 a.m. to 3:00 p.m.
Fri. 8:00 a.m. to 3:00 p.m.
Contact us. We will be happy to help you.
