אימות ממוחשב של חומרה ותוכנה

פיתוח הקורס

ד"ר מרק טרכטנברוט

יועצים

פרופ' עמירם יהודאי, פרופ' אורנה קופרמן, פרופ' עופר שטריכמן

נקודות זכות

4 נקודות זכות

רמה

—

שיוך

תואר שני / מדעי המחשב

• 2027סמסטר א – לא מתוכנןסמסטר ב – נפתחקיץ – לא מתוכנן
• 2028סמסטר א – לא מתוכנןסמסטר ב – נפתחקיץ – לא מתוכנן

תנאי קבלה: קבלה לתואר שני במדעי המחשב.

שיוך נוסף: מדעים / מדעי המחשב

שיוך נוסף: הנדסה / הנדסת תוכנה

תנאי קבלה: קבלה לתואר שני במדעי המחשב.

מערכות קריטיות רבות משתמשות ברכיבי תוכנה וחומרה המתאפיינים בהתנהגות מורכבת מאוד, והם אמורים לענות על דרישות אמינות גבוהות במיוחד. הקורס דן בשאלה איך ניתן להבטיח שמערכת כזאת אכן מקיימת את כל תכונות ההתנהגות הנדרשות ממנה. אתגר זה שונה בתכלית מהנושא של בדיקת המערכת (כאשר היא נבדקת על מספר סופי של בדיקות), מאחר ובדיקה כזו אינה מספקת הוכחת הנכונות.

הקורס דן בשיטות המאפשרות להוכיח שמערכת המתוארת על-ידי מודל פורמלי מופשט אכן מקיימת תכונות התנהגות המתוארות גם הן באופן פורמלי, באמצעות לוגיקה טמפורלית. הקורס מתמקד בעיקר בשיטת "בדיקת מודל" (Model Checking).

בין הנושאים הנדונים: לוגיקות LTL ו-CTL להגדרת תכונות התנהגות, אוטומטים שונים למידול מערכות, אלגוריתמי בדיקת מודל וסיבוכיותם. יידונו שיטות שונות להתמודדות עם בעיית "התפוצצות המצבים": בדיקת מודל סימבולית באמצעות תרשימי החלטה בינאריים (Binary Decision Diagrams) ובדיקת מודל מוגבלת (Bounded Model Checking). הקורס כולל גם היכרות עם כלים אוטומטיים לבדיקת מודל.