ReVe for PLC
Regression Verification for Programmable Logic Controller Software
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.
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
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
Especially IC3 makes it feasible to prove the equivalence of the big example within the
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.
T describes further options or experiments within the case.
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.
The project is led by Prof. Bernhard
Beckert and Dr. Vladimir Klebanov. It is
part of the DFG Priority
Programme 1593 "Design for Future – Managed Software