אימות פורמלי הוא תחום במדעי המחשב העוסק בבדיקה והוכחת נכונות של מערכות תוכנה וחומרה, כדי לוודא באופן מוחלט שהן נטולת באגים. לפני כמה שבועות נפטר מקורונה אדמונד (אד) קלארק, מהאבות המייסדים של התחום. נספר על אימות פורמלי, איך באגים תרמו לקידומו, ומעט על קלארק ועל פועלו.

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

האם ישנה דרך לבדוק מערכת בצורה אלגוריתמית אוטומטית, כך שבסוף התהליך נדע בוודאות מוחלטת שהיא נטולת באגים? השאלה הזו העסיקה חוקרים במדעי המחשב כבר בשנות ה-70 ואף מוקדם יותר [1]. התשובה תלויה בסוגי המערכות ובסוגי הבאגים. למשל, "בעיית העצירה" (שעליה פירטנו בכתבה קודמת שלנו [2]) לא ניתנת לפתרון ממוחשב, ולכן אם נשאל את השאלה ביחס למערכות מחשב כלליות, ולבאגים כמו "התוכנה אינה עוצרת", התשובה תהיה שאי אפשר לבדוק זאת אוטומטית.
מאידך, אם נגביל את עצמנו למערכות פשוטות מאוד נוכל לבדוק בקלות באגים בצורה אוטומטית. למשל, אם נרצה לבדוק את נכונות פעולתו של שבב שסופר לאחור ממספר נתון קטן מ-100 ועד 0, נוכל לעשות זאת על ידי בדיקת כל האפשרויות [3].
דוגמה נוספת: נתייחס לשבב עם שתי נורות שיכולות להיות במצב "דולק" או "כבוי" כאל מכונה שיש לה ארבעה מצבים (דולק-דולק, דולק-כבוי, כבוי-דולק, כבוי-כבוי). כעת נוכל להגדיר תכונה רצויה, למשל "תמיד לפחות אחת הנורות דולקת", וכדי לבדוק אם היא מתקיימת נבחן את האופן שבו בנוי השבב. במבט ראשון לא ברור לגמרי אם ניתן לעשות זאת באופן אוטומטי.

התחום העוסק בבדיקת נכונות של מערכות נקרא "אימות פורמלי", שכן אנחנו מעוניינים לאמת בצורה פורמלית שהמערכת נטולת באגים. ההבדל המהותי בין אימות פורמלי לבדיקות אנושיות הוא שבסיום תהליך האימות הפורמלי יש בידינו הוכחה מתמטית לכך שהמערכת נטולת באגים (בהנחה שהבאגים הוגדרו נכון).

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

בתחילת שנות ה-80 פיתחו אדמונד קלארק ואלן אמרסון גישה הנקראת "בדיקת מודל" [4], ובה ניתנים לנו תיאור של מערכת ממוחשבת ושל תכונות שהיא צריכה לקיים, ואפשר באופן אוטומטי לגמרי לוודא שהמערכת מקיימת את המפרט. פיתוח הגישה הזו, בין השאר, זיכה את קלארק בפרס טיורינג [5].

בתחילת שנות ה-90 מחשבים כבר היו נפוצים אפילו בשימוש ביתי, ומערכות ידניות רבות הוחלפו במערכות ממוחשבות. באג במערכת מחשב יכול היה לסכן חיים (לדוגמה, באג בבקרת מטוס או במערכת רמזורים). מתבקש היה שאימות פורמלי יהפוך לסטנדרט בפיתוח מערכות מחשב.

וזה כמעט קרה.

האירוע שהציב את האימות הפורמלי במרכז הבמה היה, כמתבקש, באג. ב-1993 הוציאה אינטל לשוק את סדרת מעבדי "פנטיום", שעברו את כל הבדיקות האנושיות הרגילות ונמצאו תקינים. אלא שב-1994 התגלה בהם באג שחמק מבעד לבדיקות. אינטל נאלצה להחזיר את כל המעבדים, מהלך שעלה כחצי מיליארד דולר [6].

עוד שני באגים מפורסמים תרמו לאימוץ התחום: ב-1996 באג בתוכנת ההנחיה של משגר הלוויינים אריאן 5 גרם ללוויין להפעיל את מנגנון ההשמדה העצמי, ולאיבוד כל המטען שעליו, בשווי מאות מיליוני דולרים [7]; וב-1999 באג במערכת הניווט גרם לגשושית מיפוי אקלים להישרף בכניסה לאטמוספירה של מאדים [8].

השימוש באימות פורמלי נשא פרי: כבר ב-1997 נמצא באג קריטי בסדרת מעבדים של אינטל, לפני שלב הייצור. תעשיית ההייטק למדה את הלקח, ואימות פורמלי הפך לחלק מרכזי בתהליך הייצור. לשמחתנו, הבסיס התיאורטי הבשיל במשך כ-20 שנה, והיה מוכן לפיתוחים תעשייתיים. כיום אימות פורמלי הוא לא רק תחום מחקר אקדמי אלא גם שלב מרכזי בייצור מערכות מחשב. בגרסאות הנוכחיות של חלונות למשל מותקנת תוכנת אימות פורמלי הבודקת בזמן אמת שמנהלי התקנים ("דרייברים") לא מבצעים שגיאות [9]. 

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

לצערנו, לפני כמה שבועות נפטר אדמונד קלארק, שהניח את היסודות לתחום האימות הפורמלי והוביל את שימושיו הפרקטיים [10]. בפרט, הוא זיהה לראשונה את האפשרות לבדוק נכונות של מערכות מול תכונות הניתנות לתיאור בצורה נוחה (הנקראת לוגיקה טמפורלית).
ניזכר בדוגמת השבב עם הנורות. הכלים שפיתח קלארק מאפשרים לבדוק אם התכונה "תמיד לפחות אחת הנורות דולקת" מתקיימת במערכת, ואם לא - מדווחים שנמצא באג.

מקורות:

[1] מאמר על בדיקת מערכת בצורה אלגוריתמית אוטומטית - The temporal logic of programs

[2] פוסט של "מדע גדול, בקטנה" על בעיית העצירה

[3] לקריאה על בדיקת מודל בוויקיפדיה

[4] מאמר על בדיקת המודל שפיתחו אדמונד קלארק ואלן אמרסון - Design and synthesis of synchronization skeletons using branching time temporal logic

[5] על זכייתו של קלארק בפרס טיורינג

[6] לקריאה על באג הפנטיום בוויקיפדיה

[7] לקריאה על אסון אריאן 5

[8] לקריאה על גשושית מיפוי האקלים בוויקיפדיה

[9] דוגמה לתוכנת אימות פורמלי לדרייברים ב"חלונות"

[10] הספד לאדמונד קלארק בפיטסבורג פוסט גאזט