אימות תוכנה

מתוך ויקיפדיה, האנציקלופדיה החופשית
קפיצה אל: ניווט, חיפוש
הנדסת תוכנה
מאמר זה הוא חלק מקטגוריית הנדסת תוכנה

Coding Shots Annual Plan high res-5.jpg
מתכנת בעבודתו

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

Crystal Clear | Scrum | Unified Process | Extreme Programming | Continuous integration

תחומים תומכים
ניהול פרויקטים | ניהול תצורה | תיעוד | הבטחת איכות | Profiling
כלים
מהדר | מקשר | IDE | ניהול גרסאות | אוטומציית בנייה

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

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

שיטות[עריכת קוד מקור | עריכה]

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

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

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

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

מגבלות[עריכת קוד מקור | עריכה]

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

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

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

ראו גם[עריכת קוד מקור | עריכה]