פרטי המסמך:

הועלה: סוג מסמך: מסמך אונליין מסמך אונליין
עמודים: 120 הורדות: 8096
הוכחת נכונות של תוכניות ע"י שיטת Floyd ושיטת Hoare. בדיקת מודל: לוגיקות טמפורליות, בדיקת מודל CTL, שימוש ב-BDDs, בדיקת מודל סימבולית ובדיקת מודל חסומה. המסמך עוקב אחר הקורס "מבוא לאימות תוכנה (236342)" בטכניון, אך הוא איננו חומר רשמי שאושר על ידי צוות הקורס, אלא סיכום אישי של ניר אדר. סטודנטים בקורס צריכים לשים לב כי המסמך עלול להכיל טעויות ואי דיוקים.

1. מבוא

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

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

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

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

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

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

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

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

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



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

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

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

תוכניות עם מספר מצבים אינסופי

תוכניות עם מספר מצבים סופי

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

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

מפרט: הינו שפה בסדר ראשון. הרחבה של תחשיב היחסים.

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

התוכנית מיוצגת כטרנספורמצית קלט-פלט. מקבלת plot:$x,y$נתונים ומחזירה לדוגמא plot:$x \cdot y$. אנו מתעניינים בתוצאות ופחות בדרך החישוב.

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

מחשוב: תוכנות כגון Teoram Prover. דורשות התערבות של המשתמש.

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

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



אין תגובות!
שיתוף:
| עוד