Property-Preserving Generation of Tailored Benchmark Petri Nets

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

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    13 Citations (Scopus)
    281 Downloads (Pure)

    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
    Number of pages8
    ISBN (Electronic)978-1-5386-2867-6
    ISBN (Print)978-1-5386-2868-3
    DOIs
    Publication statusPublished - Jun 2017
    Event17th International Conference on Application of Concurrency to System Design, ACSD 2017 - Zaragoza, Spain
    Duration: 25 Jun 201730 Jun 2017
    Conference number: 17
    http://pn2017.unizar.es/program/provisional-program-acsd-2017/

    Conference

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

    Keywords

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

    Fingerprint

    Dive into the research topics of 'Property-Preserving Generation of Tailored Benchmark Petri Nets'. Together they form a unique fingerprint.

    Cite this