עבור לינוקס, הוצע מנגנון לאימות הפעולה הנכונה של הליבה

להכללה בליבת לינוקס 5.20 (אולי הענף ימונה 6.0), מוצע סט תיקונים עם יישום מנגנון RV (Runtime Verification), המספק כלים לבדיקת הפעולה הנכונה במערכות אמינות במיוחד המבטיחות את היעדר כשלים. האימות מתבצע בזמן ריצה על ידי הצמדת מטפלים לנקודות מעקב שבודקות את התקדמות הביצוע בפועל מול מודל דטרמיניסטי ייחוס קבוע מראש של האוטומט המגדיר את ההתנהגות הצפויה של המערכת.

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

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

מקור: OpenNet.ru