Microkernelul seL4 a fost verificat matematic pentru arhitectura RISC-V
Organizația RISC-V Foundation a anunțat verificarea funcționării microkernelului seL4 pe sisteme cu arhitectura setului de comenzi RISC-V. Verificarea constă în o dovadă matematică a fiabilității funcționării seL4, care atestă conformitatea completă cu specificațiile date în limbaj formal. Dovada fiabilității permite utilizarea seL4 în sisteme critice bazate pe procesoare RISC-V RV64, care necesită un nivel ridicat de fiabilitate și garantează absența […]
