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ı, Bilgisayar donanımları, Bilgisayar yazılımları, Sıra eksiltme teknikleri, Model Checking, Hardware/Software Co-Design, Hardware/Software Co- Verification, Partial Order Reduction Techniques, SDL IV DOKÜMANTASYON MERK, Hardware, Computer softwares, Model control, Order reduction techniques
- 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ı: Belirtilmemiş.
Ö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
- Bir atık barajının sismik yükler ve sürekli yağış etkisinde dinamik analizinin değerlendirilmesi
Evaluation of dynamic analysis of tailings dam under the effect of seismic loads and continuous rainfall
HASAN ÇELT
Yüksek Lisans
Türkçe
2025
Maden Mühendisliği ve Madencilikİstanbul Teknik ÜniversitesiMaden Mühendisliği Ana Bilim Dalı
PROF. DR. ATAÇ BAŞÇETİN
- 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
Savunma ve Savunma Teknolojileriİstanbul Teknik ÜniversitesiMakine Mühendisliği Ana Bilim Dalı
YRD. DOÇ. DR. LEVENT ALİ KAVURMACIOĞLU
- Disk kanatçık sistemlerindeki düzensizlik davranışının ANSYS programı ile istatistiksel olarak incelenmesi
Statistical investigation of mistuning behaviour of bladed disc systems with ANSYS program
ONUR AĞDACI
Yüksek Lisans
Türkçe
2018
Savunma ve Savunma Teknolojileriİstanbul Teknik ÜniversitesiUçak ve Uzay Mühendisliği Ana Bilim Dalı
PROF. DR. VEDAT ZİYA DOĞAN
- Sincap kafesli asenkron makinenin rotor alan yönlendirmeli kontrolü
Rotor field-orientation control of a squirrel cage induction machine
SAFFET ALTAY
Yüksek Lisans
Türkçe
1995
Elektrik ve Elektronik Mühendisliğiİstanbul Teknik ÜniversitesiPROF.DR. M. EMİN TACER