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