Verifying the interface compliance of federates using pre- and postconditions of RTI services
Çalışma zamanı altyapısı (RTI) servislerinin ön ve son koşullarını kullanarak federe arayüz uyumluluğunun geçerlenmesi
- Tez No: 386936
- Danışmanlar: YRD. DOÇ. DR. FEZA BUZLUCA, DR. OKAN TOPÇU, YRD. DOÇ. DR. YUNUS EMRE SELÇUK
- Tez Türü: Yüksek Lisans
- Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Computer Engineering and Computer Science and Control
- Anahtar Kelimeler: Belirtilmemiş.
- Yıl: 2010
- Dil: İngilizce
- Üniversite: İstanbul Teknik Üniversitesi
- Enstitü: Bilişim Enstitüsü
- Ana Bilim Dalı: Bilgisayar Bilimleri Ana Bilim Dalı
- Bilim Dalı: Bilişim Bilim Dalı
- Sayfa Sayısı: 91
Özet
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.
Özet (Çeviri)
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.
Benzer Tezler
- Kalite çemberleri ve TS-ISO 9000 uygulamaları
Quality circles and TS-ISO 9000 practies
MUSA GÜRSOY
Yüksek Lisans
Türkçe
1994
Endüstri ve Endüstri Mühendisliğiİstanbul Teknik ÜniversitesiPROF.DR. ATAÇ SOYSAL
- Design of a stylus with variable tip compliance
Değiştirilebilir uç esnekliğine sahip stylus tasarımı
ÖZDEMİR CAN KARA
- IEEE 1149.1 standardı kullanarak test edilebilir lojik devre tasarımı
Testable lojik circit design by using IEEE 1149.1 standard
A.BETÜL TUNCER
Yüksek Lisans
Türkçe
1992
Elektrik ve Elektronik Mühendisliğiİstanbul Teknik ÜniversitesiPROF. DR. AHMET DERVİŞOĞLU
- Bir arıza giderme uzman sistem kabuğu (AGUSK) ve CFM56 turbofan jet motor arızaları için bir uygulama
Başlık çevirisi yok
MEHMET BİRLİK
Yüksek Lisans
Türkçe
1998
Mühendislik Bilimleriİstanbul Teknik ÜniversitesiMühendislik Bilimleri Ana Bilim Dalı
DOÇ. DR. GAZANFER ÜNAL
- Fotovoltaik silisyum güneş hücreleri için nikel metal kontak geliştirilmesi
Development of nickel metal contacts for photovoltaic silicon solar cells
BERKELI AKGAYEV
Yüksek Lisans
Türkçe
2024
EnerjiNecmettin Erbakan ÜniversitesiEnerji Sistemleri Mühendisliği Ana Bilim Dalı
DR. ÖĞR. ÜYESİ VEYSEL ÜNSÜR
