Synthesis of Reactive Systems
Jens Regenberg
Software development generally implies three phases, design, implementation, and verification. As the separation of implementation and verification is timeconsuming and effortful, both phases can be replaced by an automated synthesis development phase. The problem of distributed synthesis is to examine whether for a specification and an architecture there exists an implementation that meets the specification. ReaSyn is a tool, which examines for a given architecture and specification whether the underlying distributed system is realizable and creates an according program. Existing theoretical approaches were implemented: ReaSyn constructs and solves distributed games [MW03] in order to generate an optimized PROMELA program. Finally, ReaSyn is evaluated with respect to experimental results and possible extensions are discussed.
Diploma Thesis.