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

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

6.6.1. מבוא והגדרות

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

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

אנחנו עובדים על מבנה קריפקה $plot:$M\left( {S,R,L} \right)$$ ונוסחה plot:$f$ . המטרה שלנו היא להחזיר את קבוצת המצבים המספקים את f.

את plot:$M$ נקבל באופן הבא (בדומה למה שהצגנו בסעיף על יצוג מכונת קריפקה):

רלציית מעברים שנתונה על ידי BDD מייצג $plot:$R\left( {\bar v,\bar v'} \right)$$ . ( $plot:$\bar v$$ מייצג את המצב הנוכחי, $plot:$\bar v'$$ מייצג את המצב הבא).
: לכל נוסחה אטומית $plot:$a \in AP$$ נקבל את ה-BDD שמייצג את קבוצת המצבים המספקים את ונסמנו ב- $plot:$a\left( {\bar v} \right)$$ .

כמו כן, לפעמים נתונים גם:

קבוצת המצבים כולה $plot:$S\left( {\bar v} \right)$$ . לא חובה במקרה זה כי לעתים $plot:$R\left( {\bar v,\bar v'} \right)$$ מספיק לצרכים.
קבוצת המצבים ההתחלתיים $plot:${S_0}\left( {\bar v} \right)$$ .

באלגוריתם הלא סימבולי "טיפלנו" בכל פעם בתת נוסחה של plot:$f$ עד אשר הגענו לטיפול בנוסחה כולה. האלגוריתם הסימבולי עובד בצורה דומה:

באלגוריתם הלא סימבולי הראנו כי בהנתן תת נוסחה של (הפונקציה הנבדקת) , מתקיים כי $plot:$\forall s \in S,g \in label\left( s \right) \Leftrightarrow s \vDash g$$ .
באלגוריתם הסימבולי "הטיפול" ב- יהיה כך: נבנה BDD שייצג את קבוצת כל המצבים המספקים את (תמיד בעבודה עם BDD האלגוריתמים יעבדו על קבוצות מצבים ולא על מצבים בודדים).

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