Verified code generation for a visual modeling tool
Bir görsel modelleme aracı için doğrulanmış kod üretimi
- Tez No: 892351
- Danışmanlar: PROF. DR. MEHMET HALİT SEYFULLAH OĞUZTÜZÜN
- Tez Türü: Yüksek Lisans
- Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Computer Engineering and Computer Science and Control
- Anahtar Kelimeler: Belirtilmemiş.
- Yıl: 2024
- Dil: İngilizce
- Üniversite: Orta Doğu Teknik Üniversitesi
- Enstitü: Fen Bilimleri Enstitüsü
- Ana Bilim Dalı: Bilgisayar Mühendisliği Ana Bilim Dalı
- Bilim Dalı: Belirtilmemiş.
- Sayfa Sayısı: 99
Özet
Bu tez, kullanıcıların ardışık bir hesaplamayı görsel olarak modellemelerini ve emniyet kritik yazılım sisteminin parçası olmak üzere modelden kod üretmelerini sağlayan IMODE aracı için doğrulanmış bir kod üreticisi sunmaktadır. Üretilen kod, herhangi bir yan etki olmadan modeldeki hesaplamaları olduğu gibi gerçekleştirmeli ve uygulanacak emniyet kritik standartlarına uygun olmalıdır. Kod üreticisi şu aşamalardan geçer: (i) Model girdisini IMODE XML kayıt dosyaları ile alır; (ii) Girdi modelin bütünlük ve yapısının düzgünlüğünü kontrol eder; (iii) Modeli, model öğeleri tarafından etkilenen giriş-çıkış ilişkilerini yakalayan mantıksal ifadelerle açıklar; (iv) C dilinin alt kümesinde kod üretir; (v) Üretilen kodu, modelin mantıksalifadeleriyle oluşturulan ön ve son koşullarını kullanarak Hoare mantığı ile doğrularve son olarak (vi) üretilen kodu çıkarır. Kod üreticisinin kendi doğruluğunu sağlamak için, Agda programlama dili, bağımlı tiplere sahip bir fonksiyonel programlama dili, kullanıldı. Agda'nın bütünleşik teorem ispatlayıcısı kullanılarak kod üreticisi yapısı ile doğru yaklaşımına uygun olarak kanıtlanmıştır.
Özet (Çeviri)
This thesis introduces a verified code generator for the IMODE tool, which enables users to model a sequential computation visually and to generate executable code from the model that will be part of a safety critical software system. The generated code must carry out exactly the computation modeled without any side effects and must be compliant to the applicable safety critical software standards. The code generator goes through the following stages: (i) It takes its model input from the IMODE XML save files, (ii) checks the input model for well-formedness, (iii) annotates it with logical expressions that capture the input-output relationships effected by the model elements, (iv) generates code in a subset of C, (v) verifies the generated code using Hoare logic, adopting the pre- and post-conditions derived from the annotated model, and, finally, (vi) outputs the verified code. To ensure the correctness of the code generator itself, the Agda programming language, a functional programming language with dependent types, has been used for implementation. Using the Agda's integrated theorem prover, the code generator is proved adhering to the correct-by-construction approach.
Benzer Tezler
- Offline stator resistance estimation for permanent magnet synchronous motor and real-time implementation using embedded coder
Kalıcı mıknatıslı senkron motorlar için offline stator direnci tahmini ve embedded koder kullanarak gerçek zamanlı uygulaması
LÜTFÜ EMRE EFE
Yüksek Lisans
İngilizce
2023
Elektrik ve Elektronik Mühendisliğiİstanbul Teknik ÜniversitesiElektrik Mühendisliği Ana Bilim Dalı
DOÇ. DR. SALİH BARIŞ ÖZTÜRK
- Karma gerçeklik ortamında parametrik tasarım ve robotik fabrikasyon yöntemi
Parametric design and robotic fabrication method within mixed-reality environment
YUSUF BUYRUK
Doktora
Türkçe
2023
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİstanbul Teknik ÜniversitesiBilişim Ana Bilim Dalı
PROF. DR. GÜLEN ÇAĞDAŞ
- Computational analysis of external store carriage in transonic speed regime
Harici yük taşımanın transonik sürat bölgesinde hesaplamalı analizi
İ. CENKER ASLAN
Yüksek Lisans
İngilizce
2003
Havacılık Mühendisliğiİstanbul Teknik ÜniversitesiUçak Mühendisliği Ana Bilim Dalı
DOÇ. DR. AYDIN MISIRLIOĞLU
PROF. DR. OKTAY BAYSAL
- Design of rotational parts using step AP224 features with automatic NC-code generation
Step 224 unsurları kullanarak dönel parça tasarımı ve otomatik NC-kod oluşturulması
KADİR AKKUŞ
Yüksek Lisans
İngilizce
2011
Makine MühendisliğiOrta Doğu Teknik ÜniversitesiMakine Mühendisliği Bölümü
PROF. DR. S. ENGİN KILIÇ
- Frezeleme işlemi sırasında iş parçasındaki sıcaklık dağılımının analizi
Thermal analysis of work piece during milling process
TAYGUN RECEP GÜNGÖR
Yüksek Lisans
Türkçe
2014
Makine Mühendisliğiİstanbul Teknik ÜniversitesiMakine Mühendisliği Ana Bilim Dalı
PROF. DR. MUSTAFA ÖZDEMİR