Yazılımların formal yöntemler ile doğrulanması ve geçerlilenmesi
Formal verification and validation of software
- Tez No: 155413
- Danışmanlar: Y.DOÇ.DR. ALİ ZİYA ALKAR
- Tez Türü: Yüksek Lisans
- Konular: Elektrik ve Elektronik Mühendisliği, Electrical and Electronics Engineering
- Anahtar Kelimeler: SCR, CTL Yapılar, Mod Grafiği (Modechart), Sembolik Model Kontrolü, CTL Formül, SCR, CTL Structures, Modechart, Symbolic Model Checking, CTL Formula
- Yıl: 2004
- Dil: Türkçe
- Üniversite: Hacettepe Üniversitesi
- Enstitü: Fen Bilimleri Enstitüsü
- Ana Bilim Dalı: Elektrik-Elektronik Mühendisliği Ana Bilim Dalı
- Bilim Dalı: Belirtilmemiş.
- Sayfa Sayısı: 133
Özet
YAZILIMLARIN FORMAL YÖNTEMLER İLE DOĞRULANMASI VE GEÇERLİLENMESİ Mustafa ŞAHİNOĞLU ÖZ Bu çalışmada, yazılımların doğrulanması ve geçerlilenmesi hakkında bilgi ve metotlar verilmiş, verilen bilgiler doğrultusunda yazılımların doğruluğunu kontrol edebilen bir yazılım aracı geliştirilmiştir. Çalışma, yazılımların gereklerinin nasıl modellendiğini anlatmakta ve bu modellerden faydalanarak, yazılımların istenilen gereklere uyup uymadığına bakılmasını araştırmaktadır. Yazılım gereklerinin belirlenmesi aşamasında SCR (Software Cost Reduction) gerek belirleme yönteminden faydalanılmıştır. Bu gerek yönteminin kullanımı ve CTL (Computation Tree Logic) yapılar kullanılarak, gereklerin modellenmesi örneklerle verilmiştir. Gerçek zamanlı sistemleri modellemek için kullanılan mod grafikleri (Modechart) ve geçerleme yöntemi de çalışma kapsamı içinde incelenmiştir. Gereklerden meydana getirilen sistem modelinin formal yöntemler ile gösterimini ve formal yöntemler ile doğrulanmasını sağlayan“sembolik model kontrol yöntemi”araştırılmış ve bu yöntemden yola çıkılarak, CTL formüllerin ve CTL yapıların kullanıldığı, bilgisayar ortamında çalışabilen bir program geliştirilmiştir.
Özet (Çeviri)
FORMAL VERIFICATION AND VALIDATION OF SOFTWARE Mustafa ŞAHİNO?LU ABSTRACT In this study, the methods of verifying and validating software are explained and a program that checks the validity of the software has been developed. In the first phase of this thesis study, we looked into the requirements that form a software program and modelled these requiements. After the modelling phase is completed, these requirements are checked with respect to the software in target. While developing the software requirements, SCR (Software Cost Reduction) requirement development method has been used. The application of this method and explanation on how these requirements modelled by using CTL structures are given by examples. Modechart method is used for modelling real time systems, and its formal verification methods are investigated in the scope of this study. In this thesis, the method of supporting the formal representation of the system models which are constructed by the requirements and their verification by formal methods called Symbolic Model Checking has also been investigated. Using this method, a software program has been developed where CTL structures and CTL formula are used.
Benzer Tezler
- Analysis of mobile bim adoption at construction site: A case study of a complex infrastructure project
İnşaat sahasında mobil bım adaptasyonunun analizi: Kompleks altyapı projesi vaka analizi
ELİF TUĞÇE NURTAN GÜNEŞ
Yüksek Lisans
İngilizce
2018
İnşaat Mühendisliğiİstanbul Teknik Üniversitesiİnşaat Mühendisliği Ana Bilim Dalı
DOÇ. DR. ESİN ERGEN PEHLEVAN
DR. OZAN KÖSEOĞLU
- Anklaşman sistemi yazılım modelinin model sınamasının yapılması
Model verification of interlocking software model
DAVUT POLAT
Yüksek Lisans
Türkçe
2015
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİstanbul Teknik ÜniversitesiBilgisayar Mühendisliği Ana Bilim Dalı
YRD. DOÇ. DR. TOLGA OVATMAN
- Gevşetilmiş bellek modelleri üstünde çalışan proğramlarin doğruluğunun kontrolu için durağan yöntemler
Static methods for checking correctness of programs on relaxed memory systems
İSMAİL KURU
Yüksek Lisans
İngilizce
2015
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolKoç ÜniversitesiBilgisayar Bilimleri ve Mühendisliği Ana Bilim Dalı
DOÇ. DR. SERDAR TAŞIRAN
- Turbopompa beslemeli sıvı yakıtlı roket motorları için kriyojenik pompa tasarım ve çark optimizasyon aracı oluşturulması
Development of cryogenic pump design and impeller optimization tool for turbopump-fed liquid propellant rocket engines
MUHAMMED BATUHAN KÖROĞLU
Yüksek Lisans
Türkçe
2023
Makine Mühendisliğiİstanbul Teknik ÜniversitesiMakine Mühendisliği Ana Bilim Dalı
PROF. DR. SEYHAN ONBAŞIOĞLU
- An IFC-based framework for sustainable construction
Sürdürülebilir yapım için IFC-tabanlı bir yaklaşım
BAHRİYE İLHAN