License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.06161.4
URN: urn:nbn:de:0030-drops-7084
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2006/708/
Go to the corresponding Portal

Kemper, Peter ; Tepper, Carsten

A Petri Net Approach to Verify and Debug Simulation Models

pdf-format:
06161.KemperPeter.Paper.708.pdf (0.2 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{kemper_et_al:DagSemProc.06161.4,
  author =	{Kemper, Peter and Tepper, Carsten},
  title =	{{A Petri Net Approach to Verify and Debug Simulation Models}},
  booktitle =	{Simulation and Verification of Dynamic Systems},
  pages =	{1--13},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6161},
  editor =	{David M. Nicol and Corrado Priami and Hanne Riis Nielson and Adelinde M. Uhrmacher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2006/708},
  URN =		{urn:nbn:de:0030-drops-7084},
  doi =		{10.4230/DagSemProc.06161.4},
  annote =	{Keywords: Discrete event simulation, verification, debugging, process interaction, Petri net analysis}
}

Keywords: Discrete event simulation, verification, debugging, process interaction, Petri net analysis
Collection: 06161 - Simulation and Verification of Dynamic Systems
Issue Date: 2006
Date of publication: 07.09.2006

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI