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ı: Belirtilmemiş.
Ö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
- A Model for representing texts script theory
Başlık çevirisi yok
ÇİĞDEM KEYDER
Yüksek Lisans
İngilizce
1990
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolOrta Doğu Teknik ÜniversitesiBilgisayar Mühendisliği Ana Bilim Dalı
DOÇ. DR. MÜREN GÖKERİ
- Bilgi sistemlerinin çözümlenmesi (jeodezik bilgi sistemi)
Analyzing information systems (geodetic information system)
YALKIN ÇAĞLAR
Yüksek Lisans
Türkçe
2002
Jeodezi ve Fotogrametriİstanbul Teknik ÜniversitesiJeodezi ve Fotogrametri Ana Bilim Dalı
PROF. DR. ORHAN ALTAN
- Veri ambarı oluşumunda kullanılan teknolojilerin incelenmesi ve veri ambarlarının kişiye özel üretimde kullanımı
Examination of technologies used for building data warehouses and use of data warehouses in mass customization
ŞEFİK EĞRİBOZ
Yüksek Lisans
Türkçe
2002
İşletmeİstanbul Teknik Üniversitesiİşletme Mühendisliği Ana Bilim Dalı
DR. HALİL HALEFŞAN SÜMEN
- Bilişim teknolojilerinin olanakları ile dijital olarak yeniden üretilip ağlarla dağıtılabildiği çağda sanat yapıtı
Başlık çevirisi yok
İBRAHİM ORTON AKINCI
Yüksek Lisans
Türkçe
2004
Güzel SanatlarYıldız Teknik ÜniversitesiSanat ve Tasarım Ana Bilim Dalı
Y.DOÇ.DR. İNCİ EVİNER