Swen Jacobs: Verification and Synthesis of Parameterized Systems

In this talk, I will present an overview of our work on model checking and synthesis of reactive systems that are composed of a parametric number of (finite-state) components. The starting point is the parameterized synthesis approach, which is based on cutoff results that reduce reasoning about parametric systems to reasoning about systems of bounded size. I will show how we extended existing cutoff results for token-passing systems to more general systems and specifications, and how we applied the parameterized synthesis approach with these extensions to obtain correct-by-construction implementations of the AMBA AHB protocol for an arbitrary number of communicating components.