CHARACTERISING THE STRUCTURE OF SIMULATION MODELS IN CCS
Date
1993-10-01
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
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.
Description
Keywords
Computer Science