Formal Modeling and Analysis of the HLA RTI

Robert Allen, and David Garlan

Proceedings of the 1997 Spring Simulation Interoperability Workshop, Orlando, FL, March 1997.

Online links: Postscript PDF BIBTEX Citation

Abstract

The HLA RTI is a complex artifact, supporting several classes of interaction (e.g., federation management, object management, time management). A critical challenge in producing an RTI architectural framework (and its associated simulation interface specifications) is to develop confidence that its specification is well-formed and complete. In this paper we describe on-going work in formally modelling the HLA both to document the standard more precisely, as well as to analyze it for anomalies, omissions, inconsistencies, and ambiguities. The technical basis for this work is the use of a formal architectural description language, called Wright, and its accompanying toolset.

Keywords

Software Architecture, Formal Specification, HLA, Wright

For further information, please visit the home pages of the ABLE research project and Carnegie Mellon University's Composable Systems Group.

Last modified: 10/15/2001. For comments and problems, contact able-help@cs.cmu.edu.