Mikro kods seL4 matemātiski pārbaudīts RISC-V arhitektūrai.
RISC-V Foundation paziņoja par mikroberta seL4 darbības pārbaudes apliecināšanu RISC-V arhitektūras sistēmās. Pārbaude sastāv no matemātiskā pierādījuma seL4 uzticamības, kas apliecina pilnīgu atbilstību noteiktajiem specifikācijām formālajā valodā. Uzticamības pierādījums ļauj izmantot seL4 kritiski svarīgās sistēmās, kas balstītas uz RISC-V RV64 procesoriem, kas prasa augstu uzticamības līmeni un garantē trūkumu […]
