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

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

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

6.4. אלגוריתם מפורש לבדיקת מודל CTL

בעיית בדיקת המודל: נתון מבנה plot:$M = \left( {S,{S_0},R,L} \right)$ ונוסחת plot:$f\,\,CTL$.

  • נחשב את קבוצת כל המצבים ב-plot:$M$ שמספקים אתplot:$f$: plot:${S_f} = \left\{ {s \in S|M,S \vDash f} \right\}$
  • נבדוק האם plot:${S_0} \subseteq {S_f}$ - כלומר האם קבוצת המצבים ההתחלתיים מוכלת ב-plot:${S_f}$.
  • פלט האלגוריתם: אם קבוצת המצבים ההתחלתיים מוכלת ב-plot:${S_f}$ אז נחזיר כי plot:$M \vDash f$ ואחרת נחזיר plot:$M\not  \vDash f$. תזכורת: מבנה M מספק נוסחה plot:$f$ (plot:$M \vDash f$) אם כל אחד ממצביו ההתחלתיים מספק את הנוסחה.

אנו קוראים לתהליך "בדיקת מודל" כי אנחנו בודקים האם מבנה M הוא מודל לנוסחה plot:$f$. (plot:$M \vDash f$)

תגיות המסמך:

לפרק הקודם6.3.6. זיהוי ביטויים מהלוגיקות השונות
לפרק הבא6.4.1. הבעיה והאלגוריתם
אין תגובות!
שיתוף:
| עוד