CMU-CS-99-126
Computer Science Department
School of Computer Science, Carnegie Mellon University



CMU-CS-99-126

Formalizing a Specification for Analysis:
The HLA Ownership Properties

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

April 1999

CMU-CS-99-126.ps
CMU-CS-99-126.pdf


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


Interfaces are commonly specified using informal or semi-formal 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.

58 pages


Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu