2026-07-20T05:25:18Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:708 2024-03-06T11:06:50Z ddc:004 open_access

A Petri Net Approach to Verify and Debug Simulation Models Kemper, Peter Tepper, Carsten Discrete event simulation verification debugging process interaction Petri net analysis Verification and Simulation share many issues, one is that simulation models require validation and verification. In the context of simulation, verification is understood as the task to ensure that an executable simulation model matches its conceptual counterpart while validation is the task to ensure that a simulation model represents the system under study well enough with respect to the goals of the simulation study. Both, validation and verification, are treated in the literature at a rather high level and seem to be more an art than engineering. This paper considers discrete event simulation of stochastic models that are formulated in a process-oriented language. The ProC/B paradigm is used as a particular example of a class of simulation languages which follow the common process interaction approach and show common concepts used in performance modeling, namely a) layered systems of virtual machines that contain resources and provide services and b) concurrent processes that interact by message passing and shared memory. We describe how Petri net analysis techniques help to verify and debug a large and detailed simulation model of airport logistics. We automatically derive a Petri net that models the control flow of a Proc/B model and we make use of invariant analysis and modelchecking to shed light on the allocation of resources, constraints among entities and causes for deadlocks. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Peter Kemper and Carsten Tepper 2006 Is Part Of Dagstuhl Seminar Proceedings, Volume 6161, Simulation and Verification of Dynamic Systems (2006) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DagSemProc.06161.4 urn:nbn:de:0030-drops-7084 https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06161.4 eng https://creativecommons.org/licenses/by/4.0/legalcode