Sonlu durum sistemleri için sembolik bir model doğrulayıcısının gerçekleştirimi
Implementation of a symbolic model checker for finite state systems
- Tez No: 29684
- Danışmanlar: PROF. DR. H. SELÇUK GEÇİM
- Tez Türü: Yüksek Lisans
- Konular: Elektrik ve Elektronik Mühendisliği, Electrical and Electronics Engineering
- Anahtar Kelimeler: Belirtilmemiş.
- Yıl: 1993
- Dil: Türkçe
- Üniversite: Hacettepe Üniversitesi
- Enstitü: Fen Bilimleri Enstitüsü
- Ana Bilim Dalı: Elektrik-Elektronik Mühendisliği Ana Bilim Dalı
- Bilim Dalı: Belirtilmemiş.
- Sayfa Sayısı: 158
Özet
IV ÖZET Bu tezde sonlu durum sistemleri için sembolik bir model doğrulayıcı DOS ortamında C dilinde gerçekleştirilmiştir. Bir sistemin belirli bir özelliği sağlayıp sağlamadığının denetimi olarak tanımlanan doğrulama problemi ve özel olarak model doğrulama yöntemi incelenmiştir. Genel bir yaklaşım çerçevesinde ifade gücü yüksek mü-hesabı için bir model doğrulama yöntemi tanımlanmıştır. Sonlu durum sistemlerinin doğrulamasında ortaya çıkan durum patlaması probleminin çözümü için ikil karar şemaları kullanılmıştır. Boole cebri için tanımlanan ikil karar şemaları Boole fonksiyonlarının gösteriminde ekonomik yapılar üretilmesini olanaklı kılarlar. İkil karar şemalarının kullanımı ile sistem bilgileri olası en küçük boyutlarda saklanır. Böylelikle daha fazla durumlu sistemlerin doğrulamasının yapılması mümkündür. Yöntem bu alanda en yaygın olarak kullanılan yapı olan Zamansal Mantık ile karşılaştırılmış ve Zamansal Mantık formüllerinin mü-hesabmda gösterimleri tanımlanmıştır. Gerçekleştirimde kullanım kolaylığını sağlayacak ve zaman ve yer karmaşıklığını azaltacak gelişmeler belirtilmiştir. ANAHTAR KELİMELER Doğrulama, Model Doğrulama, İkil Karar Şemaları, Mü-hesabı, Zamansal Mantık
Özet (Çeviri)
ABSTRACT In this thesis a symbolic model checker for finite state systems is implemented using C on DOS environment. Verification problem which is the process of checking whether a system meets a specified property and specifically the model checking method are investigated. A model checking method is defined in a general framework for mu-calculus which has high expressivity. For the solution of the state explosion problem which occurs in the verification of finite state systems binary decision diagrams are used. Binary decision diagrams that are defined for Boolean algebra allow to produce economical structures in the representation of Boolean functions. By the usage of binary decision diagrams system data are stored in smallest possible sizes. So that it is possible to verify the systems with more states. Method is compared with the Temporal Logic which is the most popular structure in this area and the representation of Temporal Logic formulas in mu-calculus are defined. Improvements which allows usage simplicity and reduction in the time and space complexity are stated. KEYWORDS Verification, Model Checking, Binary Decision Diagrams, Mu-calculus, Temporal Logic
Benzer Tezler
- Designing, verification and validation of railway signaling systems using coloured petri nets
Demiryolu sinyalizasyon sistemleri için renkli petri ağlarını kullanarak tasarım, doğrulama ve onaylama
ALI ELHAYEK
Yüksek Lisans
İngilizce
2016
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİstanbul Teknik ÜniversitesiKontrol ve Otomasyon Mühendisliği Ana Bilim Dalı
PROF. DR. MEHMET TURAN SÖYLEMEZ
- Utilizing mathematica software solution of boundary value problems in nuclear engineeringby the greens function method
Mathematica yazılımı kullanılarak nükleer mühendislikte karşılaşılan sınır değer problemlerinin green fonksiyonu metodu ile çözümü
DİLEK ŞENER
Yüksek Lisans
İngilizce
1998
Nükleer Mühendislikİstanbul Teknik ÜniversitesiNükleer Enerji ve Enerji Sistemleri Ana Bilim Dalı
DOÇ. DR. AKİF ATALAY
- Sembolik dinamik sistemleri ve kodlama teorisi üzerine
Başlık çevirisi yok
HASAN AKIN
Doktora
Türkçe
1998
MatematikYüzüncü Yıl ÜniversitesiMatematik Ana Bilim Dalı
PROF. DR. ABDURRRAHİM YILMAZ
- Kafes sistemlerin optimum tasarımı
Optimum design of truss systems
NURGÜL GÖKDERE
Yüksek Lisans
Türkçe
2002
Makine Mühendisliğiİstanbul Teknik ÜniversitesiMekanik Ana Bilim Dalı
DOÇ. DR. EROL ŞENOCAK
- Suboptimal control of dynamic systems using polynominal parameterization symbolic manipulation
Polinom parametrizasyonu ve sembolik manipülasyon kullanarak dinamik sistemlerin yaklaşık-optimum kontrolü
EROL YILMAZ
Yüksek Lisans
İngilizce
1997
Makine MühendisliğiOrta Doğu Teknik ÜniversitesiMakine Mühendisliği Ana Bilim Dalı
PROF. DR. REŞİT SOYLU