We describe how to apply the tools and techniques of process
algebra to explore and verify the structure of simulation models.
Process algebras are concise and precise object-oriented notations
in which to express model structure and component interactions. We
demonstrate how to specify the structure and basic synchronisations of
simulation models using Milner's CCS (Calculus of Communicating
Systems) notation, and how to test for the consequences of a
specification using the modal $mu$-calculus (Stirling). In this
way we open up the possibility of verifying from its static model
description that a simulation model has certain basic desirable
properties (is deadlock and livelock free and has appropriate
safety, liveness and fairness characteristics (Manna and Pnueli)).
Thus adopting these techniques from process algebra both makes models
more reliable and saves a considerable amount of debugging time.
We are currently acquiring citations for the work deposited into this collection. We recognize the distribution rights of this item may have been assigned to another entity, other than the author(s) of the work.If you can provide the citation for this work or you think you own the distribution rights to this work please contact the Institutional Repository Administrator at email@example.com