Formalizing a Specification for Analysis:
The HLA Ownership Properties
Authors:Craig A. Damon, Ralph Melton, Robert J. Allen, Elizabeth Bigelow, James M. Ivers, David Garlan
TR CMU-CS-99-126
April 1999.
Download the PostScript.
Abstract
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.
Keywords:
Formal specification, model checking, Z specification language,
distributed simulation
Back to Nitpick Home Page