Property-Preserving Generation of Tailored Benchmark Petri Nets
Bottleneck of the validation and evaluation of analysis and verification tools for distributed systems is the shortage of benchmark problems. Specifically designed benchmark problems are typically artificial, rare, and small, and it is difficult to guarantee challenging properties of realistic benchmarks. This talk will show how to systematically construct arbitrarily complex Petri Nets with guaranteed safety properties. Key to our construction is a top-down parallel decomposition based on lightweight assumption commitment specifications. We will discuss this approach, its current limitations, possible extensions, and envisioned application scenarios along a number of concrete examples.