מידע כללי
קורס זה מהווה המשך והעמקה של קורס המבוא לאימות תוכנה לכיוון בדיקת- מודלים. חזרה על לוגיקות טמפורליות כשפות מפרט. השוואת כוח הביטוי של שפות טמפורליות. אלגוריתמים לבדיקת מודל של לוגיקת זמן לינארי (LTL). אוטומטים מעל מילים אינסופיות ושימושם עבור בדיקת מודל LTL. שקילויות ויחסי סדר של מערכות ביחס למפרטים. שיטות שונות להתגבר על בעית התפוצצות המצבים, כולל אבסטרקציה ומודולריות.
פקולטה: מדעי המחשב
|תואר ראשון
|תארים מתקדמים
מקצועות קדם
מידע סמסטריאלי
שעות שבועיות
3 נקודות אקדמיות • 2 שעות הרצאה • 1 שעות תרגול
ניווט לדף המקצוע
אחראים
פרופ. גרימברג אורנה
קבוצות רישום
|
|
|
|
שעות שבועיות
3 נקודות אקדמיות • 2 שעות הרצאה • 1 שעות תרגול
ניווט לדף המקצוע
אחראים
פרופ. גרימברג אורנה
קבוצות רישום
|
|
|
|
שעות שבועיות
3 נקודות אקדמיות • 2 שעות הרצאה • 1 שעות תרגול
ניווט לדף המקצוע
אחראים
פרופ. גרימברג אורנה
קבוצות רישום
|
|