License
When quoting this document, please refer to the following
URN: urn:nbn:de:0030-drops-7084
URL: http://drops.dagstuhl.de/opus/volltexte/2006/708/
Go to the corresponding Portal


Kemper, Peter ; Tepper, Carsten

A Petri Net Approach to Verify and Debug Simulation Models

pdf-format:
Document 1.pdf (211 KB)


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:DSP:2006:708,
  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 =		{http://drops.dagstuhl.de/opus/volltexte/2006/708},
  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 Published by LZI