W celu włączenia do jądra Linuksa 5.20 (być może gałąź będzie miała numer 6.0) proponowany jest zestaw poprawek z implementacją mechanizmu RV (Runtime Verification), który dostarcza narzędzi do sprawdzania poprawności działania na wysoce niezawodnych systemach, gwarantujących brak awarii. Weryfikacja odbywa się w czasie wykonywania poprzez dołączenie procedur obsługi do punktów śledzenia, które sprawdzają rzeczywisty postęp wykonania w porównaniu z wcześniej określonym referencyjnym deterministycznym modelem automatu, który definiuje oczekiwane zachowanie systemu.
Informacje z punktów śledzenia przesuwają model z jednego stanu do drugiego, a jeśli nowy stan nie odpowiada parametrom modelu, generowane jest ostrzeżenie lub jądro wprowadzane jest w stan „paniki” (oczekuje się, że systemy o wysokiej niezawodności wykryją i reagować na takie sytuacje). Model automatu, który definiuje przejścia z jednego stanu do drugiego, jest eksportowany do formatu „dot” (graphviz), po czym za pomocą narzędzia dot2c jest tłumaczony na reprezentację w języku C, która jest ładowana w postaci modułu jądra, który śledzi odchylenia postępu realizacji od wcześniej zdefiniowanego modelu.
Sprawdzanie modelu w czasie wykonywania jest pozycjonowane jako lżejsza i łatwiejsza do wdrożenia metoda weryfikacji prawidłowego wykonania w systemach o znaczeniu krytycznym, uzupełniająca klasyczne metody weryfikacji niezawodności, takie jak sprawdzanie modeli i matematyczne dowody zgodności kodu ze specyfikacjami podanymi w formalnym dokumencie. język. Do zalet RV należy możliwość zapewnienia ścisłej weryfikacji bez konieczności osobnej implementacji całego systemu w języku modelowania, a także elastyczna reakcja na nieprzewidziane zdarzenia, np. w celu zablokowania dalszej propagacji awarii w systemach krytycznych.
Źródło: opennet.ru