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ı: Belirtilmemiş.
Ö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
- Mimari tasarım eğitimi tasarım bilgisi bağlamında stüdyo eleştirileri
Architectural design education: Design knowledge cummunicated in studio critiques
BELKIS ULUOĞLU
- Dokuma kumaşlarda örgü tipinin ham kumaşın boyutları ve geometrik özellikleri üzerindeki etkilerinin araştırılması
Başlık çevirisi yok
EMEL ÖNDER
Yüksek Lisans
Türkçe
1985
Tekstil ve Tekstil MühendisliğiEge ÜniversitesiTekstil Mühendisliği Ana Bilim Dalı
DOÇ. DR. GÜNGÖR BAŞER
- Barajların hacim-verim ilişkisi üzerine bir araştırma
Başlık çevirisi yok
MEHMET KILIÇARSLAN
Yüksek Lisans
Türkçe
1987
İnşaat MühendisliğiÇukurova Üniversitesiİnşaat Mühendisliği Ana Bilim Dalı
DOÇ. DR. TEFARUK HAKTANIR
- Kemalpaşa etlik piliç işletmelerinin teknik ve ekonomik yönden incelenmesi
Başlık çevirisi yok
HAYRİ TUNA YÜKSELEN
- Toz kakaoda tağşiş saptama metodları üzerinde çalışmalar
Başlık çevirisi yok
TOMRİS ALTUĞ
Doktora
Türkçe
1987
Gıda MühendisliğiEge ÜniversitesiGıda Mühendisliği Ana Bilim Dalı
YRD. DOÇ. DR. MERAL GÖNÜL