A Petri Net Approach to Verify and Debug Simulation Models

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.