Verifying the interface compliance of federates using pre- and postconditions of RTI services

The Federation Architecture Metamodel (FAMM) provides a domain specific language for describing the architecture of a High Level Architecture (HLA) compliant federation. A federation architecture model (FAM) consists of the object models and the behavioral models of participating federates. The communication behavior of each federate is to be modeled in the same level of detail as the HLA Federate Interface Specification so as to facilitate standard-compliant code generation. However, this level of detail increases the likelihood of the modelers making mistakes in following the standard. Thus, beyond well-formedness, static checking of the well-behavedness of federate behavioral models is desirable. If it can be shown that all the preconditions of the HLA Runtime Infrastructure (RTI) services used in a behavioral model are satisfiable then we have some assurance that the interface behavior can be compliant to the HLA Federate Interface Specification. In this paper, we present a model checking based procedure to verify the interface behavior of an HLA federate modeled in FAMM. Verification is performed automatically by the help of (1) a model interpreter that takes a FAM as input, and generates the PROMELA model of its behavioral part as output, (2) the SPIN model checker that performs model checking given the generated PROMELA process as input and then outputs the verification result in terms of the preconditions that will not hold at run-time.