Trace Analysis- Gain Insight through Modelchecking and Cycle Reduction ∗

Verification and validation of models are crucial steps to the success of a model-based development of systems. Traces are a common and powerful mean to document the dynamic behavior of a model and are generated from many sources, ranging from simulation engines to modelcheck-ers. In this paper, we describe techniques and correspond-ing tool support that helps a modeler to gain insight in the dynamic behavior of a complex model based on trace analy-sis. 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 interest and develop a novel technique to reduce the sequence of events leading to such states. The proposed techniques are implemented in Traviando, a stand alone tool with an open XML inter-face to import traces from many modeling environments, e.g., the APNN toolbox and Mobius among others. A sub-tle modeling error in a multi-class server system serves as an application example to illustrate the effectiveness of our approach in revealing the cause of an observed effect