Show/Hide Menu
Hide/Show Apps
anonymousUser
Logout
Türkçe
Türkçe
Search
Search
Login
Login
OpenMETU
OpenMETU
About
About
Açık Bilim Politikası
Açık Bilim Politikası
Frequently Asked Questions
Frequently Asked Questions
Browse
Browse
By Issue Date
By Issue Date
Authors
Authors
Titles
Titles
Subjects
Subjects
Communities & Collections
Communities & Collections
Verifying the interface compliance of federates using pre- and postconditions of RTI services
Date
2009-12-01
Author
Kizilay, Vijdan
Oguztüzün, Halit
Topçu, Okan
Buzluca, Feza
Metadata
Show full item record
Item Usage Stats
0
views
0
downloads
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. Copyright © (2009) by SISO - Simulation Interoperability Standards Organization.
URI
https://www.scopus.com/inward/record.uri?partnerID=HzOxMe3b&scp=84865581577&origin=inward
https://hdl.handle.net/11511/79557
Collections
Unverified, Article