הועלה לאתר:  
מספר עמודים: 120
הורדת המסמך בגרסה להדפסהלהורדת המסמך בשלמותו

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

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

6.2. מבנה קריפקה - Kripke Structure

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

הגדרה פורמלית:

תהי plot:$AP$ קבוצת נוסחאות אטומיות. מבנה קריפקה הוא הרביעיה: plot:$M = \left( {S,R,L,{S_0}} \right)$ כאשר:

  • plot:$S$ - קבוצת מצבים סופית.
  • plot:$R \subseteq S \times S$ רלציית מעברים plot:$R$ טוטאלית (לכלplot:$S$ קיים plot:$S'$ כך ש-plot:$\left( {S,S'} \right) \in R$).
  • plot:$L:S \to {2^{AP}}$ פונקצית סימון המתאימה לכל מצב את הנוסחאות האטומיות שמתקיימות בו.
  • plot:${S_0} \subseteq S$ -  קבוצת מצבים התחלתיים (אופציונאלי)

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



דוגמא

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

תהי התוכנית בעלת המשתנים plot:$x,y$ שתחומן plot:$\left\{ {0,1} \right\}$ וכן משתנה PC שתחומו plot:$\left\{ {{L_1},{L_2}} \right\}$.

התוכנית עצמה היא:

plot:\[\begin{gathered}   {L_1}{\text{:}} & {\text{while}}\,{\text{true}}\,{\text{do}} \hfill \\    &  & \,{L_2}{\text{:}}\,\,\,{\text{x: = \neg x}} \hfill \\    & {\text{od}} \hfill \\ \end{gathered} \]

נתון שהתוכנית מתחילה במצב plot:$y = 0$. מתקיים תמיד כי כל אחד ממצבי התוכנית נותן ערך

ל-plot:$x,y,PC$. נבנה את מכונת המצבים הבאה:

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



נרצה לבדוק תכונות על התוכנית. נגדיר 2 תכונות:

plot:$\begin{gathered}   a: &  & x = y \hfill \\   b: &  & x = 0 \hfill \\ \end{gathered} $

נקרא לתכונות אלו בשם נוסחאות אטומיות.

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

כעת נעבור למכונת קריפקה. ניתן סימון לכל מצב. ערכי המשתנים המקוריים לא מעניינים אותנו.



עבור מכונת הקריפקה שהוצגה, מתקיים:

plot:$\begin{gathered}   S = \left\{ {{S_1},{S_2},...,{S_8}} \right\} \hfill \\   {S_0} = \left\{ {{S_1},{S_3}} \right\} \hfill \\   R = \left\{ {\left( {{S_1},{S_2}} \right),\left( {{S_2},{S_3}} \right),\left( {{S_3},{S_4}} \right),\left( {{S_4},{S_1}} \right),\left( {{S_5},{S_6}} \right),\left( {{S_6},{S_7}} \right),\left( {{S_7},{S_8}} \right),\left( {{S_8},{S_5}} \right)} \right\} \hfill \\   L\left( {{S_2}} \right) = L\left( {{S_1}} \right) = \left\{ {a,b} \right\} \hfill \\   L\left( {{S_3}} \right) = L\left( {{S_4}} \right) = \emptyset  \hfill \\   L\left( {{S_5}} \right) = L\left( {{S_6}} \right) = \left\{ b \right\} \hfill \\   L\left( {{S_7}} \right) = L\left( {{S_8}} \right) = \left\{ a \right\} \hfill \\ \end{gathered} $

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



תגיות המסמך:

לפרק הקודם6.1. מבוא
לפרק הבא6.3. לוגיקות טמפורליות פסוקיות
אין תגובות!
שיתוף:
| עוד