Jacobs

In this project we want to establish Global Synchronization Protocols (GSPs) as a new computational model for concurrent systems with a parametric number of components. Besides local updates of a component, GSPs support synchronous global updates of the system, which may be guarded with global conditions on the state of the system. With this combination, they can be used to model applications that depend on global synchronization between components, e.g. by consensus or leader election, at an abstraction level that hides the internal implementation of the agreement protocol, while faithfully preserving its pre- and postconditions.We will identify conditions under which parameterized safety verification of GSPs remains decidable, even though this problem is in general undecidable for the combination of communication primitives that GSPs support. A preliminary version of GSPs already supports both global synchronization and global transition guards, and we plan to further extend the system model to include asynchronous message-passing and different extensions for fault tolerance, while preserving decidability of parameterized verification.Moreover, we will identify conditions for small cutoffs for safety verification, i.e., small bounds on the number of components that need to be considered to provide parameterized correctness guarantees. Based on these cutoffs, we will also develop an approach to automatically synthesize GSPs that satisfy given properties by construction. Finally, we will also investigate a refinement-based synthesis approach for GSPs and compare its properties to the cutoff-based approach.Our research into decidable fragments of GSPs will be guided by applications from different areas, such as sensor networks, robot swarms, or blockchain-based applications.

Funding Body

Funding Body

Deutsche Forschungsgemeinschaft (DFG)