Anatoly Levenchuk (ailev) wrote,
Anatoly Levenchuk
ailev

Безбажники из Австралии

Австралийская команда делает операционные системы без багов -- http://ertos.nicta.com.au/. Пока это все предназначено главным образом для мобильных телефонов.

Вот только парочка их достижений:
-- 8700 строк верифицированного кода микроядра ОС (http://www.ok-labs.com/_assets/image_library/Klein_EHACDEEKNSTW_09.pdf). Очень интересный жизненный цикл получения этого кода (сам код на C, но прототип на Haskell. У меня складывается, что написание сразу двух эквивалентных программ на двух разных языках является сейчас магистральным направлением для хорошо верифицированных и надежных программ -- тот же Harold Lawson употребил этот прием для архитектуры Cy-Clone, коды которой писал на ассемблере, а исполнимые комментарии на чем-то типа Паскаля, а затем добивался одинакового исполнения кодов и комментариев -- "для проверки". Ребята из ERTOS потратили 2 человеко-года на написание Haskell-прототипа, и 2 человеко-месяца на переписывание его на С. И затем грохнули 20 человеко-лет на доказательство правильности кода -- 11 человеко-лет на само доказательство и 9 человеко-лет на инструментарий для этого доказательства. Т.е. стоимость "доказанного кода" идет к стоимости "недоказанного кода" примерно как 10:1).

-- автоматический синтез кода драйвера (при этом код получается верифицированным "по определению"): http://www.ok-labs.com/_assets/video_thumbs/Automatic_device%20driver_synthesis_with_Termite.pdf

Фирма, которая коммерциализирует эти теоретические результаты: http://www.ok-labs.com/

Еще они там хвастаются, что вышеприведенные два супердостижения -- это единственное за 42 года, что Австралия сумела презентовать на конференции ACM по операционным системам. Ага, Австралия. Вот фотография, например, автора статьи про синтез драйвера: http://www.e1os.org/rus/team.html. По русски он говорит не хуже нас с вами.

dz, когда мир (а не только русскоязычные коллеги) услышит про ваш Фантом (http://www.dz.ru/solutions/phantom)?
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

  • 26 comments