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

ספר אלקטרוני מאת: ניר אדר

6.1. מבוא

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

ו-"לא" + דוגמא נגדית אם המערכת אינה מספקת את המפרט.

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

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

	הוכחת נכונות	אימות אוטומטי
מספר המצבים	אינסופי או גדול מאוד	סופי וקטן יחסית (עד $plot:${10^{300}}$$ )
סוג התוכנית	טרנספורמטיבית	ריאקטיבית = תגובתית
מפרט	לוגיקה מסדר ראשון (למשל תחשיב היחסים)	לוגיקה טמפורלית (עיתית)
חישוביות	בלתי כריעה	כריעה
אוטומציה	עזרה מהמשתמש	אוטומציה מלאה
כלים	Theorem proves	RuleBase

השוואה בין הנושאים בהם עסקנו בחלקו הראשון של המסמך לבין הנושאים בהם נעסוק בחלק זה

דוגמאות נוספות למערכות בעלות מספר מצבים סופי:

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

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

מניעה הדדית - mutual exclusion

$plot:$C{S_i}$$ משתנה פסוקי שהוא נכון במצב אם ורק אם תהליך נמצא בקטע הקריטי .

נוכל לכתוב בלוגיקה טמפורלית: $plot:$\neg \left( {C{S_1} \wedge C{S_2}} \right)$$ globally – כלומר לעולם לא יהיו שני תהליכים בקטע הקריטי.
אי הרעבה

כל דרישה תתמלא בסופו של דבר (תוך זמן סופי, eventually).

$plot:\[{\text{globally }}\left( {{\text{request}} \to {\text{eventually granted}}} \right)\]$
פרוטוקולי תקשורת

כל הודעה שנשלחה תגיע תוך זמן סופי: $plot:$globally\left( {sent \to eventually\,\,arrived} \right)$$ .

כל הודעה שמתקבלת גם נשלחה קודם: $plot:$\left( {\neg \,\,got - message} \right)\,\,until\,\,\,sent - message$$