Abstract
| 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 Computer Society |
| 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 | Spain |
| City | Zaragoza |
| Period | 25/06/17 → 30/06/17 |
| Internet address |
Fingerprint
Keywords
- benchmark generation
- property preservation
- verification
- model checking
- modal transition systems
Cite this
}
Property-Preserving Generation of Tailored Benchmark Petri Nets. / Bernhard, Steffen; Jasper, Marc; Meijer, Jeroen; van de Pol, Jaco.
17th International Conference on Application of Concurrency to System Design - ACSD 2017: 25-30 June 2017, Zaragoza, Spain : proceedings. Piscataway, NJ : IEEE Computer Society, 2017.Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review
TY - GEN
T1 - Property-Preserving Generation of Tailored Benchmark Petri Nets
AU - Bernhard, Steffen
AU - Jasper, Marc
AU - Meijer, Jeroen
AU - van de Pol, Jaco
N1 - (Invited Paper)
PY - 2017/6
Y1 - 2017/6
N2 - 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.
AB - 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.
KW - benchmark generation
KW - property preservation
KW - verification
KW - model checking
KW - modal transition systems
U2 - 10.1109/ACSD.2017.24
DO - 10.1109/ACSD.2017.24
M3 - Conference contribution
SN - 978-1-5386-2868-3
BT - 17th International Conference on Application of Concurrency to System Design - ACSD 2017
PB - IEEE Computer Society
CY - Piscataway, NJ
ER -