Geri Dön

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ı

  1. Tez No: 858824
  2. Yazar: MERVE BERİK
  3. Danışmanlar: PROF. DR. YAHYA KEMAL BAYKAL
  4. Tez Türü: Yüksek Lisans
  5. Konular: Elektrik ve Elektronik Mühendisliği, Electrical and Electronics Engineering
  6. Anahtar Kelimeler: Belirtilmemiş.
  7. Yıl: 2024
  8. Dil: İngilizce
  9. Üniversite: Çankaya Üniversitesi
  10. Enstitü: Fen Bilimleri Enstitüsü
  11. Ana Bilim Dalı: Elektrik ve Elektronik Mühendisliği Ana Bilim Dalı
  12. Bilim Dalı: Elektrik Elektronik Mühendisliği Bilim Dalı
  13. Sayfa Sayısı: 77

Ö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

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

    İngilizce

    2007

    Elektrik ve Elektronik MühendisliğiOrta Doğu Teknik Üniversitesi

    Elektrik ve Elektronik Mühendisliği Ana Bilim Dalı

    PROF. DR. MURAT AŞKAR

  2. Verification and validation of robotic systems's safety

    Robotik sistemlerin emniyetinin doğrulanması ve onaylanması

    ZEKERİYYA DEMİRCİ

    Yüksek Lisans

    Türkçe

    Türkçe

    2023

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolEskişehir Osmangazi Üniversitesi

    Bilgisayar Mühendisliği Ana Bilim Dalı

    PROF. DR. AHMET YAZICI

    DOÇ. DR. METİN ÖZKAN

  3. Design and implementation of a novel peer-to-peer approach to multipoint video conferencing

    Çok-noktalı video konferansın uçtan-uca tasarımı ve uygulanması

    TAHİR ÇELEBİ

    Yüksek Lisans

    İngilizce

    İngilizce

    2005

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

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

    DOÇ. DR. ÖZNUR ÖZKASAP

    PROF. REHA CİVANLAR

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

    İngilizce

    2011

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

    Bilgisayar Mühendisliği Ana Bilim Dalı

    PROF. DR. MEHMET UFUK ÇAĞLAYAN