Data abstraction method for model checking of real-time systems
Gerçek zamanlı sistemlerin model denetimi için veri soyutlama yöntemi
- Tez No: 381029
- Danışmanlar: PROF. DR. SEMİH BİLGEN
- Tez Türü: Doktora
- Konular: Elektrik ve Elektronik Mühendisliği, Electrical and Electronics Engineering
- Anahtar Kelimeler: Belirtilmemiş.
- Yıl: 2015
- Dil: İngilizce
- Üniversite: Orta Doğu Teknik Üniversitesi
- Enstitü: Fen Bilimleri Enstitüsü
- Ana Bilim Dalı: Elektrik-Elektronik Mühendisliği Ana Bilim Dalı
- Bilim Dalı: Belirtilmemiş.
- 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
- 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
- Hipersezgisel yöntemlerle lojistik ağ tasarımı ve optimizasyon
Logistic network design and optimization using hyperheuristic methods
VURAL EROL
Doktora
Türkçe
2017
Endüstri ve Endüstri Mühendisliğiİstanbul Teknik ÜniversitesiEndüstri Mühendisliği Ana Bilim Dalı
DOÇ. DR. MURAT BASKAK
PROF. DR. GÜLGÜN KAYAKUTLU
- 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
2018
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolKoç ÜniversitesiBilgisayar Bilimleri ve Mühendisliği Ana Bilim Dalı
PROF. DR. ATTİLA GÜRSOY
- 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
2005
İstatistikOndokuz Mayıs Üniversitesiİstatistik Ana Bilim Dalı
YRD. DOÇ. DR. KAMİL ALAKUŞ
- 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