Formalising Simulation. A goal of ADVANCE is to use a formal approach to developing the simulation framework. In a commercial simulator, the semantics of a given simulation is determined by the descriptions of each component model in the design hierarchy to be simulated, as defined in the simulation language reference manual and also the implementation of the synchronisation and communica- tion mechanisms, used by those component models, in the simulator kernel. In ADVANCE, we will develop and refine simulation models which define, formally, not only the components but also the synchronisation and commu- nication mechanisms themselves. The model description itself will therefore define, completely the simulation semantics of that model in the formal lan- guage, Event-B. This will enable the ADVANCE user to start with an un- timed, high-level model of the system and, using systematic Event-B formal refinement, introduce incrementally more and more timing and synchronisa- tion detail and prove formally that, at each step, the more detailed model is a correct refinement of its abstract parent. At each step it will also be possible to simulate and model check the model description.
