Abstract

Plants are a long-term and expensive investment, additionally, they need to be adapted to the market and technology process. The plant evolves by changing of hardware and software components. A evolution step can introduce defects in the plant workflow. How can we find such introduction of defects in view of the high safety claim of plants? In this master thesis we apply regression verification on two version of automation software, to prove the equivalence or to find divergence in the software behaviour.

Publications

Please refer to the project's publication page.

Software

We provide our software for generating SMV of PLC software as open source via github. The repository lies at github: areku/structuredtext. As the repository is currently set to private, access is only granted upon request.

If you have questions, feel free to get in touch with Mattias Ulbrich or Alexander Weigl. You are allowed to extend or modify the software under the terms of GPL 3.

For running generated SMV in a sophisticated manner, you should take NuXMV. Especially IC3 makes it feasible to prove the equivalence of the big example within the PPU case study.

Results

We evaluated our approach with the Pick and Place (PPU) case study ‐ designed and developed by the AIS at TUM.

The notion of the investigated cases X.Y+T is as follows. X is the base revision and Y the update or new revision to be checked against, e. g. 03.05 is the proof of equivalence between scenarios 3 and 5 of the PPU. The tag T describes further options or experiments within the case.

1. TA ‐ Timer Abstraction OP ‐ Exclusion of metallic workpieces OM ‐ Exclusion of plastic workpieces PM ‐ Physical Model used

For a detailed explanation of the results, please refer to chapter 4.2, p. 68 in Alexander Weigl's master thesis.