W celu włączenia do jądra Linux 5.20 (możliwe, że gałąź otrzyma numer 6.0) zaproponowano zestaw poprawek implementujących mechanizm RV (Runtime Verification), stanowiący narzędzie do weryfikacji poprawności działania w systemach o wysokiej niezawodności, gwarantujących brak awarii. Weryfikacja odbywa się w czasie rzeczywistym poprzez podpięcie handlerów do punktów śledzenia, porównujących rzeczywisty przebieg wykonania z wcześniej określonym etalonowym deterministycznym modelem automatu, definiującym oczekiwane zachowanie systemu.
Informacje z punktów śledzenia przenoszą model z jednego stanu w inny, a jeśli nowy stan nie odpowiada parametrom modelu, generowane jest ostrzeżenie lub jądro przechodzi w stan „panic” (zakłada się, że systemy o wysokiej niezawodności będą determinować takie sytuacje i reagować na nie). Model automatu, definiujący przejścia między stanami, eksportowany jest do formatu „dot” (graphviz), po czym tłumaczony za pomocą narzędzia dot2c na przedstawienie w języku C, które ładowane jest w formie modułu jądra, monitorującego odchylenia wykonania od zdefiniowanego modelu.
Porównanie z modelem w czasie wykonania jest pozycjonowane jako lżejszy i prostszy w praktycznej realizacji sposób potwierdzania poprawności wykonania w krytycznych systemach, uzupełniający klasyczne metody potwierdzania niezawodności, takie jak weryfikacja modeli oraz matematyczne dowody zgodności kodu ze specyfikacjami określonymi w formalnym języku. Do zalet RV należy możliwość zapewnienia ścisłej weryfikacji bez potrzeby oddzielnej implementacji całego systemu w języku modelującym, a także elastyczne reagowanie na nieprzewidziane zdarzenia, na przykład w celu zablokowania dalszego rozprzestrzeniania się awarii w systemach krytycznych.
Źródło: opennet.ru
