Property-Preserving Generation of Tailored Benchmark Petri Nets

Steffen Bernhard, Marc Jasper, Jeroen Meijer, Jaco van de Pol

  • 3 Citations

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 languageEnglish
Title of host publication17th International Conference on Application of Concurrency to System Design - ACSD 2017
Subtitle of host publication25-30 June 2017, Zaragoza, Spain : proceedings
Place of PublicationPiscataway, NJ
PublisherIEEE Computer Society
Number of pages8
ISBN (Electronic)978-1-5386-2867-6
ISBN (Print)978-1-5386-2868-3
DOIs
StatePublished - Jun 2017
Event17th International Conference on Application of Concurrency to System Design, ACSD 2017 - Zaragoza, Spain

Conference

Conference17th International Conference on Application of Concurrency to System Design, ACSD 2017
Abbreviated titleACSD
CountrySpain
CityZaragoza
Period25/06/1730/06/17
Internet address

Fingerprint

Petri nets
Decomposition
Specifications

Keywords

  • benchmark generation
  • property preservation
  • verification
  • model checking
  • modal transition systems

Cite this

Bernhard, S., Jasper, M., Meijer, J., & van de Pol, J. (2017). Property-Preserving Generation of Tailored Benchmark Petri Nets. In 17th International Conference on Application of Concurrency to System Design - ACSD 2017: 25-30 June 2017, Zaragoza, Spain : proceedings Piscataway, NJ: IEEE Computer Society. DOI: 10.1109/ACSD.2017.24

Bernhard, Steffen; Jasper, Marc; Meijer, Jeroen; van de Pol, Jaco / Property-Preserving Generation of Tailored Benchmark Petri Nets.

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: Scientific - peer-reviewConference contribution

@inbook{2970b2c688b84909b2d78315bdf4e0f7,
title = "Property-Preserving Generation of Tailored Benchmark Petri Nets",
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.",
keywords = "benchmark generation, property preservation, verification, model checking, modal transition systems",
author = "Steffen Bernhard and Marc Jasper and Jeroen Meijer and {van de Pol}, Jaco",
note = "(Invited Paper)",
year = "2017",
month = "6",
doi = "10.1109/ACSD.2017.24",
isbn = "978-1-5386-2868-3",
booktitle = "17th International Conference on Application of Concurrency to System Design - ACSD 2017",
publisher = "IEEE Computer Society",
address = "United States",

}

Bernhard, S, Jasper, M, Meijer, J & van de Pol, J 2017, Property-Preserving Generation of Tailored Benchmark Petri Nets. in 17th International Conference on Application of Concurrency to System Design - ACSD 2017: 25-30 June 2017, Zaragoza, Spain : proceedings. IEEE Computer Society, Piscataway, NJ, 17th International Conference on Application of Concurrency to System Design, ACSD 2017, Zaragoza, Spain, 25-30 June. DOI: 10.1109/ACSD.2017.24

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: Scientific - peer-reviewConference contribution

TY - CHAP

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

ER -

Bernhard S, Jasper M, Meijer J, van de Pol J. Property-Preserving Generation of Tailored Benchmark Petri Nets. In 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. Available from, DOI: 10.1109/ACSD.2017.24