Formale Entwicklung einer Steuerung für eine Fertigungszelle mit SYSYFOS
This work provides a formally verified solution for production cell control, though it appears incremental in applying existing synthesis methods to a specific domain.
The paper tackled the problem of developing a formally verified control system for a production cell by applying deductive synthesis, achieving a complete specification from informal requirements and demonstrating its applicability to hardware and mechanical systems.
Using the synthesis approach of Manna and Waldinger, a formally specified and verified control circuitery for a production cell was developped. Building an appropriate formal language level, we could achieve a requirements specification to the informal description. We demonstrated that the paradigm of deductive synthesis can be applied to the development of complete verified systems, including hardware and mechanics. We defined two domain-specific logical operators that schematise frequent patterns in specification and proof and hence allow a more concise and expressive presentation. In Burghardt (1995), an english short version of this paper, without appendices, can be found.