Formalizing a Specification for Analysis: The HLA Ownership Properties

Authors: Craig A. Damon, Ralph Melton, Robert J. Allen,
Elizabeth Bigelow, James M. Ivers, and David Garlan

Technical Report CMU-CS-99-126.

Abstract

Interfaces are commonly specified using informal or semi-informal techniques, relying primarily on natural language descriptions. Such specifications, however, can easily overlook significant details and are not amenable to analysis by automated tools. This paper looks at formalizing one portion of a substantial specification, the ownership management chapter of the DoD HLA framework, and at the subsequent analysis using the tool Ladybug.

Keywords:Formal specification, model checking, Z specification language, distributed simulation

Brought to you by Composable Software Systems Research Group in the School of Computer Science at Carnegie Mellon University.

[Last modified 26-Aug-1999.
Mail suggestions to the Maintainer.]