Automatic Synthesis of Distributed and Parameterized Systems

• Applicant: Privatdozent Dr.-Ing. Swen Jacobs
• Subject Area: Theoretical Computer Science
• Term: from 2015 to 2019
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 266796805

The goal of synthesis methods is to automatically construct systems that satisfy a given formal specification, relieving the designer from tedious and error-prone manual implementation of the low-level details of the system. Despite these benefits, formal methods that guarantee correctness a priori, like synthesis, have hardly found their way into the practice of system design, in contrast to a posteriori methods like verification. One reason for this is that the underlying computationalproblems are even harder than for verification. However, after the impressive recent advances in automated reasoning methods, research on synthesis has picked up again in recent years.A crucial research area that has received little attention is the synthesis of distributed systems of concurrently running processes. The growing importance of such systems, like multi-core processors, and communicating embedded devices or web services, has not been accordingly reflected in the research on synthesis methods for such systems. However, synthesis is particularly important for these systems, as the subtle interplay between separate components makes it notoriously hard to construct correct systems manually.This proposal aims at developing new methods and tools for the synthesis of distributed and parameterized systems, such as communication protocols with a given or even a parametric number of components. To this end, we will study approaches for the verification of distributed and parameterized systems, and generalize the underlying ideas to develop novel methods for the more difficult task of automatic synthesis. This will include the development of efficient methods for the distributed synthesis problem with finite-state components, reductions from parameterized to distributed synthesis, and methods for the synthesis of distributed infinite-state systems.The goal of this project is to develop new foundational methods for synthesis, and test the resulting approaches on small and medium-scale benchmark case studies. Our benchmark case studies include the ARM AMBA bus controller and cache coherence protocols. The AMBA controller has been used as a benchmark for existing synthesis tools, but has never been solved for a parametric number of components. Cache coherence protocols are a technically challenging case study, as the main goal here is to synthesize implementations which are not only correct, but also as efficient as possible. We will develop methods that can solve the parameterized synthesis problem for these and more complex case studies.

• DFG Programme: Research Grants