Temporal Verification Framework for HLA Federations
Assignments
Analysis of temporal
reasoning based simulation verification process
Program design and
coding for Temporal Reasoning based verification process
Date :
March 2000-March 2001
Supported
by : ACIMS/TUBITAK
Languages :
DEVS/JAVA,
Prolog
Brief Description
“Temporal Verification
Framework” offers a verification process based on Temporal Reasoning. The tool
takes simulation execution
results (state variables and related times) and temporal formulas that
represent the behavior of the system as inputs and generates verification
result according to the temporal formulas.
Temporal assertions are
directly related the real world, they can be generated from natural language
statements since it is based on logic. These assertions impose safety and
liveness conditions when they are generated based on the correct behaviors of
systems. Temporal assertions based verification bridges the gap between the
operation of simulation models and what is expected from the simulation.
This framework offers a
well-defined process for operational verification in developing verified,
validated and accredited simulation models and HLA Federations.
For HLA domain, the approach enables us to focus on whole
federation behavior as well as separate federate behaviors. This allows
simulation developers to verify that they have behaviorally correct federations
that are composed of dynamically verified federates.
The main parts of the
architecture are observer, language acceptor and verificator. When these two
modules are plugged in a federation execution, the behavior of federation is
verified at execution time. A proof-of-concept program was developed using the
DEVSJAVA and Prolog and DEVS/HLA
environments. The software shows the advantages of OOP paradigm with Logic
programming paradigm combination.
In addition to all, the
framework creates a design
satisfying simulation execution results. This is a reverse engineering approach
to determine how different user’s design from the design that execution results
support.
The software tool is taken a part in the report “MSIAC
(Modeling & Simulation Information Analysis Center) Verification,
Validation and Acreditation Automated Support Tools” A State of the Art Report
15 December 2000”.