История изменений
Исправление Zubok, (текущая версия) :
Кстати, слышал про L4, даже в закладках есть какой-то проект про L4 на github'е. А что значит, что оно (ядро) формально верифицировано?
Ы? Это L4 формально верифицировано? Вообще, формально верифицированное - это значит, что используя системы машинные доказательства проверяют систему на соответсвие каким-нибудь требованиям (каким - это зависит от того, что именно хотят проверить: корректность, отсутсвие вечных циклов и т. п.
UPD. Вот написал и глянул. Ты про проект L4.verified? http://ertos.nicta.com/research/l4.verified/approach.pml
Исходная версия Zubok, :
Кстати, слышал про L4, даже в закладках есть какой-то проект про L4 на github'е. А что значит, что оно (ядро) формально верифицировано?
Ы? Это L4 формально верифицировано? Вообще, формально верифицированное - это значит, что используя системы машинные доказательства проверяют систему на соответсвие каким-нибудь требованиям (каким - это зависит от того, что именно хотят проверить: корректность, отсутсвие вечных циклов и т. п.