A TLA+ Specification of the HLA Time Management Algorithm

摘要

The High Level Architecture (HLA) Interface Specification visually (using Statecharts) and textually (with structured English prose and embedded mathematics) defines a model of a simulation middleware. While such a specification is enough for a software engineer to construct a conforming Runtime Infrastructure (RTI) or to build a federate against the defined Application Programming Interface (API), the specification is not formal enough to allow a computer to automatically verify that the specification enforces invariants of the simulation middleware. Formal methods, such as the Temporal Logic of Actions (TLA+), exist to capture specifications of models of systems in a way that such verification can be performed. This paper presents a TLA + specification of the Time Management algorithm described in the HLA Interface Specification. The TLC Model Checker (part of the TLA+ Toolbox) is used to show that the specification does enforce desired invariants of the Time Management algorithm.