Geri Dön

Yazılımların formal yöntemler ile doğrulanması ve geçerlilenmesi

Formal verification and validation of software

  1. Tez No: 155413
  2. Yazar: MUSTAFA ŞAHİNOĞLU
  3. Danışmanlar: Y.DOÇ.DR. ALİ ZİYA ALKAR
  4. Tez Türü: Yüksek Lisans
  5. Konular: Elektrik ve Elektronik Mühendisliği, Electrical and Electronics Engineering
  6. 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
  7. Yıl: 2004
  8. Dil: Türkçe
  9. Üniversite: Hacettepe Üniversitesi
  10. Enstitü: Fen Bilimleri Enstitüsü
  11. Ana Bilim Dalı: Elektrik-Elektronik Mühendisliği Ana Bilim Dalı
  12. Bilim Dalı: Belirtilmemiş.
  13. 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

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

    İ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

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

    Türkçe

    2015

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİstanbul Teknik Üniversitesi

    Bilgisayar Mühendisliği Ana Bilim Dalı

    YRD. DOÇ. DR. TOLGA OVATMAN

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

    İngilizce

    2015

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolKoç Üniversitesi

    Bilgisayar Bilimleri ve Mühendisliği Ana Bilim Dalı

    DOÇ. DR. SERDAR TAŞIRAN

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

    Türkçe

    2023

    Makine Mühendisliğiİstanbul Teknik Üniversitesi

    Makine Mühendisliği Ana Bilim Dalı

    PROF. DR. SEYHAN ONBAŞIOĞLU

  5. An IFC-based framework for sustainable construction

    Sürdürülebilir yapım için IFC-tabanlı bir yaklaşım

    BAHRİYE İLHAN

    Doktora

    İngilizce

    İngilizce

    2014

    Mimarlıkİstanbul Teknik Üniversitesi

    Mimarlık Ana Bilim Dalı

    DOÇ. DR. HAKAN YAMAN