Geri Dön

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

  1. Tez No: 29684
  2. Yazar: TARIK SEÇKİN
  3. Danışmanlar: PROF. DR. H. SELÇUK GEÇİM
  4. Tez Türü: Yüksek Lisans
  5. Konular: Elektrik ve Elektronik Mühendisliği, Electrical and Electronics Engineering
  6. Anahtar Kelimeler: Belirtilmemiş.
  7. Yıl: 1993
  8. Dil: Türkçe
  9. Üniversite: Hacettepe Üniversitesi
  10. Enstitü: Fen Bilimleri Enstitüsü
  11. Ana Bilim Dalı: Elektrik-Elektronik Mühendisliği Ana Bilim Dalı
  12. Bilim Dalı: Belirtilmemiş.
  13. 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

  1. 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

    İngilizce

    2016

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİstanbul Teknik Üniversitesi

    Kontrol ve Otomasyon Mühendisliği Ana Bilim Dalı

    PROF. DR. MEHMET TURAN SÖYLEMEZ

  2. 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

    İngilizce

    1998

    Nükleer Mühendislikİstanbul Teknik Üniversitesi

    Nükleer Enerji ve Enerji Sistemleri Ana Bilim Dalı

    DOÇ. DR. AKİF ATALAY

  3. Sembolik dinamik sistemleri ve kodlama teorisi üzerine

    Başlık çevirisi yok

    HASAN AKIN

    Doktora

    Türkçe

    Türkçe

    1998

    MatematikYüzüncü Yıl Üniversitesi

    Matematik Ana Bilim Dalı

    PROF. DR. ABDURRRAHİM YILMAZ

  4. Kafes sistemlerin optimum tasarımı

    Optimum design of truss systems

    NURGÜL GÖKDERE

    Yüksek Lisans

    Türkçe

    Türkçe

    2002

    Makine Mühendisliğiİstanbul Teknik Üniversitesi

    Mekanik Ana Bilim Dalı

    DOÇ. DR. EROL ŞENOCAK

  5. 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

    İngilizce

    1997

    Makine MühendisliğiOrta Doğu Teknik Üniversitesi

    Makine Mühendisliği Ana Bilim Dalı

    PROF. DR. REŞİT SOYLU