מבוא לאימות תוכנה

1. מבוא

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

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

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

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

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

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

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

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

מסמך זה מתרכז בבדיקות סטאטיות של תוכניות.

הנושאים העיקריים בהם מסמך זה עוסק:

1. הוכחת נכונות של תוכניות ע"י לוגיקה – תוכניות בעלות מספר מצבים אינסופי.
2. בדיקת מודלים במערכות בעלות מספר סופי של מצבים.

הבלדים בין תוכניות עם מס' מצבים סופי לתוכניות עם מס' מצבים אינסופי:

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