Verifying functional and non-functional properties of manufacturing control systems

Verification of control software is usually not applied in industrial practice because of additional work expenses and missing theoretical background that is necessary to apply this technique. Therefore, this contribution presents an integrated approach to verify functional and a subset of non-functional properties of manufacturing control systems. To support the user in creating a well-defined but also understandable specification of plant behavior, two approaches are introduced that specify functional requirements with Symbolic Timing Diagrams and non-functional ones with a Safety-Oriented Technical Language. These behavior descriptions are then translated to temporal logic formulas to perform model-checking of the closed-loop system of plant and controller.