Static partial order reduction and model checking of hardware/software co-design systems
Durağan kısmi sıra eksiltme ve donanım/yazılım birleşik sistemlerin model kontrolü
- Tez No: 90974
- Danışmanlar: DOÇ. DR. GÜNEY GÖNENÇ
- Tez Türü: Doktora
- Konular: Elektrik ve Elektronik Mühendisliği, Electrical and Electronics Engineering
- Anahtar Kelimeler: Model Kontrolü, Donanım/Yazılım Birleşik Tasarım, Donanım/Ya zılım Birleşik Doğrulama, Kısmi Sıra Eksiltme Teknikleri, SDL vı, Model Checking, Hardware/Software Co-Design, Hardware/Software Co- Verification, Partial Order Reduction Techniques, SDL IV DOKÜMANTASYON MERK
- Yıl: 2000
- 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ı: 150
Özet
oz DURAĞAN KISMI SIRA EKSİLTME VE DONANIM/YAZILIM BİRLEŞİK SİSTEMLERİN MODEL KONTROLÜ Yenigün, Hüsnü Doktora, Elektrik Elektronik Mühendisliği Bölümü Tez Yöneticisi: Assoc. Prof. Dr. Güney Gönenç Temmuz 2000, 138 sayfa Günümüz tasarımlarının artık çok karmaşık ve büyük sistemler olmasından dolayı, tasarımcılar her aşamada otomatik araçlara gerek duymaktadırlar. Tasarlanan sistem ler büyüdükçe, istemeden de olsa daha fazla hatalı tasarımlar yapılmakta, ve bu da sorun giderme safhasının proje tamamlanma süresinde çok büyük bir faktör olmasına yol açmaktadır. Model kontrolü metodunun sorun giderme safhasında ne denli etkili ve yararlı bir metod olduğu bilinmektekir. Son zamanlarda, tasarlanan sistemlerin sadece yazılım veya sadece donanımdan ibaret olmadığım görmekteyiz. Yazılım/donanım birleşik tasarımı adı verilen bu yön temde, sistemin yüksek performans gerektiren bölümleri donanım yolu ile, kolayca değiştirilebilmesi gereken kısımları ise yazılım yolu ile tasarlanmaktadır. Sadece donanım veya sadece yazılım tasarımlan için model kontrolü araçları hali hazırda mevcuttur. Fakat donanım/yazılım birleşik tasarımları için bir model kontrolü aracı bulunmamaktadır. Bu tezde, donanım/yazılım birleşik tasarımları için bir model kontrolü aracı geliştirilmiştir. Aynı zamanda, model kontrolü araçlarının pratik uygulamasının önündeki en büyük engel olan durum uzayı patlaması problemine de değinilmiştir. Kısmi sıra eksiltme tekniklerinin yazılım tasarımlarının model kontrolünde bu probleme iyi bir çözüm olduğu bilinmektedir. Donanım tasarımlarının model kontrolünde de bu problemeçare olarak sembolik arama teknikleri kullanılmaktadır. Donanım/yazılım birleşik tasarımlarının model kontrolünde doğal olarak karşımıza çıkan ilk soru kısmi sıra eksiltme tekniği ile sembolik arama tekniğinin birlikte kul lanılıp kullanılamayacağıdır. Bu tezde bu soru olumlu yanıtlanmış, ve bunun nasıl yapılabileceği açıklanmıştır. Kısmi sura eksiltme tekniğinin, model kontrolü aracının dışında, bir ön süreç olarak geliştirilmesini kolaylaştıran yeni bir formülasyonu ver ilmiştir.
Özet (Çeviri)
ABSTRACT STATIC PARTIAL ORDER REDUCTION AND MODEL CHECKING OF HARDWARE/SOFTWARE CO-DESIGN SYSTEMS Yenigün, Hüsnü Ph.D., Department of Electrical and Electronics Engineering Supervisor: Assoc. Prof. Dr. Güney Gönenç July 2000, 138 pages Due to the complexity of the systems developed nowadays, developers need automated tool support at every step of the design cycle. As the systems get bigger, more and more bugs are mistakenly coded into the designs. Therefore, the debugging phase becomes an important factor for reducing time-to-market for industrial projects. Model checking has shown to be a very useful method for the debugging phase of complex designs. A recent trend in system development is the so-called“co-design”, where the parts of the system that require high performance are developed in hardware, and the parts which require easy reconfigurability are developed in software. There exist model checking tools for pure hardware and pure software systems. However, this is not the case for co-design systems. This thesis introduces a model checking environment for co-design systems. The state explosion problem which is the biggest obstacle for the practical appli cation of model checking is addressed as well Partial order reduction is known to be a good remedy for the state explosion problem in model checking of software systems. Similarly, symbolic search techniques are used to fight off state explosion for model checking of hardware systems. The natural question that arises for model checking of co-design systems is if the partial order reduction techniques and symbolic search be combined. In this thesis, mit is explained how these two techniques can be used simultaneously as well A new formulation of the partial order reduction technique is given for this purpose, which allows the implementation of it as a preprocessing stage, performed prior to model checking.
Benzer Tezler
- Distal femur parsiyel artiküler medial kondil kırıklarında (AO 33B2.1) 4 farklı tespit yönteminin biyomekanik karşılaştırması
Biomechanic comparison of 4 different fixation methods in distal femur partial articular medial condyle fractures (AO 33B2.1)
ATAHAN DURĞAL
Tıpta Uzmanlık
Türkçe
2024
Ortopedi ve TravmatolojiSağlık Bilimleri ÜniversitesiOrtopedi ve Travmatoloji Ana Bilim Dalı
PROF. DR. GÜZELALİ ÖZDEMİR
- Eksenel gaz türbini kanat ucu geometrisinin hesaplamalı akışkanlar dinamiği ile aerotermal tasarımı
Aerothermal design of axial gas turbine blade tip using computational fluid dynamics
CEM BERK ŞENEL
Yüksek Lisans
Türkçe
2016
Makine Mühendisliğiİstanbul Teknik ÜniversitesiMakine Mühendisliği Ana Bilim Dalı
YRD. DOÇ. DR. LEVENT ALİ KAVURMACIOĞLU
- Düşük sıcaklıkta enerji depolama
Low temperature thermal storage
ERTÜRK ÇAĞRIHAN GENÇ
Yüksek Lisans
Türkçe
2019
Makine Mühendisliğiİstanbul Teknik ÜniversitesiMakine Mühendisliği Ana Bilim Dalı
PROF. DR. MUSTAFA ÖZDEMİR
- Küt cisimlerde sürüklenme kuvvetinin azaltılması için kilitlenmiş girdap oluşumlarının deneysel yöntemlerle araştırılması
Başlık çevirisi yok
ŞEREF ERKARA
Doktora
Türkçe
1997
Uçak Mühendisliğiİstanbul Teknik ÜniversitesiUçak Mühendisliği Ana Bilim Dalı
PROF. DR. M. ZEKİ ERİM