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

Vijdan Kizilay*, Halit Oguztüzün, Okan Topçu, Feza Buzluca

*Bu çalışma için yazışmadan sorumlu yazar

Araştırma sonucu: Kitap/Rapor/Konferans Bildirisinde BölümKonferans katkısıbilirkişi

Özet

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.

Orijinal dilİngilizce
Ana bilgisayar yayını başlığıFall Simulation Interoperability Workshop 2009, 2009 Fall SIW
Sayfalar451-458
Sayfa sayısı8
Yayın durumuYayınlandı - 2009
EtkinlikFall Simulation Interoperability Workshop 2009, 2009 Fall SIW - Orlando, FL, United States
Süre: 21 Eyl 200925 Eyl 2009

Yayın serisi

AdıFall Simulation Interoperability Workshop 2009, 2009 Fall SIW

???event.eventtypes.event.conference???

???event.eventtypes.event.conference???Fall Simulation Interoperability Workshop 2009, 2009 Fall SIW
Ülke/BölgeUnited States
ŞehirOrlando, FL
Periyot21/09/0925/09/09

Parmak izi

Verifying the interface compliance of federates using pre- and postconditions of RTI services' araştırma başlıklarına git. Birlikte benzersiz bir parmak izi oluştururlar.

Alıntı Yap