CENG 651

Güvenlik İçin Formal Yöntemler

Bu ders, emniyet ve güvenlik açısından kritik uygulamalar için biçimsel yöntemlerin yazılım mühendisliği yöntemleri ile nasıl kullanılacağını gösterecektir. Bu ders içinde konuya özel CSP süreç algebrası ve Zamansal Mantık gibi biçimsel ifade yöntemleri ile system modelleme ve doğrulama araçları açıklanacaktır. Ayrıca, ders içinde biçimsel yöntemlerin sistemlerin emniyet ve güvenlik özelliklerinin analizinde kullanım şekli de araştırılacaktır.

Dersin Amacı:

Yazılım mühendisliği alanında emniyet ve güvenlik için kullanılan biçimsel yöntemleri öğretmek. Emniyet ve güvenlik için yazılım mühendisliği alanında kullanılan algoritmaları tanıtmak ve bu algoritmaları gerçekleme becerisi geliştirmek. Bu alandaki uygulamalara yakınlık kazandırmak. Dönem projesi ile raporlama ve sunma becerisi geliştirmek.

Kaynakça:

B. Bérard et al.. Systems and Software Verification, Model Checking Techniques and Tools, Springer-Verlag, 2001

Öğrenme Çıktıları:

1. Yazılım mühendisliği alanında emniyet ve güvenlik için kullanılan biçimsel yöntemleri ile ilgili temel kavramları açıklayabilme

2. Yazılım mühendisliği alanında emniyet ve güvenlik için kullanılan güncel biçimsel yöntemleri tanıma

3. Yazılım sistemleri için emniyet ve güvenlik ile ilgili algoritmaları gerçekleyebilme

4. Yapılan çalışmaları raporlayabilme ve sunabilme

Konular
Biçimsel Yöntemlere Giriş
Önerme ve Betimleme Mantıkları
Program Doğrulama
Program Doğrulama
CSP süreç algebrası
Protokol Doğrulama
Model Denetimi
Otomata ile Sistem Modelleme
Zamansal Mantık ile Sistem Özellikleri Tanımlama
Model Denetimi Algoritmaları
Model Denetimi Algoritmaları
Sembolik Model Denetimi
Soyutlama Yöntemleri
SPIN Model Denetim Aracı

Notlandırma:

Vize: 30%

Ödev: 10%

Araştırma Sunumu: 30%

Final: 30%