Gerard Holzmann из Лаборатории реактивного движения (Jet Propulsion Laboratory) NASA, на конференции HotDep 2012, прочёл лекцию о том, как писался код для марсохода Curiosity.
Какие методики, стандарты кодирования и инструменты разработки применялись программистами NASA, для написания кода.
скачать лекцию (mp4 — 228 Mb — продолжительность 1 час).
Тезисы
— написано 3.8 миллиона строк кода на языке C,
— было задействовано 40 программистов,
— код пислся в течении 5 лет (в среднем, получается 10 строк полностью тестируемого кода в час),
— работает это всё на VxWorks,
— Использовался Стандарт кодирования с проверкой по коммиту:
http://lars-lab.jpl.nasa.gov/JPL_Coding_Standard_C.pdf
(язык программирования С, 32 правила).
— Ежедневная сборка со статическим анализом кода (5 разных анализаторов),
— Warning считается ошибкой, штрафы за сломанный билд.
— Code review с использованием Scrub (какая-то внутренняя утилита).
— Юнит тесты.
— Ежедневные интеграционные тесты, штрафы за сломанный интеграционный тест.
— Утилита для логической проверки модели кода (‘logic verification with model checker’) ключевых частей программы. Выполняется математическое доказательство корректности кода на основании модели.
— Доска позора (вывешиваются фотографии нарушителей)
Ссылки
http://www.usenix.org/conference/hotdep12/tbd