Specification of technical plant behavior with a safety-oriented technical language

Manual reconfiguration of existing systems is a common task for engineers. Especially, the modernization of plants depends on an unambiguous and reliable documentation. Furthermore, the well defined specification of plant behavior enables the engineer to verify the control software with a model checking tool. In order to be able to provide the description correctly and without misunderstandings, it should be done formally. Temporal logics, like the computation tree logic, offer an ideal solution for this purpose. However, they are based on a complex theory. In order to use them anyway in practice, the formal expressions have to be developed by automated procedures out of an intuitively understandable description. This contribution proposes a text-block based method, which enables the user to create such a formal specification by the use of a safety-oriented technical language.