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

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

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

6.5. BDD - Binary Decision Diagram

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

פונקציה בוליאנית: plot:${x_1},...,{x_n},{x_{n + 1}} \in \left\{ {0,1} \right\},f\left( {{x_1},...,{x_n}} \right) = {x_{n + 1}}$

יתרונות BDD לייצוג פונקציות בוליאניות:

  1. לעיתים קרובות מקבלים ייצוג מצומצם בזיכרון.
  2. ביצוע יעיל (בגודל ה-BDD) של פעולות בוליאניות.
  3. ייצוג קנוני – ל-2 פונקציות בוליאניות שקולות יהיה ייצוג BDD זהה, ולכן מאפשר לבדוק שקילות בקלות.

BDD מאפשר לנו לייצר באופן סימבולי את המודל, ולטפל בבעיות "מהעולם האמיתי". מעט היסטוריה: בתחילת שנות ה-80 השיטות לבדיקת מודל שפותחו היו שיטות מפורשות שהתאימו רק לבעיות עם מספר מצומצם של משתנים – "בעיות צעצוע". החל משנות השמונים, במשך שנים רבות, כל כלי בדיקת המודל היו מבוססים על שימוש ב-BDDs.

תגיות המסמך:

לפרק הקודם6.4.4.5. דוגמא
לפרק הבא6.5.1. תיאור קבוצה ע"י פונקציה בוליאנית
אין תגובות!
שיתוף:
| עוד