בדיקות בזמן ריצה (Run time verification)

07/11/2019 - 12:00
Speaker: 
Seminar: 
מיקום: 
Abstract: 

הנדסת תכנה כוללת שיטות לפיתוח מערכות המאפשרות חלוקת עבודה, יעילות והקטנת מספר התקלות. כתת-תחום של הנדסת תוכנה, "שיטות פורמליות" עוסקת בטכניקות לבדיקת מערכות וניפוי טעויות. לקראת סוף שנות ה- 60 פותחו שיטות להוכחת נכונות של תכנה, כשהמוטיבציה הראשונית נבעה, בין היתר, מפרויקטי החלל, שדרשו אמינות חסרת תקדים למערכות. נושא זה הלך והתפתח עם השנים, כאשר מערכות מחשב חודרות לתחומים רבים כמו רפואה, תחבורה וכולי. השיטה הישנה של בדיקות תכנה שרדה אף היא, ולמרות שהאמינות שהיא מבטיחה הנה פחותה מזאת של הוכחת נכונות, הרי שהיא עדיין יותר ישימה מבחינת כוח חישוב. בשנים האחרונות עולה הפופולריות של בדיקות בזמן ריצה: האפשרות לעקוב אחרי ביצוע המערכת ולהתריע או אף למנוע תקלות, תוך כדי ריצה. זוהי טכניקה שנמצאת בין בדיקות תכנה, שכן אינה מבטיחה מראש הוכחה מלאה של נכונות התכנה, ובין בדיקות תכנה, שכן היא בודקת את המערכת, בזמן ריצה, מול מפרט מורכב.

 

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