Çalışma Zamanı Altyapısı (rtı) Servislerinin Ön Ve Son Koşullarını Kullanarak Federe Arayüz Uyumluluğunun Geçerlenmesi

Abstract

Bu tez federasyon mimari modelini (FAM) olusturan federelerin Canlı Sıralama Çizelgelerinden (LSCs) PROMELA modellerini üreterek federelerin arayüz davranıslarının HLA Arayüz Spesifikasyonuna uyumluluğu üzerine bir model denetleme yaklasımı sunmaktadır. Federasyon Mimari Metamodeli (FAMM), Alan Özel Metamodelleme yaklasımının HLA uyumlu federasyonlarına uyarlanmasıyla federasyon için biçimsel bir gösterim ve uygulama alanına yönelik bir dil sağlamaktadır. FAMM federasyon mimari modelini olusturan nesne modellerinin ve federasyonu olusturan federelerin davranıs modellerinin modellenmesini sağlayan bir metamodeldir. FAMM'ın kullanıldığı modelleme ortamında standart uyumlu kod üretimini kolaylastırmak amacıyla her bir federenin davranıs modelinin programlama seviyesi detayında modellenmesi gerekmektedir. Ancak bu seviyede detay modelcilerin standarda göre hata yapma olasılığını arttırmaktadır. Bu nedenle iyi bir biçimin yanında, federelerin davranıs modellerinin anlamsal kavramının statik olarak denetlemesi istenir. Eğer bir davranıs modelinde kullanılan HLA RTI servislerinin tüm ön kosullarının karsılanabildiği gösterilebilirse, arayüz davranısının HLA Federe Arayü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çin sunulan model denetleme tabanlı prosedür birkaç adımdan olusmaktadır. Geçerleme islemi otomatik olarak su islemler yardımıyla gerçeklestirilmektedir: (1) Federasyon mimari modelini girdi olarak alan bir yorumlayıcı modelin davranıs kısmının PROMELA modelini çıktı olarak üretmektedir, (2) SPIN model denetleyicisi girdi olarak aldığı PROMELA modeli üzerinde model denetleme islemini gerçeklestirir ve geç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 interface behaviors of federates to the High Level Architecture (HLA) Federate Interface Specification by generating PROMELA models from Live Sequence Charts (LSCs) of federates in a federation architecture model (FAM). FAMM provides a domain specific language and a formal representation for describing the architecture of an HLA compliant federation. A federation architecture model consists of the object models and the behavioral models of participating federates. Currently, the behavioral model of each federate is required to be modeled in the same level of detail as the HLA Federate Interface Specification so as to facilitate standardcompliant code generation. However, this level of detail increases the likelihood of the modelers making mistakes in the following standart. Thus, beyond wellformedness, 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. Model checking based procedure which is presented to verify the interface behavior of an HLA federate modeled in FAMM consists of a few steps. 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 model as input and then outputs the verification result in terms of the preconditions that will not hold at run-time.