In this paper, we describe a novel technique that helps a modeler gain insight into the dynamic behavior of a complex stochastic discrete event simulation model based on trace analysis. We propose algorithms to distinguish progressive from repetitive behavior in a trace and to extract a minimal progressive fragment of a trace. The implied combinatorial optimization problem for trace reduction is solved in linear time with dynamic programming. We present and compare several approximate and one exact solution method. Information on the reduction operation as well as the reduced trace itself helps a modeler to recognize the presence of certain errors and to identify their cause. We track down a subtle modeling error in a dependability model of a multi-class server system to illustrate the effectiveness of our approach in revealing the cause of an observed effect. The proposed technique has been implemented and integrated in Traviando, a trace analyzer to debug stochastic simulation models.

Performance trees are a recently-proposed mechanism for the specification of performance properties and measures. They represent an attractive alternative to stochastic logics, since they support traditional stochastic model checking queries, while also allowing for the direct extraction of a wide range of quantitative measures. In this paper we illustrate differences in expressiveness between performance trees and continuous stochastic logic (CSL), and present quantitative semantics showing the mathematical basis underlying performance tree operators. As a running example, we demonstrate performance query specification with performance trees on a stochastic Petri net model of a healthcare system.

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.

Verification and validation of simulation models are cru- cial steps to the success of a simulation project. Traces are a common and powerful mean to document the dynamic be- havior of a model and are generated by most simulation engines. In this paper, we describe techniques and cor- responding tool support that helps a modeler to gain in- sight in the dynamic behavior of complex simulation models based on trace analysis. We propose to visualize traces by message sequence charts. We use a common modal logic, namely the linear time logic (LTL), to identify states of int er- est and a pattern system to make specification of formulas more productive. The proposed techniques are implemented in Traviando, a stand alone tool with an open XML interface to import traces from various modeling environments, e.g., the APNN toolbox, the ProC/B toolset and Mobius.

Discrete event simulation is broadly applied in the analysis of dynamic and concurrent systems and often with complex and detailed models. The process of creation and coding a non-trivial simulation model is error prone and the identification and understanding of what really goes on in a simulation run needs adequate tool support for making verification, validation and debugging productive. This holds in particular for the analysis of simulation traces, a powerful debugging aid with the challenge of large amounts of data. In this paper, we present Traviando, a trace visualizer and analyzer from Dortmund university

A major problem in modelling and subsequent simulation of process-oriented systems (ProC/B models), is the functional correctness of the model. Therefore a model should be first analysed for its functional correctness before it is analysed by simulation. Petri nets are well suited for model based and state based functional analysis, but are often not adequate or not used for the specification of process models. We present in this paper a transformer for an automatic mapping from ProC/B models onto PNs. The resulting PN-models can be analysed with PN-algorithms and the results from the PN-analysis can be interpreted at the ProC/B level.

Process interaction is a well known paradigm to formulate simulation models. In practice, complex models of interacting processes require substantial effort in the verification and validation phase of a simulation study. A simulator trace can document all activities performed in a simulation run. In this paper, we present two visualization aids to investigate the dynamic behavior of a simulation model based on traces. The first approach animates the graphical model description to visualize a trace in the same language as used to specify the model itself. The second approach employs a variant of message sequence charts or sequence diagrams to give an orthogonal illustration of interacting processes that generate the dynamic behavior. Both approaches have been implemented and evaluated. We consider a particular process-oriented modeling formalism, the ProC/B notation, and its corresponding tool, the ProC/B Toolset, that have been developed for the modeling and analysis of logistics networks.

A 1,2,3,4-tetrahydroisoquinoline having smooth muscle relaxant activity of the formula: wherein R1 and R2 are each hydrogen or lower alkyl and X is -O- or -S-, and pharmaceutically acceptable salts thereof.

This paper presents algorithms and experimental results for model-checking continuous-time Markov chains (CTMCs) based on a structured analysis approach. In this approach, a CTMC is represented as a term in Kronecker algebra that reflects the component structure of the system model. Such representations can be obtained in a natural way from various high-level specification formalisms, such as stochastic extensions of Petri nets, process algebras or activity networks. Properties are expressed in continuous stochastic logic (CSL) which includes means to express transient, steady-state and path performance measures. This paper describes novel model-checking algorithms for CSL that fully exploit the compositional description of the CTMC. This yields an effective way to combat the state-space explosion problem and enables the model-checking of fairly large Markov chains. Furthermore, we show how state-space aggregation (modulo bisimulation) and the elimination of vanishing states can be done in a component-wise manner. To demonstrate the applicability of the approach, and to assess the efficiency of our algorithms, we analyze a stochastic Petri net-model of a workstation cluster system and a simple queuing network.