פיתוח פורמלי של יחידות תוכנה היא טכניקה אשר מבטיחה את נכונות היחידה כבר בעת יצירתה. טכניקה זו משמשת בעשור האחרון לפיתוח מערכות קריטיות כמו למשל קו מספר 14 במטרו של פריס שהוא קו ללא נהג הנשלט על ידי תוכנה. בטכניקה זו מתחילים מאפיון פורמלי של המערכת וממירים אותו בשלבים למודלים יותר ויותר קונקרטיים עד השלב האחרון שבו המודל מתורגם לקוד. בכל שלב אנחנו מוכיחים מתמטית שהמודל החדש (הקונקרטי יותר) מתנהג על פי המודל הקודם (המופשט יותר). בצורה זו מקבלים הוכחה מתמטית שהקוד מתנהג בדיוק על פי האפיון. טכניקה זו אפקטיבית במיוחד לשלושה סוגים של מערכות תוכנה:
שגיאה במערכת קריטית עלולה לעלות בחיי אדם או בסכומי עתק. לדוגמא, שגיאה בטיפול ב-overflow במערכת הניהוג של טיל אריאן-5 גרמה להשמדת הטיל ולנזק של כ-500 מיליון יורו. השגיאה בפעולת החילוק של הפנטיום המקורי עלתה לאינטל כ-500 מיליון דולר. בסכומים כאלה משתלם להשקיע יותר מאמץ כדי לודא שהמערכת אינה מכילה כלל שגיאות. לדוגמא, חברת AMD מוכיחה באופן פורמלי את האלגוריתמים הנומריים של המעבדים שלה. מקרה נוסף שבו כדאי להשקיע בפיתוח פורמלי הוא קוד ספרייה. מבני נתונים רבים מכילים קוד עדין אשר קשה לכתוב בטכניקות רגילות ללא שגיאות. למרות שבימינו שפות הפיתוח מגיעות עם ספריות של מבני נתונים עדיין עולה הצורך במקרים רבים לפתח מבני נתונים יעודיים המתאימים לבעיות הספציפיות של החברה. מכיוון שקוד כזה יהיה בשימוש של הרבה מפתחים לאורך זמן, הרי שהנזק מכל שגיאה בו מוכפל כמה וכמה פעמים. לכן כדאי להשקיע יותר מאמץ כדי לודא שהקוד אינו מכיל שגיאות. לבסוף, סוגי מערכות תוכנה מסוימים, בייחוד תוכנה מבוזרת ומקבילית קשה מאוד לבדוק. הסיבה היא ששגיאות רבות תלויות בתזמון של היחידות המקביליות, אבל מכיוון שלא ניתן לשלוט על תזמונים אלה איננו יכולים לכסות את התנהגות המערכת בזמן הבדיקות וגם אם הצלחנו לגלות בעיה הסיכוי שנצליח לשחזר אותה קטן. לדוגמא, באוגוסט 2007 שגיאה בפרוטוקול הביזור של שרתי חברת Skype גרם לכך שכ-220 מיליוני המשתמשים של שירות הטלפון (ובכללם כ-5 מיליון לקוחות משלמים) לא יכלו להשתמש בשירות במשך כיומיים. השגיאה הייתה קיימת במערכת זמן רב אבל באה לידי ביטוי רק כשנוצר מצב מסוים (מהו בדיוק גם אנשי Skype כנראה לא יודעים) שחשף אותה. לכן כדאי להשקיע יותר מאמץ כדי למדל את התנהגות המערכת המבוזרת בצורה מתמטית ולהוכיח שאינה מכילה שגיאות. |
|
|
Constructing Correct Software |