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

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

6.7.3. הוכחת נכונות בעזרת SAT – Unbounded Model Checking

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

הכנה: נוסחה לתיאור מסלול ללא מעגלים:

$plot:\[LoopFree\left( {{{\bar v}_0},...,{{\bar v}_k}} \right) = \left( {\mathop \wedge \limits_{i = 0}^{k - 1} R\left( {{{\bar v}_i},{{\bar v}_{i + 1}}} \right)} \right) \wedge \,\,\,\left( {\,\mathop \wedge \limits_{0 \leqslant i < j \leqslant k} \left( {{{\bar v}_i} \ne {{\bar v}_j}} \right)} \right)\]$

נשתמש ב-2 נוסחאות לצורך בדיקת המודל:

$plot:$\varphi _{base}^k\left( {{{\bar v}_0},...,{{\bar v}_k}} \right) = I\left( {{{\bar v}_0}} \right) \wedge \left( {\mathop \wedge \limits_{i = 0}^{k - 1} R\left( {{{\bar v}_i},{{\bar v}_{i + 1}}} \right)} \right) \wedge \,\left( {\mathop \vee \limits_{j = 0}^k \neg p\left( {{{\bar v}_j}} \right)} \right)$$

אם הנוסחה ספיקה נסיק שיש שגיאה – קיים מסלול שבו יש מצב המספק $plot:$\neg p$$ .

אם הנוסחה איננה ספיקה – כל מסלול באורך plot:$k$ ממצב התחלתי מכיל רק מצבים המספקים את plot:$p$

$plot:\[\varphi _{step}^k\left( {{{\bar v}_0},...,{{\bar v}_k},{{\bar v}_{k + 1}}} \right) = \left( {\mathop \wedge \limits_{j = 0}^k R\left( {{{\bar v}_j},{{\bar v}_{j + 1}}} \right) \wedge p\left( {{{\bar v}_j}} \right)} \right) \wedge \neg p\left( {{{\bar v}_{k + 1}}} \right) \wedge \,\,\,\left( {\,\mathop \wedge \limits_{j = 0}^{k - 1} \left( {{{\bar v}_j} \ne {{\bar v}_k}} \right)} \right)\]$

המצב המעניין עבור $plot:\[\varphi _{step}^k\]$ הוא המצב בו $plot:\[\varphi _{step}^k\]$ איננה ספיקה. כאשר $plot:\[\varphi _{step}^k\]$ איננה ספיקה אז לכל מסלול (לא בהכרח ממצב התחלתי) באורך plot:$k + 1$ , אם כל מצביו plot:$1,...,k$ מספקים את plot:$p$ , אז המצב האחרון plot:$k
+ 1$ מספק גם הוא את .

האלגוריתם להוכחת נכונות באמצעות SAT:

נבחר . אם $plot:$\varphi _{base}^k$$ ספיקה נחזיר את ההשמה המספקת כדוגמא נגדית ( $plot:$M\not \vDash AGp$$ ).
אחרת, אם $plot:\[\varphi _{step}^k\]$ לא ספיקה, נעצור ונחזיר true, כלומר $plot:$M \vDash AGp$$ .
אחרת – נגדיל את ונחזור לשלב 1.