Chris Tofts and Graham Birtwistle
School of Computer Studies
University of Leeds
Leeds, LS2 9JT, UK
chris@scs.leeds.ac.uk, graham@scs.leeds.ac.uk
ACM Transactions on Modeling and Computer Simulation
vol. 8, no. 3 (July 1998)
Paper (PostScript
240 KB)
Paper (GZipped
PostScript 73 KB)
Papers only available to TOMACS subscribers and others authorized to access the ACM Digital Library.
In this paper, we present semantic translations for the actions of muDemos, a process-based, discrete event simulation language. Our formal translation schema permits the automatic construction of a process algebraic representation of the underlying simulation model which can then be checked for freedom from deadlock and livelock, as well as system-specific safety and liveness properties. As simulation methodologies are increasingly being used to design and implement complex systems of interacting objects, the ability to perform such verifications is of increasing methodological importance. We also present a normal form for the syntactic construction of $\mu$Demos programs which allows for the direct comparison of such programs (two programs with the same normal form must execute in identical fashion), reduces model proof obligations by minimising the number of language constructs, and permits an implementer to concentrate on the basic features of the language (since any program implementation which efficiently evaluates normal forms will be an efficient evaluator for the complete language).
Simulation, Semantics
D.4.8 [Simulation]
Discrete Event Simulation, Process Algebra, Sematics