Mikrokernel seL4 je matematično overjen za arhitekturo RISC-V
Organizacija RISC-V Foundation je sporočila o overitvi delovanja mikrokernel seL4 v sistemih z arhitekturo nabora ukazov RISC-V. Overitev se osredotoča na matematični dokaz, da se seL4 izkazuje za zanesljivega, kar potrjuje popolno skladnost z zahtevami, postavljenimi v formalno zapisani specifikaciji. Dokaz zanesljivosti omogoča uporabo seL4 v kritičnih sistemih na osnovi procesorjev RISC-V RV64, ki zahtevajo višjo raven zanesljivosti in zagotavljajo odsotnost […]
