Bir görsel modelleme aracı için doğrulanmış kod üretimi

---

Tezin Türü: Yüksek Lisans

Tezin Yürütüldüğü Kurum: Orta Doğu Teknik Üniversitesi, Fen Bilimleri Enstitüsü, BİLGİSAYAR MÜHENDİSLİĞİ ANABİLİM DALI, Türkiye

Tezin Onay Tarihi: 2024

Tezin Dili: İngilizce

Öğrenci: EBRU ÇELEBİ

Danışman: Mehmet Halit S. Oğuztüzün

Açık Arşiv Koleksiyonu: AVESİS Açık Erişim Koleksiyonu

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