Methods and tools to the verification of safety-related control software

This paper gives a summary of a project which deals with methods for the proof of the demanded properties of user-written control software. Although these methods are based on formal methods they are covered with user-friendly interfaces. The document displays the modelling of a control system, which consists of a programmable logic controller (PLC), a user program and the environment. It demonstrates the description of the requirements for this system and it explains how we prove these requirements at the generated model