Generating libraries of highly correct and safe functions by using proof-based formal methods
İspat-tabanlı yazılım doğruluğu ve güvenilirliğini gösterme tekniklerini kullanarak güvenilir bir kütüphane oluşturmak
- Tez No: 374441
- Danışmanlar: YRD. DOÇ. DR. AYTEKİN VARGÜ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: 2014
- Dil: İngilizce
- Üniversite: Melikşah Üniversitesi
- Enstitü: Fen Bilimleri Enstitüsü
- Ana Bilim Dalı: Elektrik ve Bilgisayar Mühendisliği Ana Bilim Dalı
- Bilim Dalı: Belirtilmemiş.
- Sayfa Sayısı: 120
Özet
Bu tezde, büyük ölçekli yazılım oluşturabilmek için kullanılabilecek yüksek düzeyde doğruluğa sahip ve güvenilir fonksyonların formal tanımlarından oluşan bir kütüphane üretildi. Büyük programların doğruluğunu ve güvenliğini ispatlamak zor olmasına ragmen, eğer kendisinin bileşenlerinin doğruluğu ve/veya güvenliği önceden gösterilebilirse bu işlem yapılabilir. Benzer bir yaklaşım STL'nin pek çok kullanışlı küçük ölçekli prosedürler ve fonksiyonlar sağladığı C++'ta kullanılmaktadır. Yazılım doğruluğunu kontrol etmek için en güçlü yöntemlerden biri formal yöntemleri kullanmaktır. Bu araştırmada, programların özelliklerini yazmak ve onların tanımlanan özellikler açısından doğru ve güvenli olduğunu ispatlamak için Athena isimli bir teorem ispatlayıcı kullanılmıştır. Aksiyomatik tanımlar ve ispatlar prefix notasyonu ile karşılaştırıldığında daha okunabilir ve kısa ifadelerin yazılmasını sağlayan infix notasyonunda yapılmıştır. Athena'da CODEGEN adı verilen bir program, aksiyomlar ve teoremlerden kod üretmek için kullanılabilmektedir. Fakat bu program sadece prefix notasyonundaki tanımlarla çalışır. Onun infix notasyonlarla çalışmasını mümkün kılmak için aksiyomatik tanımları infix notasyonundan prefix notasyonuna dönüştüren bir program Java'da yazılmıştır. Son olarak bu tezde infix notasyonuyla bellek tanımı yapılmış ve böylelikle bellekte güncelleme yapan programların üretilmesi sağlanmıştır.
Özet (Çeviri)
In this thesis, a specification library of highly correct and safe functions which can be used to compose large scale software is constructed. Although it is hard to prove the correctness and safety of large programs, it can be done if the correctness and/or safety of its components are shown beforehand. A similar approach is used in C++ where STL provides many useful small-scale procedures and functions. One of the strongest methods to verify software correctness is to use formal methods. In this research, Athena has been used as a theorem prover to write specifications of programs and prove that they are correct and safe with respect to the given specifications. The axiomatic definitions and the proofs are written in infix notation which makes them more readable and shorter with respect to the prefix notation. In Athena a program called CODEGEN can be used to extract code from the axioms and theorems. But it only works with the definitions in the prefix notation. In order to make it work with the infix definitions, a program that converts axiomatic definitions in infix notation to prefix notation is implemented in Java. The last contribution of this thesis is to define memory by using the infix notation to make it possible to generate code that updates memory locations.
Benzer Tezler
- Olasılıksal modeller ile Türkçe müzik türlerinin sınıflandırılması
Classification of Turkish music genres with probabilistic models
MEHMET CÜNEYT ÖZBALCI
Yüksek Lisans
Türkçe
2022
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolBursa Teknik ÜniversitesiBilgisayar Mühendisliği Ana Bilim Dalı
PROF. DR. TURGAY TUGAY BİLGİN
- Okunabilir kopyalama algoritmalı DSM sisteminin gerçeklenmesi
Başlık çevirisi yok
ÖZGÜR KORAY ŞAHİNGÖZ
Yüksek Lisans
Türkçe
1998
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİstanbul Teknik ÜniversitesiKontrol ve Bilgisayar Mühendisliği Ana Bilim Dalı
DOÇ. DR. TAKUHİ NADİA ERDOĞAN
- Selection, design & applications of solid binding peptides for controlled biomineralization
Kontrollü biyomineralizasyon için katı yüzeylere bağlanan peptitlerin seçimi, tasarımı ve uygulamaları
MUSTAFA GÜNGÖRMÜŞ
Doktora
İngilizce
2012
BiyomühendislikUniversity of WashingtonMalzeme Bilimi ve Mühendisliği Ana Bilim Dalı
PROF. DR. MEHMET SARIKAYA
- Mimari bir dilin biçim grameri analizi ve bilgisayar ortamında sunumu
Başlık çevirisi yok
EDA VELİBAŞOĞLU
- A web mapping infrastructure design and implementation with open source geo information technology: A case study of ITU Smart Campus
Web haritalama alt yapı tasarımı ve açık kaynak kodlu coğrafi bilgi teknolojileri ile İTÜ Akıllı Kampüs uygulaması çalışması
ROUHOLLAH NASIRZADEHDIZAJI
Yüksek Lisans
İngilizce
2015
Jeodezi ve Fotogrametriİstanbul Teknik ÜniversitesiCoğrafi Bilgi Teknolojileri Ana Bilim Dalı
PROF. DR. RAHMİ NURHAN ÇELİK