Submitted: June 2008
Abstract
Simulation is one method of composing models to observe the behaviour of a system. It has been, and is still used widely both in the industry and research fields to provide insight into a system and a basis to make decisions for problems related to the system. MoDeST is a powerful specification language developed by Formal Methods and Tools research group at the University of Twente. The objective of bringing on this language is to analyse the behaviour of a system by either doing model checking to asses functional correctness or simulation to establish reliability whilst providing both stochastic and nondeterministic features. With this thesis, we want to develop a simulator for MoDeST models based on the tool Motor, which was written to make analyzing and evaluating MoDeST specifications possible.
Our simulator is implemented in C++ language by modifying and creating new modules in Motor. The main purpose is that the user can observe the state of the MoDeST model from time to time and solve nondeterministic transitions manually if needed. Implementing interpreter for MoDeST/Motor is the main part of this project in order to be able to traverse the model tree correctly and to collect data for analyzing. The most deciding aspect of a simulation is the randomness, since it has a big role in modeling the system itself and in solving nondeterminism in the simulation. MoDeST supports three important distributions: Uniform, Normal and Exponential. While Uniform distribution is essential for the other distributions but easy to implement, it is a challenge to find a way of implementing random number generator for Normal and Exponential distributions which is both reliable and fast. For this part we used the improved Ziggurat method of Marsaglia and Tsang, which has been proven to be very fast for decreasing densities.
Another challenge in implementing the simulator is designing the clock advancing scenario, as clock is an important feature is MoDeST. The key phrase here is maximum time advance, that is to advance the clocks in a certain state as far as possible such that the environment—apart from the clocks’ value—stays the same.