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