Abstract
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 paper shows 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 illustrate how a specific strategy for design choices, which may well be automated, leads to benchmarks that grow exponentially with the number of its parallel components, and that are very difficult to verify. In particular, we will report numbers from a systematic sequence of concrete corresponding verification attempts using today's leading verification technology.
Original language | English |
---|---|
Title of host publication | 17th International Conference on Application of Concurrency to System Design - ACSD 2017 |
Subtitle of host publication | 25-30 June 2017, Zaragoza, Spain : proceedings |
Place of Publication | Piscataway, NJ |
Publisher | IEEE |
Number of pages | 8 |
ISBN (Electronic) | 978-1-5386-2867-6 |
ISBN (Print) | 978-1-5386-2868-3 |
DOIs | |
Publication status | Published - Jun 2017 |
Event | 17th International Conference on Application of Concurrency to System Design, ACSD 2017 - Zaragoza, Spain Duration: 25 Jun 2017 → 30 Jun 2017 Conference number: 17 http://pn2017.unizar.es/program/provisional-program-acsd-2017/ |
Conference
Conference | 17th International Conference on Application of Concurrency to System Design, ACSD 2017 |
---|---|
Abbreviated title | ACSD |
Country/Territory | Spain |
City | Zaragoza |
Period | 25/06/17 → 30/06/17 |
Internet address |
Keywords
- benchmark generation
- property preservation
- verification
- model checking
- modal transition systems