Formal verification for I2C communication protocol in aerospace and aviation industries
Havacılık ve uzay endüstrilerinde I2C iletişim protokolünün formal doğrulaması
- Tez No: 858824
- Danışmanlar: PROF. DR. YAHYA KEMAL BAYKAL
- Tez Türü: Yüksek Lisans
- Konular: Elektrik ve Elektronik Mühendisliği, Electrical and Electronics Engineering
- Anahtar Kelimeler: Formel doğrulama, Formal verification
- Yıl: 2024
- Dil: İngilizce
- Üniversite: Çankaya Üniversitesi
- Enstitü: Fen Bilimleri Enstitüsü
- Ana Bilim Dalı: Elektrik ve Elektronik Mühendisliği Ana Bilim Dalı
- Bilim Dalı: Elektrik Elektronik Mühendisliği Bilim Dalı
- Sayfa Sayısı: Belirtilmemiş.
Özet
Havacılık sektörü, birçok alt sistem içeren havacılık uygulamalarına sahiptir. Bu nedenle cihazlar ve bileşenler arasında doğru ve güvenilir veri iletişimi kritik bir gerekliliktir. Bu bağlamda, yüksek hız, esneklik, düşük güç tüketimi ve güvenilirlik açısından I2C haberleşme protokolü diğer protokollere göre yaygın bir şekilde tercih edilir. Ancak, I2C veri iletiminde veri bozulması, veri kaybı, yavaş veri iletimi gibi sorunlar ortaya çıkabilir. Bu sorunlar havacılık sektöründe uçuş güvenliği riskleri, elektronik ve mekanik sorunlar, hava trafik yönetimi sorunları, yanlış navigasyon bilgileri gibi ciddi sonuçlara yol açabilir. Bu nedenle, I2C RTL tasarımının eksiksiz ve hatasız bir şekilde yazılması ve ayrıca doğrulanması önemli bir gerekliliktir. Bu tezdeki I2C Master Tasarımı OpenCores'dan indirilmiştir. Sayısal Tasarım Doğrulamada birçok doğrulama yöntemi vardır. Formal Doğrulama en kritik sistemlerde en kesin ve güvenilir doğrulama sağlayan yöntemlerden biridir. Bu yöntem, zamandan ve maliyetten tasarruf sağlayarak tasarımın belirli özelliklere ve gereksinimlere uygun olduğunu matematiksel olarak kontrol eder ve kanıtlar. Bu yöntemin uygulanabilmesi için açık kaynaklı, kolay entegre edilebilir, esnek, geniş kapsamlı Verilog desteği sunan bir sentez çerçevesi olan Yosys ile Yosys tabanlı Symbiyosys aracı kullanılmıştır. Bu tezde tasarım gereksinimlerine göre uygun, Symbiyosys'in kullanım desteği olan SystemVerilog Donanım Doğrulama Dili ve SystemVerilog Assertion kullanılarak tasarımdaki hatalar tespit edilmiştir. Formal Doğrulama sayesinde, I2C tasarımlarının olduğu havacılık operasyonlarının sorunsuz bir şekilde devam etmesini sağlayarak sorunların yaşanmasını engeller.
Özet (Çeviri)
Aerospace Industry has many aviation applications that involve vast number of subsystems. Therefore, the need of reliable data communication between devices and components is a critical subject. In this context, I2C communication protocol is widely preferred over other protocols in terms of high speed, flexibility, low power consumption and reliability. However, issues such as data corruption, data loss, slow data transmission may occur in I2C data transmission. These problems can lead to serious consequences in the aviation industry, such as safety risks at multiple levels, electronic problems, air traffic management issues, and incorrect navigation information. Therefore, it is an important requirement that the I2C RTL design be written completely and without errors and also verified. The I2C master design in this thesis was downloaded from OpenCores. There are several verification methods for digital design verification. Formal Verification, which will be used for this thesis, is one of the most precise and reliable methods, especially in critical systems. This method is a significant method that mathematically proves that the design complies with certain features and requirements by saving time. This method checks and proves that the design meets specific features and requirements, providing a mathematical proof while saving time and costs. Yosys, an open source, easily integrated, flexible, synthesis framework that offers comprehensive Verilog support, and the Yosys-based Symbiyosys tool were used to implement this method. In this thesis, using the SystemVerilog Hardware Verification Language and SystemVerilog Assertion supported by Symbiyosys, design errors have been detected according to the design requirements. Thanks to Formal Verification, it prevents problems by ensuring that avionic operations with I2C designs continue smoothly.
Benzer Tezler
- The implementation of a direct digital synthesis based function generator using systemc and VHDL
Doğrudan sayısal sentez tabanlı fonksiyon üretecinin systemc ve VHDL kullanılarak gerçeklenmesi
UĞUR KAZANCIOĞLU
Yüksek Lisans
İngilizce
2007
Elektrik ve Elektronik MühendisliğiOrta Doğu Teknik ÜniversitesiElektrik ve Elektronik Mühendisliği Ana Bilim Dalı
PROF. DR. MURAT AŞKAR
- Formal verification and controller synthesis for discrete-time systems
Başlık çevirisi yok
EBRU AYDIN GÖL
Doktora
İngilizce
2014
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolBoston UnıversıtyPROF. CALIN BELTA
- FPFM: A formal specification and verification framework for security policies in multi-domain mobile networks
FPFM: Çok etki alanlı gezgin ağlarda güvenlik politikaları betimleme ve doğrulama çerçevesi
DEVRİM ÜNAL
Doktora
İngilizce
2011
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolBoğaziçi ÜniversitesiBilgisayar Mühendisliği Ana Bilim Dalı
PROF. DR. MEHMET UFUK ÇAĞLAYAN
- Specification and formal verification of fuzzy information processing for the case of edge detection
Kenar algılama durumu icin bulanık bilgi işlemenin belirlenmesi ve resmi olarak doğrulanması
KEMAL KESKİN
Yüksek Lisans
İngilizce
2009
Elektrik ve Elektronik MühendisliğiNortheastern UnıversıtyElektrik ve Bilgisayar Mühendisliği Ana Bilim Dalı
PROF. DR. MİECZYSLAW MİTCH KOKAR
