Mikrokernel seL4 matematycznie zweryfikowany dla architektury RISC-V
Organizacja RISC-V Foundation ogłosiła weryfikację działania mikrojądra seL4 na systemach z architekturą zestawu instrukcji RISC-V. Weryfikacja polega na matematycznym dowodzie niezawodności działania seL4, który świadczy o pełnej zgodności z wymaganiami określonymi w formalnym języku specyfikacji. Dowód niezawodności umożliwia wykorzystanie seL4 w krytycznych systemach opartych na procesorach RISC-V RV64, które wymagają wyższego poziomu niezawodności i gwarantują brak […]
