Abstract

The simulation business is a business in which expensive simulators are used to train people in a certain field of expertise. A simulator performs this task by simulating the real world and stimulating the trainee as would happen in the real world. Due to the (high) level of imitation, the trainee behaves (and becomes conditioned) as he would in the real environment thus learning the required skills.

Often a group of simulators are connected to extend the training possibilities. These connected simulators allow training that is impossible in "stand-alone" simulators. Examples are tactical training and training involving a great deal of (in)direct human-human interaction. Computer generated entities with which the trainee has to cope cannot be compared with the behavior of real humans.

When simulators are connected the importance of certain (technical) aspects like protocol, latency and mutual exclusion become more evident. To cope with these general problems in a unified way, standards are devised. Examples are Dis- tributed Interactive Simulation (DIS) and High Level Architecture (HLA). The problem domain of inter simulator communication is abstracted to "elementary" Publish/Subscription.. The publish/subscription abstraction, DIS, the DIS based broker and HLA are modeled using a model language called Promela In order to prove if a model is correct a formal specification of what "correct" must be made. Using the Promela language we create LTL which in turn can be applied on the models in order to prove their correctness. When the models and the LTL formulae are finished a tool called SPIN is used to verify wether the models are correct.

SPIN searches the states in the model to find a counterexample situation in which the formula does not hold. If it does find such an example, SPIN will report so. If it does not find an example we have proven that (for the model) the described formula is true. In English a formula can be statements like "It is always the case that when a message is send, it must be received". The modeling has created a better insight in how SPIN does the job of verification. For example it is shown that the verification of large models is not possible due to memory restrictions. It is however shown to be possible to correctly de- scribe the publish/subscription, broker, DIS and HLA functionality in SPIN and verify them.