אימות תוכנה

אימות תוכנה הוא תחום שמנסה להוכיח שתוכנה עושה בדיוק מה שמוגדר לה.

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


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

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

אימות משמש גם לאימות מעגלים לוגיים בחומרה, שם בעיית התפוצצת המצבים בדרך כלל פחות קשה.


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

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

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

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

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


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

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

אימות גם עוזר לבדוק מעגלים בחומרה, שהם כמו תוכניות שעובדות על חשמל.


אימות קשה ודורש ידע מיוחד. יש גם בעיה תאורטית: אי אפשר תמיד להחליט אם תוכנית תעצור.

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