CE 608 | Ders Tanıtım Bilgileri

Dersin Adı
Eşzamanlı Sistemlerin Formal Spesifikasyonu ve Doğrulanması
Kodu
Yarıyıl
Teori
(saat/hafta)
Uygulama/Lab
(saat/hafta)
Yerel Kredi
AKTS
CE 608
Güz/Bahar
3
0
3
7.5

Ön Koşul(lar)
Yok
Dersin Dili
İngilizce
Dersin Türü
Seçmeli
Dersin Seviyesi
Doktora
Dersin Koordinatörü -
Öğretim Eleman(lar)ı
Yardımcı(lar)ı -
Dersin Amacı Bu dersin amacı reaktif sistemlerin spesifikasyonlara uygun davranıp davranmadıklarının kesin bir şekilde doğrulanmasında kullanılan formalizmlerin derinlemesine incelenmesidir. Bu formalizmlerden bir kısmı matematiksel temellere bir kısmıda mantık temellerine dayanır. CCS ve CSP matematiksel temellere dayanan formal diller olup mantık mantık temeline dayanan nitelemeside vardır. Formal metodlar endüstride elektronik devre ve ağ protokollerinin doğrulanmısında başarı ile kullanılmışlardır. Protokollerinin doğrulanması dersde üzerinde durulacak bir alandır. Sistemler, bu konuda yazılmiş araçlar kullanılarak formal bir şekilde tanımlanıp doğrulanacaktır
Öğrenme Çıktıları Bu dersi başarıyla tamamlayabilen öğrenciler;
  • değişik spesifikasyon formalizmleri kullanarak, sistemlerin nasıl davranması gerektiğini değişik şekillerde ifade edebilirler.
  • davranışsal eşdeğerlilik kavramını oluşturan prensipleri açıklayabilirler.
  • modal mantık kullanarak sistemlerin özelliklerini belirtebilirler.
  • doğrulama araçlarını kullanarak tasarlanın sistemlerin, istenen özelliklere sahip olup olmadıklarını gösterebilirler.
  • karşılaştıkları bir doğrulama probleminde kullanılabilecekleri en faydalı formal teknikleri ve metodları seçebilirler.
Tanımı Bu ders eşzamanlı ve reaktif sistemlerin davranışları hakkında akıl yürütmekde kullanılan formal spesifikasyon tekniklerinin gözden geçirilmesi üzerinedir.

 



Ders Kategorisi

Temel Meslek Dersleri
Uzmanlık/Alan Dersleri
Destek Dersleri
İletişim ve Yönetim Becerileri Dersleri
Aktarılabilir Beceri Dersleri

 

HAFTALIK KONULAR VE İLGİLİ ÖN HAZIRLIK ÇALIŞMALARI

Hafta Konular Ön Hazırlık
1 Formal spesifikasyona ve doğrulamaya giriş. Formal metod ne demektir? Nerede ve niçin kullanılırlar? Test ile doğrulama arasındaki fark nedir? Okutman Yansıları
2 Formal spesifikasyon dilleri ve araçları Aceto et.al. “Reactive Systems: Modelling Specification and Verification”
3 LOTOS: Temporal sıralamaya dayanan bir spesifikasyon dili T Bolognesi, E Brinksma. "Introduction to the ISO specification language LOTOS" Computer Networks and ISDN systems, 1987.
4 Labelled transition systems Hoare. “Communicating Sequential Processes” Ch. 1.
5 Bir spesifikasyon dili CSP (Bağlantılı sıralı işlemler) Hoare. “Communicating Sequential Processes” Ch. 2-3.
6 Spesifikasyon dili CCS Robin Milner, “Communication and Concurrency” Ch. 1-3
7 Eşdeğerliliğe giriş ve CCS kullanarak doğrulamansı Robin Milner, “Communication and Concurrency” Ch. 4.
8 Eşdeğerli tabanlı doğrulama (devam) Robin Milner, “Communication and Concurrency” Ch. 4.
9 Midterm
10 CCSkullanarak prerorder tabanlı doğrulama Cleaveland and Steffen "A preorder for partial process specifications"LNCS, 1990, Vol 458, 141-151.
11 CCS dilinin mantıksal nitelemesi Robin Milner, “Communication and Concurrency”, Ch 10.
12 Manalı örnekler Aceto et.al. “Reactive Systems: Modelling Specification and Verification” pages 50 - 53
13 Makale sunumları -
14 Makale sunumları
15 Tekrar
16 -

 

Dersin Kitabı Okutman materyelleri
Diğer Kaynaklar 1) Luca Aceto, Anna Ingolfsdottir, Kim Larsen and Jiri Srba “Reactive Systems: Modelling Specification and Verification”, Cambridge University Press, 2007 2.) Robin Milner, “Communication and Concurrency”, (3rd ed.). Prentice Hall. 1989.3) C. A. R. Hoare. “Communicating Sequential Processes”, Prentice Hall,1985

 

DEĞERLENDİRME ÖLÇÜTLERİ

Yarıyıl İçi Çalışmaları Sayı Katkı Payı %
Derse Katılım
Laboratuvar / Uygulama
Arazi Çalışması
Küçük Sınavlar / Stüdyo Kritiği
Ödev
Sunum / Jüri Önünde Sunum
1
20
Proje
1
20
Çalıştay
Portfolyo
Ara Sınav / Sözlü Sınav
1
25
Final Sınavı / Sözlü Sınav
1
35
Toplam

Yarıyıl İçi Çalışmalarının Başarı Notuna Katkısı
3
65
Yarıyıl Sonu Çalışmalarının Başarı Notuna Katkısı
1
35
Toplam

AKTS / İŞ YÜKÜ TABLOSU

Aktiviteler Sayı Süresi (Saat) İş Yükü
Teorik Ders Saati
(Sınav haftası dahildir: 16 x toplam ders saati)
16
3
48
Laboratuvar / Uygulama Ders Saati
Sınav haftası dahil değildir. 16 x uygulama/lab ders saati
16
Sınıf Dışı Ders Çalışması
15
4
Arazi Çalışması
Küçük Sınavlar / Stüdyo Kritiği
Ödev
Sunum / Jüri Önünde Sunum
1
30
Proje
1
30
Çalıştay
Portfolyo
Ara Sınavlar / Sözlü Sınavlar
1
20
Final / Sözlü Sınav
1
37
    Toplam
225

 

DERSİN ÖĞRENME ÇIKTILARININ PROGRAM YETERLİLİKLERİ İLE İLİŞKİSİ

#
Program Yeterlilikleri / Çıktıları
* Katkı Düzeyi
1
2
3
4
5
1 Bilgisayar Mühendisliği alanında bilimsel araştırma yaparak bilgiye genişlemesine ve derinlemesine ulaşır, bilgiyi değerlendirir, yorumlar ve uygular. X
2 Bilgisayar Mühendisliği alanında uygulanan güncel teknik ve yöntemler ile bunların kısıtları hakkında kapsamlı bilgi sahibidir. X
3 Belirsiz, sınırlı ya da eksik verileri kullanarak, bilimsel yöntemlerle bilgiyi tamamlar ve uygular, değişik disiplinlere ait bilgileri bir arada kullanabilir. X
4 Mesleğinin yeni ve gelişmekte olan uygulamalarının farkındadır, ihtiyaç duyduğunda bunları inceler ve öğrenir. X
5 Bilgisayar Mühendisliği alanı ile ilgili problemleri tanımlar ve formüle eder, çözmek için yöntem geliştirir ve çözümlerde yenilikçi yöntemler uygular. X
6 Yeni ve/veya özgün fikir ve yöntemler geliştirir, karmaşık sistem veya süreçleri tasarlar ve tasarımlarında yenilikçi/alternatif çözümler geliştirir. X
7 Kuramsal, deneysel ve modelleme esaslı araştırmaları tasarlar ve uygular, bu süreçte karşılaşılan karmaşık problemleri irdeler ve çözümler. X
8 Disiplin içi ve çok disiplinli takımlarda etkin biçimde çalışabilir, bu tür takımlarda liderlik yapabilir ve karmaşık durumlarda çözüm yaklaşımları geliştirebilir, bağımsız çalışabilir ve sorumluluk alır. X
9 Bir yabancı dili en az Avrupa Dil Portföyü B2 Genel Düzeyinde kullanarak, sözlü ve yazılı iletişim kurar. X
10 Çalışmalarının süreç ve sonuçlarını, o alandaki veya alan dışındaki ulusal ve uluslararası ortamlarda sistematik ve açık bir şekilde yazılı ya da sözlü olarak aktarır. X
11 Bilgisayar Mühendisliği uygulamalarının sosyal, çevresel, sağlık, güvenlik, hukuk boyutları ile proje yönetimi ve iş hayatı uygulamalarını bilir ve bunların bilgisayar mühendisliği uygulamalarına getirdiği kısıtların farkındadır. X
12 Verilerin toplanması, yorumlanması, duyurulması aşamalarında ve mesleki tüm etkinliklerde toplumsal, bilimsel ve etik değerleri gözetir. X

*1 Lowest, 2 Low, 3 Average, 4 High, 5 Highest