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

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

6.7.2. בדיקת מודל מבוססת SAT – Bounded Model Checking

המטרה שלנו היא להשתמש ב-SAT Solvers כדי לבצע בדיקת מודל.

בהנתן נוסחה plot:$f$ ומבנה קריפקה M, נרצה לקודד בדיקת מודל $plot:$M \vDash f$$ לנוסחה פסוקית.

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

הגישה שנציג היא הפרכה ולא אימות: נקודד נוסחה פסוקית כך שאם יש השמה המספקת אותה יתקיים כי $plot:$M\not \vDash f$$ . במידה וההשמה אינה מספקת את הנוסחה איננו יודעים את המבנה מספק את הנוסחה, ונצטרך לבדוק נוסחה חדשה. נבצע בדיקת מודל חסומה.

הגדרת הבעיה: בהינתן מודל M, נוסף plot:$f = AGp$ (שקולה ל- $plot:$\neg f = EF\neg p$$ ) וחסם plot:$k$ , צריך לבדוק האם קיים מסלול ב-M באורך קטן או שווה ל- ממצב התחלתי שמוביל למצב המספק $plot:$\neg p$$ . אם מצאנו השמה מספקת אז יתקיים כי $plot:$M\not \vDash f$$ , כלומר $plot:$M\not \vDash AGp$$ . אם לא מצאנו השמה מספקת נגדיל את plot:$k$ .

עצירה: נעצור את התהליך במקרים הבאים: א. התפוצצות זכרון/זמן. ב. נמצא מסלול המוביל למצב המספק $plot:$\neg p$$ . ג. הגעה לחסם plot:$d$ מקסימלי על אורך המסלול, כך שאם אין שגיאה עד חסם זה מובטח שאין שגיאה בכלל ומתקיים $plot:$M \vDash AGp$$ .

בדיקת מודל חסומה עבור M ו- $plot:$\varphi = EF\neg p$$ :

נקבע (אפשרי לקבוע )
נבנה נוסחה פסוקית המתארת את פרישת המודל עד עומק : הנוסחה תתאר את כל הרישות באורך של מסלולים אפשריים ב-M ממצב התחלתי.
נבנה נוסחה פסוקית $plot:$f_\varphi ^k$$ המתארת את כל הרישות באורך המספקות את $plot:$\varphi $$ .
נבדוק האם הנוסחה $plot:$f_M^k \wedge f_\varphi ^k$$ ספיקה. אם כן אז קיים $plot:${s_0} \in S$$ כך ש- $plot:$M,{s_0} \vDash EF\neg p$$ ולכן $plot:$M\not \vDash AGp$$ .

נקודת מפתח להבנת נושא SAT: SAT מקבלת נוסחה ומחזירה האם קיימת לה השמה מספקת. אם במקרה שלנו הנוסחה מייצגת מבנה של מסלול חוקי, SAT מחזירה האם קיים מסלול כזה. אם קיימים מספר מסלולים, SAT תחזיר רק את קיומו של אחד מהם. (לכן SAT נוחה להוכחת E ולא להוכחת A).

מתי אפשר לעצור את האלגוריתם?

פתרון פשטני: $plot:$k = \left| S \right|$$ .
חסם הדוק יותר: $plot:$d = \mathop {\max }\limits_S \left\{ {\mathop {\min }\limits_{{s_0} \in {S_0}} path\left( {{s_0},S} \right)} \right\}$$ . כאשר $plot:$path\left( {{s_0},S} \right)$$ הוא אורך המסלול בין $plot:${s_0}$$ ל-, כלומר אנחנו מחפשים את המסלול הארוך ביותר מבין המסלולים הקצרים ביותר ממצב התחלתי את כל אחד מהמצבים. בפועל חסם זה לא מעשי – מציאתו NP-שלמה.

איך מקבלים את הנתונים? איך בונים את הנוסחה הפסוקית שנשלח אל SAT?

מודל $plot:$M = \left( {S,R,I,L} \right)$$ , כאשר זו קבוצת המצבים, רלציית המעברים $plot:$I \subseteq S$$ קבוצת המצבים ההתחלתיים ו- פונקצית הסימון.
כל מצב מתואר על ידי קידוד בינארי של משתנים בוליאנים $plot:$\bar V = \left( {{v_1},{v_2},...,{v_n}} \right)$$ .
נוסחה פסוקית המתארת את המצבים ההתחלתיים: $plot:$I\left( {\bar v} \right)$$ .
עבור $plot:$p \in AP$$ (בודקים $plot:$EF\neg p$$ ): נוסחה פסוקית לתיאור המצבים המספקים את $plot:$\neg p$$ שנסמנה $plot:$\neg p\left( {\bar v} \right)$$ .
נוסחה פסוקית המתארת את רלציית המעברים $plot:$R\left( {\bar v,\bar v'} \right)$$

בניית הפונקציות:

נסמן $plot:${\bar v_i} = \left( {{v_{i1}},{v_{i2}},...,{v_{in}}} \right)$$ .
נגדיר את בצורה הבאה:

$plot:$f_M^k\left( {{{\bar v}_0},{{\bar v}_1},...,{{\bar v}_k}} \right) = I\left( {{{\bar v}_0}} \right) \wedge R\left( {{{\bar v}_0},{{\bar v}_1}} \right) \wedge R\left( {{{\bar v}_1},{{\bar v}_2}} \right)... \wedge R\left( {{{\bar v}_{k - 1}},{{\bar v}_k}} \right)$$

הנוסחה עבור $plot:$EF\neg p$$ וחסם :

$plot:$f_\varphi ^k\left( {{{\bar v}_0},{{\bar v}_1},...,{{\bar v}_k}} \right) = \neg p\left( {{{\bar v}_0}} \right) \vee \neg p\left( {{{\bar v}_1}} \right) \vee ... \vee \neg p\left( {{{\bar v}_k}} \right)$$

אם ידוע שאנחנו בודקים באופן רציף, אפשר להשתמש בנוסחה $plot:$f_\varphi ^k\left( {{{\bar v}_0},{{\bar v}_1},...,{{\bar v}_k}} \right) = \neg p\left( {{{\bar v}_k}} \right)$$ . הסבר:
$plot:$f_M^0 \wedge f_\varphi ^0$$ פירושו שאין שגיאה במצבים ההתחלתיים.
$plot:$f_M^1 \wedge f_\varphi ^1$$ פירושו שאין שגיאה במצבים במרחק 1.

דוגמא

Shift register עם 3 ביטים plot:$x,y,z$ . כל פעם שמכניסים ביט כל הביטים זזים תא אחד שמאלה. המפרט דורש שתמיד ביט אחד לפחות יהיה שווה ל-0.

$plot:$R\left( {x,y,z,x',y',z'} \right) = \left( {x' = y} \right) \wedge \left( {y' = z} \right) \wedge \left( {z' = 1} \right)$$

$plot:$I\left( {x,y,z} \right) = \left( {x = 0} \right) \vee \left( {y = 0} \right) \vee \left( {z = 0} \right)$$

אנחנו רוצים לבדוק האם $plot:$AG\left[ {\left( {x = 0} \right) \vee \left( {y = 0} \right) \vee \left( {z = 0} \right)} \right]$$ . כדי לבצע זאת נבדוק את השלילה:

$plot:$EF\left[ {\left( {x = 1} \right) \wedge \left( {y = 1} \right) \wedge \left( {z = 1} \right)} \right]$$

ומכאן:

$plot:$\neg p\left( {x,y,z} \right) = \left( {x = 1} \right) \wedge \left( {y = 1} \right) \wedge \left( {z = 1} \right)$$

נרשום את הנוסחאות עבור plot:$k
= 2$ :

$plot:$\begin{gathered} f_M^2 = \left( {{x_0},{y_0},{z_0},{x_1},{y_1},{z_1},{x_2},{y_2},{z_2}} \right) = \hfill \\ & \left( {{x_0} = 0 \vee {y_0} = 0 \vee {z_0} = 0} \right) \wedge \left( {{x_1} = {y_0} \wedge {y_1} = {z_0} \wedge {z_1} = 1} \right) \wedge \left( {{x_2} = {y_1} \wedge {y_2} = {z_1} \wedge {z_2} = 1} \right) \hfill \\ f_\varphi ^2 = \left( {{x_0},{y_0},{z_0},{x_1},{y_1},{z_1},{x_2},{y_2},{z_2}} \right) = \hfill \\ & \left( {{x_0} = 1 \wedge {y_0} = 1 \wedge {z_0} = 1} \right) \vee \left( {{x_1} = 1 \wedge {y_1} = 1 \wedge {z_1} = 1} \right) \vee \left( {{x_2} = 1 \wedge {y_2} = 1 \wedge {z_2} = 1} \right) \hfill \\ \end{gathered} $$

דוגמא להשמה מספקת:

$plot:${x_0}$$	$plot:${y_0}$$	$plot:${z_0}$$	$plot:${x_1}$$	$plot:${y_1}$$	$plot:${z_1}$$	$plot:${x_2}$$	$plot:${y_2}$$	$plot:${z_2}$$
1	0	1	0	1	1	1	1	1
מצב התחלתי $plot:${S_0}$$		מצב 1 - $plot:${S_1}$$	מצב 2 - $plot:${S_2}$$