Specification and verification of technical plant behavior with symbolic timing diagrams

The specification of technical plant behavior is vitally important. It forms the basis for the draft of hardware and software and it serves the creation of documentation. Furthermore, the specification enables the engineer to verify the control software with a model-checking tool. In order to be able to provide the description of behavior 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 graphic-based method, which enables the user to create such a formal specification by the use of Symbolic Timing Diagrams.