Geri Dön

Data abstraction method for model checking of real-time systems

Gerçek zamanlı sistemlerin model denetimi için veri soyutlama yöntemi

  1. Tez No: 381029
  2. Yazar: MUSTAFA DURSUN
  3. Danışmanlar: PROF. DR. SEMİH BİLGEN
  4. Tez Türü: Doktora
  5. Konular: Elektrik ve Elektronik Mühendisliği, Electrical and Electronics Engineering
  6. Anahtar Kelimeler: Belirtilmemiş.
  7. Yıl: 2015
  8. Dil: İngilizce
  9. Üniversite: Orta Doğu Teknik Ü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ı: 70

Özet

Model irdeleme, sonlu durum sistemlerinin doğrulanmasında, sistem modeli ve biçimsel özellikler kullanılarak belli bir durumda belli bir özelliğin geçerli olup olmadı ğının sistematik biçimde irdelenmesini sağlayan otomatik teknikleri içerir. Model irdelemenin başlıca sınırlaması sonsuz durumlu sistemlerin modellenmesinde ortaya çıkmaktadır. Bu sınırlama, gerçek zaman kısıtlamalarının doğrulanması ve sonsuz veri tanım kümelerinin göz önünde bulundurulması zorunluluğundan dolayı, model irdelemenin gerçek zamanlı sistemlerde uygulanabilmesi için esas engeldir. Zamanlı otomatlar zamansal davranış üzerindeki gerçek zaman kısıtlarının modellenmesinde başarıyla kullanılmaktadır. Sonsuz veri kümelerinin soyutlanarak sonlu betimlenmesi model irdelemenin uygulanabilirliği bakımından zorunludur. Bu çalışmada, eşzamanlı, asenkron ve periyodik bir görev kümesi tarafından müşterek olarak üretilen veri için bir soyutlama yöntemi sunulmaktadır. Önerilen yöntem ile, üretilen verilerin zamansal bağımlılıkları dikkate alınarak sonsuz bir veri tanım kümesi sonlu bir veri tanım kümesi ile eşlenmekte, ve veri bir sonlu durum otomatı ile modellenmektedir. Önerilen yöntemin uygulanabilirliği, çok algılayıcı bir sistemde veri bütünlestirme problemi üzerinde gösterilmiştir.

Özet (Çeviri)

Model checking consists of automatic techniques for verifying whether a specified formal property holds for a specific state in a given finite-state model of a system. A major limitation of model checking arises in modeling infinite state systems. This limitation is the main obstacle for model checking of real time systems, due to the need for verifying real time constraints and the necessity of considering infinite data domains. Timed automata models are used to successfully cater for temporal behavior in modeling real time constraints. Abstracting infinite data sets with finite representations is mandatory for feasibility of model checking. In this study, we present an abstraction method for data which is collectively produced by a set of concurrent, asynchronous and periodic tasks in a real time system. The proposed method maps the infinite data domain to a finite one by taking temporal dependencies into account, and models the data with a finite state automaton. Proof of concept is provided with a case study that implements the proposed technique on a multi-sensor data aggregation problem.

Benzer Tezler

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

    Türkçe

    1998

    Mühendislik Bilimleriİstanbul Teknik Üniversitesi

    Mühendislik Bilimleri Ana Bilim Dalı

    DOÇ. DR. GAZANFER ÜNAL

  2. Hipersezgisel yöntemlerle lojistik ağ tasarımı ve optimizasyon

    Logistic network design and optimization using hyperheuristic methods

    VURAL EROL

    Doktora

    Türkçe

    Türkçe

    2017

    Endüstri ve Endüstri Mühendisliğiİstanbul Teknik Üniversitesi

    Endüstri Mühendisliği Ana Bilim Dalı

    DOÇ. DR. MURAT BASKAK

    PROF. DR. GÜLGÜN KAYAKUTLU

  3. Verification of concurrent programs via refinement proofs

    İyileştirme ispatları ile koşut-zamanlı programların doğrulanması

    SÜHA ORHUN MUTLUERGİL

    Doktora

    İngilizce

    İngilizce

    2018

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolKoç Üniversitesi

    Bilgisayar Bilimleri ve Mühendisliği Ana Bilim Dalı

    PROF. DR. ATTİLA GÜRSOY

  4. Sağ kalım analizinde parametre tahmin problemlerine katkılar

    Estimation of parameters problems to contribution in survival analysis

    ESEN ERSOY

    Yüksek Lisans

    Türkçe

    Türkçe

    2005

    İstatistikOndokuz Mayıs Üniversitesi

    İstatistik Ana Bilim Dalı

    YRD. DOÇ. DR. KAMİL ALAKUŞ

  5. Ticari banka yönetimi ve Türk ticari bankalarının temel yönetim sorunları

    The management of the commercial bank and the basic problems of the Turkish comercial bank

    AYŞE ÇİĞDEM ÖNAL

    Yüksek Lisans

    Türkçe

    Türkçe

    1994

    BankacılıkMarmara Üniversitesi

    Bankacılık Ana Bilim Dalı

    PROF. DR. NAZIM EKREN