LİSANSÜSTÜ EĞİTİM ENSTİTÜSÜ
Bilgisayar Mühendisliği (Doktora)
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 Düzeyi |
Doktora
|
|||||
| Dersin Veriliş Şekli | - | |||||
| Dersin Öğretim Yöntem ve Teknikleri | - | |||||
| 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;
|
| Ders 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. |
|
|
Temel Ders | |
| Uzmanlık/Alan Dersleri |
X
|
|
| 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 | - |
| Ders Kitabı | Okutman materyelleri |
| Önerilen Okumalar/Materyaller | 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 Aktiviteleri | Sayı | Katkı Payı % |
| Katılım | ||
| Laboratuvar / Uygulama | ||
| Arazi Çalışması | ||
| Küçük Sınav / Stüdyo Kritiği | ||
| Portfolyo | ||
| Ödev | ||
| Sunum / Jüri Önünde Sunum |
1
|
20
|
| Proje |
1
|
20
|
| Seminer/Çalıştay | ||
| Sözlü Sınav | ||
| Ara Sınav |
1
|
25
|
| Final 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
| Yarıyıl Aktiviteleri | Sayı | Süre (Saat) | İş Yükü |
|---|---|---|---|
| Teorik Ders Saati (Sınav haftası dahildir: 16 x teorik ders saati) |
16
|
3
|
48
|
| Laboratuvar / Uygulama Ders Saati (Sınav haftası dahildir. 16 x uygulama/lab ders saati) |
16
|
0
|
|
| Sınıf Dışı Ders Çalışması |
15
|
4
|
60
|
| Arazi Çalışması |
0
|
||
| Küçük Sınav / Stüdyo Kritiği |
0
|
||
| Portfolyo |
0
|
||
| Ödev |
0
|
||
| Sunum / Jüri Önünde Sunum |
1
|
30
|
30
|
| Proje |
1
|
30
|
30
|
| Seminer/Çalıştay |
0
|
||
| Sözlü Sınav |
0
|
||
| Ara Sınavlar |
1
|
20
|
20
|
| Final Sınavı |
1
|
37
|
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 temel kuramlarını üst düzeyde anlar ve uygular, | X | ||||
| 2 | Bilgisayar Mühendisliği'nde en son gelişmeler dahil olmak üzere genişlemesine ve derinlemesine bilgi sahibidir, | X | ||||
| 3 | Bilgisayar Mühendisliği'nde en yeni bilgilere ulaşır ve bunları kavrayarak araştırma yapabilmek için gerekli yöntem ve becerilerde üst düzeyde yeterliğe sahiptir, | X | ||||
| 4 | Bilime veya teknolojiye yenilik getiren, yeni bir bilimsel yöntem veya teknolojik ürün/süreç geliştiren ya da bilinen bir yöntemi yeni bir alana uygulayan kapsamlı bir çalışma yapar, | X | ||||
| 5 | Özgün bir araştırma sürecini bağımsız olarak algılar, tasarlar, uygulama ve sonuçlandırır; bu süreci yönetir, | X | ||||
| 6 | Akademik çalışmalarının çıktılarını saygın akademik ortamlarda yayınlayarak bilim ve teknoloji literatürüne katkıda bulunur, | X | ||||
| 7 | Bilimsel, teknolojik, sosyal ve kültürel gelişmeleri değerlendirir ve bilimsel tarafsızlık ve etik sorumluluk bilinciyle topluma aktarır, | X | ||||
| 8 | Bilgisayar Mühendisliği'nde fikirlerin ve gelişmelerin eleştirel analizini, sentezini ve değerlendirmesini yapar, | X | ||||
| 9 | Bilgisayar Mühendisliği'nde çalışanlarla ve daha geniş bilimsel ve sosyal topluluklarla yazılı ve sözlü etkin iletişim kurar, İngilizce'yi en az Avrupa Dil Portföyü C1 Genel Düzeyinde kullanarak ileri düzeyde yazılı, sözlü ve görsel iletişim kurar ve tartışır, | X | ||||
| 10 | Bilgisayar Mühendisliğinin kullanıldığı sistem ve konularla ilgili strateji, politika ve planlar geliştirir ve elde edilen sonuçları yorumlar. | X | ||||
*1 Lowest, 2 Low, 3 Average, 4 High, 5 Highest