YAZILIM MÜHENDİSLİĞİ (İNGİLİZCE)
Lisans TYYÇ: 6. Düzey QF-EHEA: 1. Düzey EQF-LLL: 6. Düzey

Ders Genel Tanıtım Bilgileri

Ders Kodu: 1413002016
Ders İsmi: Formal Verifikasyon
Ders Yarıyılı: Bahar
Ders Kredileri:
Teorik Pratik Kredi AKTS
3 0 3 5
Öğretim Dili: EN
Ders Koşulu:
Ders İş Deneyimini Gerektiriyor mu?: Hayır
Dersin Türü: Department Elective
Dersin Seviyesi:
Lisans TYYÇ:6. Düzey QF-EHEA:1. Düzey EQF-LLL:6. Düzey
Dersin Veriliş Şekli: Yüz yüze
Dersin Koordinatörü: Dr.Öğr.Üyesi Adem ÖZYAVAŞ
Dersi Veren(ler):
Dersin Yardımcıları:

Dersin Amaç ve İçeriği

Dersin Amacı: Bu ders sırasında, bir sistemin davranışını resmi olarak nasıl belirleyeceğinizi, bunu nasıl kanıtlayacağınızı öğreneceksiniz.
sistemin üst düzey tasarımı, bu spesifikasyonu karşılar ve son olarak,
sistemin düşük seviye uygulaması bu özellikleri korur. Kurs herhangi bir varsayımda bulunmaz
resmi doğrulamada ön bilgi. Dafny dilinin temellerinden başlayacağız ve
oradan inşa et. Sonunda, karmaşık bir sistemi tasarlayabilmeli ve doğruluğunu kanıtlayabilmelisiniz.
Dersin İçeriği: Bu derste, tamamen öğreneceksiniz
sağlam yazılım oluşturmanın farklı bir yolu: hatasız olduğu resmi olarak kanıtlanmış bir kod yazarak.
Karmaşık tasarımın nasıl yapılacağına odaklanarak bu soruna sistem perspektifinden yaklaşacağız.
(genellikle dağıtılmış) sistemler, yine de doğrulukları hakkında akıl yürütebilir. Aynı
zaman, sınıf size en umut verici araçlardan biri olan Dafny ile uygulamalı deneyim verecektir.
sistem yazılımının pratik resmi doğrulaması.

Öğrenme Kazanımları

Bu dersi başarıyla tamamlayabilen öğrenciler;
Öğrenme Kazanımları
1 - Bilgi
Kuramsal - Olgusal
1) Resmi doğrulamanın temellerini (şartname, kanıt, değişmezler, vb.) anlayın.
2 - Beceriler
Bilişsel - Uygulamalı
1) Endüktif değişmez kavramını ve nasıl bulunacağını anlayın
2) Protokol düzeyinde bir durum makinesinin doğruluğunu kanıtlayabilme
3) İyileştirme kavramını anlayın ve karmaşık bir sistemde iyileştirmeye dayalı bir kanıt gerçekleştirebileceksiniz.
3 - Yetkinlikler
İletişim ve Sosyal Yetkinlik
Öğrenme Yetkinliği
Alana Özgü Yetkinlik
Bağımsız Çalışabilme ve Sorumluluk Alabilme Yetkinliği

Ders Akış Planı

Hafta Konu Ön Hazırlık
1) Introduction to Formal Verification Formal Verification by Erik Seligman, Tom Schubert, M Kumar Released July 2015 Publisher(s): Morgan Kaufmann ISBN: 9780128008157
2) veri türleri, yüklemler, iddialar Formal Verification by Erik Seligman, Tom Schubert, M Kumar Released July 2015 Publisher(s): Morgan Kaufmann ISBN: 9780128008157
3) özyineleme, döngü değişmezleri Formal Verification by Erik Seligman, Tom Schubert, M Kumar Released July 2015 Publisher(s): Morgan Kaufmann ISBN: 9780128008157
4) Şartname ve durum makineleri Formal Verification by Erik Seligman, Tom Schubert, M Kumar Released July 2015 Publisher(s): Morgan Kaufmann ISBN: 9780128008157
5) Kanıtlama özellikleri ve endüktif değişmezler Formal Verification by Erik Seligman, Tom Schubert, M Kumar Released July 2015 Publisher(s): Morgan Kaufmann ISBN: 9780128008157
6) Dağıtılmış ve zaman uyumsuz sistemlerin modellenmesi Formal Verification by Erik Seligman, Tom Schubert, M Kumar Released July 2015 Publisher(s): Morgan Kaufmann ISBN: 9780128008157
7) İlk bölümün özeti Formal Verification by Erik Seligman, Tom Schubert, M Kumar Released July 2015 Publisher(s): Morgan Kaufmann ISBN: 9780128008157
8) Arasinav Formal Verification by Erik Seligman, Tom Schubert, M Kumar Released July 2015 Publisher(s): Morgan Kaufmann ISBN: 9780128008157
9) Eşzamansız özellikler Formal Verification by Erik Seligman, Tom Schubert, M Kumar Released July 2015 Publisher(s): Morgan Kaufmann ISBN: 9780128008157
10) Eşzamansız özellikler (devam) Formal Verification by Erik Seligman, Tom Schubert, M Kumar Released July 2015 Publisher(s): Morgan Kaufmann ISBN: 9780128008157
11) Durum makineleri ve davranışlar değişmezleri ve Dağıtılmış ve zaman uyumsuz sistemlerin modellenmesi Formal Verification by Erik Seligman, Tom Schubert, M Kumar Released July 2015 Publisher(s): Morgan Kaufmann ISBN: 9780128008157
12) Modüller ve otomasyon Formal Verification by Erik Seligman, Tom Schubert, M Kumar Released July 2015 Publisher(s): Morgan Kaufmann ISBN: 9780128008157
13) Ana bilgisayarlar arası eşzamanlılık Formal Verification by Erik Seligman, Tom Schubert, M Kumar Released July 2015 Publisher(s): Morgan Kaufmann ISBN: 9780128008157
14) Sistem doğrulamanın geleceği Formal Verification by Erik Seligman, Tom Schubert, M Kumar Released July 2015 Publisher(s): Morgan Kaufmann ISBN: 9780128008157
15) Final Formal Verification by Erik Seligman, Tom Schubert, M Kumar Released July 2015 Publisher(s): Morgan Kaufmann ISBN: 9780128008157

Kaynaklar

Ders Notları / Kitaplar: Formal Verification
by Erik Seligman, Tom Schubert, M Kumar
Released July 2015
Publisher(s): Morgan Kaufmann
ISBN: 9780128008157
Diğer Kaynaklar: Formal Verification
by Erik Seligman, Tom Schubert, M Kumar
Released July 2015
Publisher(s): Morgan Kaufmann
ISBN: 9780128008157

Ders - Program Öğrenme Kazanım İlişkisi

Ders Öğrenme Kazanımları

1

2

3

4

Program Kazanımları
1) Matematik, fen bilimleri ve bilgisayar mühendisliği konularında yeterli bilgi birikimi; bu alanlardaki kuramsal ve uygulamalı bilgileri mühendislik problemlerini modelleme ve çözme için uygulayabilme becerisi.
2) Karmaşık mühendislik problemlerini saptama, tanımlama, formüle etme ve çözme becerisi; bu amaçla uygun analiz ve modelleme yöntemlerini seçme ve uygulama becerisi.
3) Karmaşık bir sistemi, süreci, cihazı veya ürünü gerçekçi kısıtlar ve koşullar altında, belirli gereksinimleri karşılayacak şekilde tasarlama becerisi; bu amaçla modern tasarım yöntemlerini uygulama becerisi.
4) Mühendislik uygulamalarında karşılaşılan karmaşık problemlerin analizi ve çözümü için gerekli olan modern teknik ve araçları geliştirme, seçme ve kullanma becerisi; bilişim teknolojilerini etkin bir şekilde kullanma becerisi.
5) Karmaşık mühendislik problemlerinin veya disipline özgü araştırma konularının incelenmesi için deney tasarlama, deney yapma, veri toplama, sonuçları analiz etme ve yorumlama becerisi.
6) Disiplin içi ve çok disiplinli takımlarda etkin biçimde çalışabilme becerisi; bireysel çalışma becerisi.
7) Türkçe sözlü ve yazılı etkin iletişim kurma becerisi; en az bir yabancı dil bilgisi; etkin rapor yazma ve yazılı raporları anlama, tasarım ve üretim raporları hazırlayabilme, etkin sunum yapabilme, açık ve anlaşılır talimat verme ve alma becerisi.
8) Yaşam boyu öğrenmenin gerekliliği bilinci; bilgiye erişebilme, bilim ve teknolojideki gelişmeleri izleme ve kendini sürekli yenileme becerisi.
9) Etik ilkelerine uygun davranma, mesleki ve etik sorumluluk bilinci; mühendislik uygulamalarında kullanılan standartlar hakkında bilgi.
10) Proje yönetimi, risk yönetimi ve değişiklik yönetimi gibi, iş hayatındaki uygulamalar hakkında bilgi; girişimcilik, yenilikçilik hakkında farkındalık; sürdürülebilir kalkınma hakkında bilgi.
11) Mühendislik uygulamalarının evrensel ve toplumsal boyutlarda sağlık, çevre ve güvenlik üzerindeki etkileri ve çağın mühendislik alanına yansıyan sorunları hakkında bilgi; mühendislik çözümlerinin hukuksal sonuçları konusunda farkındalık.

Ders - Öğrenme Kazanımı İlişkisi

Etkisi Yok 1 En Düşük 2 Düşük 3 Orta 4 Yüksek 5 En Yüksek
           
Dersin Program Kazanımlarına Etkisi Katkı Payı
1) Matematik, fen bilimleri ve bilgisayar mühendisliği konularında yeterli bilgi birikimi; bu alanlardaki kuramsal ve uygulamalı bilgileri mühendislik problemlerini modelleme ve çözme için uygulayabilme becerisi.
2) Karmaşık mühendislik problemlerini saptama, tanımlama, formüle etme ve çözme becerisi; bu amaçla uygun analiz ve modelleme yöntemlerini seçme ve uygulama becerisi.
3) Karmaşık bir sistemi, süreci, cihazı veya ürünü gerçekçi kısıtlar ve koşullar altında, belirli gereksinimleri karşılayacak şekilde tasarlama becerisi; bu amaçla modern tasarım yöntemlerini uygulama becerisi.
4) Mühendislik uygulamalarında karşılaşılan karmaşık problemlerin analizi ve çözümü için gerekli olan modern teknik ve araçları geliştirme, seçme ve kullanma becerisi; bilişim teknolojilerini etkin bir şekilde kullanma becerisi.
5) Karmaşık mühendislik problemlerinin veya disipline özgü araştırma konularının incelenmesi için deney tasarlama, deney yapma, veri toplama, sonuçları analiz etme ve yorumlama becerisi.
6) Disiplin içi ve çok disiplinli takımlarda etkin biçimde çalışabilme becerisi; bireysel çalışma becerisi.
7) Türkçe sözlü ve yazılı etkin iletişim kurma becerisi; en az bir yabancı dil bilgisi; etkin rapor yazma ve yazılı raporları anlama, tasarım ve üretim raporları hazırlayabilme, etkin sunum yapabilme, açık ve anlaşılır talimat verme ve alma becerisi.
8) Yaşam boyu öğrenmenin gerekliliği bilinci; bilgiye erişebilme, bilim ve teknolojideki gelişmeleri izleme ve kendini sürekli yenileme becerisi.
9) Etik ilkelerine uygun davranma, mesleki ve etik sorumluluk bilinci; mühendislik uygulamalarında kullanılan standartlar hakkında bilgi.
10) Proje yönetimi, risk yönetimi ve değişiklik yönetimi gibi, iş hayatındaki uygulamalar hakkında bilgi; girişimcilik, yenilikçilik hakkında farkındalık; sürdürülebilir kalkınma hakkında bilgi.
11) Mühendislik uygulamalarının evrensel ve toplumsal boyutlarda sağlık, çevre ve güvenlik üzerindeki etkileri ve çağın mühendislik alanına yansıyan sorunları hakkında bilgi; mühendislik çözümlerinin hukuksal sonuçları konusunda farkındalık.

Öğrenme Etkinliği ve Öğretme Yöntemleri

Bireysel çalışma ve ödevi
Ders
Grup çalışması ve ödevi
Ödev
Proje Hazırlama
Rapor Yazma

Ölçme ve Değerlendirme Yöntemleri ve Kriterleri

Ölçme ve Değerlendirme

Yarıyıl İçi Çalışmaları Aktivite Sayısı Katkı Payı
Ödev 8 % 15
Projeler 1 % 15
Ara Sınavlar 1 % 30
Yarıyıl/Yıl Sonu Sınavı 1 % 40
Toplam % 100
YARIYIL İÇİ ÇALIŞMALARININ BAŞARI NOTU KATKISI % 60
YARIYIL SONU ÇALIŞMALARININ BAŞARI NOTUNA KATKISI % 40
Toplam % 100

İş Yükü ve AKTS Kredisi Hesaplaması

Aktiviteler Aktivite Sayısı Süre (Saat) İş Yükü
Ders Saati 14 3 42
Sınıf Dışı Ders Çalışması 14 3 42
Proje 1 20 20
Ödevler 8 12 96
Ara Sınavlar 1 2 2
Final 1 3 3
Toplam İş Yükü 205