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