קורסים שאינם מקנים נקודות זכות
22904 אימות ממוחשב של חומרה ותוכנה
22904 אימות ממוחשב של חומרה ותוכנה
4 נקודות זכות
שיוך: תואר שני / מדעי המחשב
שיוך נוסף: מדעים / מדעי המחשב
שיוך נוסף: הנדסה / הנדסת תוכנה
תנאי קבלה: קבלה לתואר שני במדעי המחשב.1
פיתוח הקורס: ד"ר מרק טרכטנברוט
יועצים: פרופ' עמירם יהודאי, פרופ' אורנה קופרמן, פרופ' עופר שטריכמן
מערכות קריטיות רבות משתמשות ברכיבי תוכנה וחומרה המתאפיינים בהתנהגות מורכבת מאוד, והם אמורים לענות על דרישות אמינות גבוהות במיוחד. הקורס דן בשאלה איך ניתן להבטיח שמערכת כזאת אכן מקיימת את כל תכונות ההתנהגות הנדרשות ממנה. אתגר זה שונה בתכלית מהנושא של בדיקת המערכת (כאשר היא נבדקת על מספר סופי של בדיקות), מאחר ובדיקה כזו אינה מספקת הוכחת הנכונות.
הקורס דן בשיטות המאפשרות להוכיח שמערכת המתוארת על-ידי מודל פורמלי מופשט אכן מקיימת תכונות התנהגות המתוארות גם הן באופן פורמלי, באמצעות לוגיקה טמפורלית. הקורס מתמקד בעיקר בשיטת "בדיקת מודל" (Model Checking).
בין הנושאים הנדונים: לוגיקות LTL ו-CTL להגדרת תכונות התנהגות, אוטומטים שונים למידול מערכות, אלגוריתמי בדיקת מודל וסיבוכיותם. יידונו שיטות שונות להתמודדות עם בעיית "התפוצצות המצבים": בדיקת מודל סימבולית באמצעות תרשימי החלטה בינאריים (Binary Decision Diagrams) ובדיקת מודל מוגבלת (Bounded Model Checking). הקורס כולל גם היכרות עם כלים אוטומטיים לבדיקת מודל.
חומר הלימוד
-
ספר (באנגלית):
M. Huth & M. Ryan, Logic in Computer Science: Modelling and Reasoning about Systems (Cambridge University Press, 2nd ed. 2018)
-
מדריך למידה בעברית
1 סטודנט שאינו עומד בתנאי הקבלה יכול, במקרים מסוימים, להירשם לקורס. לפרטים נוספים עיינו בסעיף קבלה לקורסים בודדים בתכנית הלימודים לתואר שני במדעי המחשב.