Model checking of ambient calculus specifications against ambient logic formulas
Çevrel cebir tanımlamalarının çevrel mantık formülleri ile model denetlemesi
- Tez No: 252581
- Danışmanlar: PROF. DR. MEHMET UFUK ÇAĞLAYAN
- 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: 2009
- Dil: İngilizce
- Üniversite: Boğaziçi Üniversitesi
- Enstitü: Fen Bilimleri Enstitüsü
- Ana Bilim Dalı: Bilgisayar Mühendisliği Ana Bilim Dalı
- Bilim Dalı: Belirtilmemiş.
- Sayfa Sayısı: 85
Özet
Biçimsel metotlar koşut zamanlı sistemlerin tanımlanmasında ve doğrulanmasında yararlanılan matematiksel tekniklerdir. Biçimsel metotların sıkça kullanılan bir örneği de model denetlemedir. Model denetleme yönteminde hedef sistemin soyutlama ile oluşturulurmuş sonlu durumlu bir modeli üzerinde tüm durumların doğrulandığı kapsamlı bir inceleme yürütülür.Sistemlerin zamana bağlı davranışlarını inceleyen model denetleyiciler mevcuttur. Yakın zamanda iki yeni kavram, konumlar ve konum değiştirme, model denetlemede önem kazanmıştır. Konum ve konum değiştirme kavramlarını kapsayan çeşitli model denetleme yöntemleri üzerine algoritmalar önerilmişse de, bu tarz bir denetleme yapabilen çok az model denetleme uygulaması gerçeklenmiştir. Bu tezde koşut zamanlı sistemlerin zamansal ve uzaysal davranışlarını inceleyebilen yeni bir model denetleme metodolojisi önerilmektedir. Önerilen bu model denetleme metodolojisi ile sistemlerin uzaysal davranışları var olan model denetleme uygulamalarından daha kapsamlı bir şekilde incelenebilmektedir.Çevrel cebir ve çevrel mantık bu tez kapsamında modellerin ve sistem özelliklerinin ifade edilmesinde kullanılacak biçimsel dillerdir. Çevrel cebir pi-cebrinden türetilmiş bir işlev cebridir. Çevrel cebir ile koşut zamanlı sistemler, konumlar ve konumsal değişiklikler üzerinden modellenebilir. Çevrel mantık koşut zamanlı sistem modellerinin zamansal ve uzaysal özeliklerinin belirtilebildiği bir kipler mantığıdır. Çevrel mantık çevrel cebir üzerine bina edilmiştir. Önerilen model denetleme metodolojisi girdi olarak bir koşut zamanlı sistemin çevrel cebrin bir alt kümesi ile ifade edilmiş bir modelini ve çevrel mantığın bir alt kümesi ile belirtilmiş sistem özelliklerini alır. Model denetleyici çıktı olarak ya başarı mesajı döner ya da verilen sistem özelliklerinin sağlanmadığı durumları döner. Önerilen model denetleme metodolojisi çevrel cebir ve çevrel mantık kullanan ve hali hazırda gerçeklenmiş olan tek araçtır.Bu tezin kapsamında, gerçeklenmiş olan araç için performans sonuçlarının durum çalışmaları üzerinden gösterilmesi de bulunmaktadır. Çok etki alanlı ağlar için tanımlanmış güvenlik politikalarının güvenlik açıklıkları bulundurmadıkları ve belirli bir ağ yapılandırmasında tutarlı oldukları biçimsel yöntemlerle doğrulanmalıdır. Bu tezdeki durum çalışmalarında çevrel cebir ile modellenmiş çok etki alanlı ağlar, çevrel mantık ile belirtilmiş özelliklere karşı, önerilen model denetleyici ile doğrulanmaktadır.
Özet (Çeviri)
Formal methods are mathematical techniques applied in specification and verification of concurrent interactive systems. Model checking is a widely used formal method for formal verification of systems. In model checking, an exhaustive search is applied on a finite state model of the target system.While there are model checkers to verify the only temporal behaviors of systems, two new notions of model checking analysis recently come into prominence, mobility and locations. Although there are various model checker proposals for modeling and verifying concurrent interactive systems with respect to mobility and locations, there are a few model checker tools able to perform such verifications. In this thesis, a new model checking methodology is proposed which is able to verify temporal and spatial properties of systems together. The proposed model checking methodology is able to perform more detailed verifications than existing tools.In this thesis, ambient logic and ambient calculus are used as formal languages to express models and the properties of the systems. Ambient calculus is a process calculus derived from pi-calculus. It is able to theorize about concurrent systems with respect to mobility and locations. Ambient logic is a modal logic able to express temporal and spatial properties of models. It is strictly based on ambient calculus. Proposed model checking methodology accepts models expressed with a fragment of ambient calculus and properties expressed with a fragment of ambient logic as inputs. It returns a success message or the states of the model which are violating properties. In the scope of this thesis, an implementation of proposed methodology is provided which is the only tool using both ambient calculus and ambient logic.In this thesis, performance of the proposed model checking methodology is shown over case studies. Security policies defined for multi-domain networks need to be formally checked against security breaches and ensured that they are consistent in a given network configuration. In case studies, a set of ambient calculus specifications modeling such networks are verified against ambient logic formulas with proposed model checking methodology.
Benzer Tezler
- Asenkron makina otomasyonu ve bir bant taşıma sisteminin otomasyonunun projelendirilmesi
Başlık çevirisi yok
OZAN ARAY
Yüksek Lisans
Türkçe
1997
Elektrik ve Elektronik Mühendisliğiİstanbul Teknik ÜniversitesiElektrik Mühendisliği Ana Bilim Dalı
PROF. DR. NURDAN GÜZELBEYOĞLU
- Model checking of apoptosis signaling pathways in lung cancers
Akciğer kanseri vakalarında apoptoz sinyal yollarının model denetlemesi
MEHTAP AYFER PARLAK
Yüksek Lisans
İngilizce
2011
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolOrta Doğu Teknik ÜniversitesiBilişim Sistemleri Bölümü
YRD. DOÇ. DR. AYSU BETİN CAN
- Data abstraction method for model checking of real-time systems
Gerçek zamanlı sistemlerin model denetimi için veri soyutlama yöntemi
MUSTAFA DURSUN
Doktora
İngilizce
2015
Elektrik ve Elektronik MühendisliğiOrta Doğu Teknik ÜniversitesiElektrik-Elektronik Mühendisliği Ana Bilim Dalı
PROF. DR. SEMİH BİLGEN
- 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
VİJDAN KIZILAY
Yüksek Lisans
İngilizce
2010
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİstanbul Teknik ÜniversitesiBilgisayar Bilimleri Ana Bilim Dalı
YRD. DOÇ. DR. FEZA BUZLUCA
DR. OKAN TOPÇU
YRD. DOÇ. DR. YUNUS EMRE SELÇUK