ReVe for PLC
Regression Verification for Programmable Logic Controller Software
AbstractPlants 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.
PublicationsPlease refer to the project's publication page.
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 Evolution".