When quoting this document, please refer to the following
URN: urn:nbn:de:0030-drops-7084
Go to the corresponding Portal

Kemper, Peter ; Tepper, Carsten

A Petri Net Approach to Verify and Debug Simulation Models

06161.KemperPeter.Paper.708.pdf (0.2 MB)


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

  author =	{Peter Kemper and Carsten Tepper},
  title =	{A Petri Net Approach to Verify and Debug Simulation Models},
  booktitle =	{Simulation and Verification of Dynamic Systems},
  year =	{2006},
  editor =	{David M. Nicol and Corrado Priami and Hanne Riis Nielson and Adelinde M. Uhrmacher},
  number =	{06161},
  series =	{Dagstuhl Seminar Proceedings},
  ISSN =	{1862-4405},
  publisher =	{Internationales Begegnungs- und Forschungszentrum f{\"u}r Informatik (IBFI), Schloss Dagstuhl, Germany},
  address =	{Dagstuhl, Germany},
  URL =		{},
  annote =	{Keywords: Discrete event simulation, verification, debugging, process interaction, Petri net analysis}

Keywords: Discrete event simulation, verification, debugging, process interaction, Petri net analysis
Seminar: 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