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

Abstract

Bu tez federasyon mimari modelini (FAM) olusturan federelerin Canlı SıralamaÇizelgelerinden (LSCs) PROMELA modellerini üreterek federelerin arayüzdavranıslarının HLA Arayüz Spesifikasyonuna uyumluluğu üzerine bir modeldenetleme yaklasımı sunmaktadır. Federasyon Mimari Metamodeli (FAMM), AlanÖzel Metamodelleme yaklasımının HLA uyumlu federasyonlarına uyarlanmasıylafederasyon için biçimsel bir gösterim ve uygulama alanına yönelik bir dilsağlamaktadır. FAMM federasyon mimari modelini olusturan nesne modellerinin vefederasyonu olusturan federelerin davranıs modellerinin modellenmesini sağlayan birmetamodeldir. FAMM'ın kullanıldığı modelleme ortamında standart uyumlu kodüretimini kolaylastırmak amacıyla her bir federenin davranıs modelinin programlamaseviyesi detayında modellenmesi gerekmektedir. Ancak bu seviyede detaymodelcilerin standarda göre hata yapma olasılığını arttırmaktadır. Bu nedenle iyi birbiçimin yanında, federelerin davranıs modellerinin anlamsal kavramının statik olarakdenetlemesi istenir. Eğer bir davranıs modelinde kullanılan HLA RTI servislerinintüm ön kosullarının karsılanabildiği gösterilebilirse, arayüz davranısının HLA FedereArayüz Spesifikasyonuna uyumluluğu konusunda biraz güvenceye sahip olabiliriz.FAMM ile modellenmis bir HLA federesinin arayüz davranısının geçerlenmesi içinsunulan model denetleme tabanlı prosedür birkaç adımdan olusmaktadır. Geçerlemeislemi otomatik olarak su islemler yardımıyla gerçeklestirilmektedir: (1) Federasyonmimari modelini girdi olarak alan bir yorumlayıcı modelin davranıs kısmınınPROMELA modelini çıktı olarak üretmektedir, (2) SPIN model denetleyicisi girdiolarak aldığı PROMELA modeli üzerinde model denetleme islemini gerçeklestirir vegeçerleme sonuçlarını çalısma zamanında karsılanamayacak ön kosullar açısından sunar.

This thesis presents a model checking approach on the compliance of the interfacebehaviors of federates to the High Level Architecture (HLA) Federate InterfaceSpecification by generating PROMELA models from Live Sequence Charts (LSCs)of federates in a federation architecture model (FAM). FAMM provides a domainspecific language and a formal representation for describing the architecture of anHLA compliant federation. A federation architecture model consists of the objectmodels and the behavioral models of participating federates. Currently, thebehavioral model of each federate is required to be modeled in the same level ofdetail as the HLA Federate Interface Specification so as to facilitate standardcompliantcode generation. However, this level of detail increases the likelihood ofthe modelers making mistakes in the following standart. Thus, beyond wellformedness,static checking of the well-behavedness of federate behavioral models isdesirable. If it can be shown that all the preconditions of the HLA RuntimeInfrastructure (RTI) services used in a behavioral model are satisfiable then we havesome assurance that the interface behavior can be compliant to the HLA FederateInterface Specification.Model checking based procedure which is presented to verify the interface behaviorof an HLA federate modeled in FAMM consists of a few steps. Verification isperformed automatically by the help of (1) a model interpreter that takes a FAM asinput, and generates the PROMELA model of its behavioral part as output, (2) theSPIN model checker that performs model checking given the generated PROMELAmodel as input and then outputs the verification result in terms of the preconditionsthat will not hold at run-time.