Микроядро seL4 математически верифицирано за архитектурата RISC-V
Организацията RISC-V Foundation съобщи за верификация на работата на микроядрото seL4 на системи с архитектура на набор от команди RISC-V. Верификацията е свързана с математическото доказателство за надеждността на работата на seL4, което удостоверява пълното съответствие на зададените формални спецификации. Доказателството за надеждност позволява използването на seL4 в критични системи на базата на процесори RISC-V RV64, които изискват повишено ниво на надеждност и гарантират отсъствието на […]
