כניסה

אימות אוטומטי של מערכות

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

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