אימות תוכנה

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

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

שיטות

ישנן שתי שיטות עיקריות לאימות תוכנה.

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

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

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

מגבלות

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

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

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

ראו גם

• מונחים בתוכנה
• הבטחת איכות תוכנה
• בדיקות תוכנה