Что делает язык Ada предпочтительным для критически важных для безопасности систем МКС?

Эта ссылка на Викиучебник перечисляет его сильные стороны, некоторые из которых:

• Чрезвычайно надежная, статическая и безопасная система типов, которая позволяет программисту создавать мощные абстракции, отражающие реальный мир, и позволяет компилятору обнаруживать многие логические ошибки до того, как они станут ошибками.
• Модульность, при которой компилятор напрямую управляет созданием очень больших программных систем из исходных кодов.
• Сокрытие информации; язык отделяет интерфейсы от реализации и обеспечивает детальный контроль над видимостью.
• Удобочитаемость, которая помогает программистам просматривать и проверять код. Ада отдает предпочтение читателю программы, а не писателю, потому что программа пишется один раз, но читается много раз. Например, синтаксис запрещает все двусмысленные конструкции, чтобы не было сюрпризов, в соответствии с законом наименьшего удивления Дао программирования. (Некоторые программисты на Аде неохотно говорят об исходном коде, который часто бывает загадочным; они предпочитают текст программы, близкий к английской прозе.)
• Переносимость: определение языка позволяет компиляторам различаться только несколькими контролируемыми способами, а в остальном очень точно определяет семантику программ; в результате исходный текст Ады легко переносим между компиляторами и целевыми аппаратными платформами. Чаще всего программу можно перекомпилировать без каких-либо изменений.
• Стандартизация: стандарты были целью и отличительной чертой с момента разработки языка в конце 1970-х годов. Первый стандарт был опубликован в 1980 году, всего через 3 года после начала проектирования. Все компиляторы Ады поддерживают один и тот же язык; единственный диалект, SPARK, представляет собой просто аннотированное подмножество и может быть скомпилировано с помощью компилятора Ada.

Важным моментом является читабельность, поскольку жизнь программного продукта не заканчивается, когда вы заканчиваете его кодирование/тестирование. Самые большие расходы (время и деньги) связаны с обслуживанием этого продукта. Таким образом, для такого длительного проекта, как ISS, использование языка, созданного для помощи в решении этой задачи, за счет сведения к минимуму ошибок и общей двусмысленности кажется уместным.

Этот ответ сравнивает его с C и C++:

Язык Ada имеет ряд встроенных функций безопасности. (Сравните с C, где стандарт состоит из двенадцати страниц, на которых обобщаются неопределенные поведения, встроенные в язык. Сравните с C++, где неопределенные поведения настолько многочисленны, что их даже не перечисляют.) Эти функции безопасности Ады могут иметь существенное значение. стоимость производительности, и из-за этого Ада также предоставляет возможность выборочного отключения этих функций безопасности.

Обратите внимание, что можно достичь того же уровня безопасности с помощью C или C++, если вы используете подмножество языков C или C++ и придерживаетесь руководства по стилю, но в Ada это идет вместе с языком.

РЕДАКТИРОВАТЬ (спасибо JCRM): первая ссылка также говорит о поддержке низкоуровневого программирования:

Ада обладает мощными специализированными функциями, поддерживающими низкоуровневое программирование для систем реального времени, критически важных для безопасности и встроенных систем. Такие функции включают, среди прочего, вставку машинного кода, адресную арифметику, низкоуровневый доступ к памяти, контроль над побитовым представлением данных, битовые манипуляции и четко определенную, статически доказуемую модель параллельных вычислений, называемую профилем Равенскара.

Там, где я работаю, мы на самом деле используем арифметику адресов и функции низкоуровневой памяти для загрузки различных данных конфигурации без необходимости каждый раз компилировать продукт, что экономит много времени.

Сроки. Ада была разработана в 1970-х и 80-х годах с целью заменить множество языков, используемых в системах реального времени Министерства обороны США. НАСА (а также организации из Европы) были активными участниками. В 1991 году Министерство обороны поручило Аде все основные разработки. НАСА сделало то же самое. До того времени Международная космическая станция была бумажной концепцией. Это начало становиться реальным именно тогда, когда мандат Ады вступил в силу.

В 1997 году Минобороны отказалось от своего мандата на Ада. Примерно то же самое сделало и НАСА. Если бы МКС была построена сегодня, ее полетное программное обеспечение, скорее всего, было бы не на Аде.

Так почему же Ада? Ада была создана для решения ряда проблем. Одним из них было большое количество языков, используемых в Министерстве обороны. Другим было предполагаемое отсутствие безопасности в этих языках, особенно в отношении систем реального времени и встроенных систем. Ада предоставила несколько функций, которых не было в других языках.

Есть много причин, по которым Ада стала нишевым языком. Во-первых, излишняя строгость и многословие языка мешают ему быть языком общего назначения. Еще одна проблема заключалась в том, что сообщество Ады упустило момент при переходе от мэйнфреймов к миникомпьютерам и настольным компьютерам. Языки, находящиеся в авангарде этих переходов (C и C++), по-прежнему широко используются. Сообщество Ады также пропустило движение за свободное программное обеспечение. Первый бесплатный компилятор Ады вышел только в 1995 году, и этот выпуск не был завершен. К тому времени было уже слишком поздно.

Я помню, как посещал курсы информатики в конце 90-х. Профессор CS объяснил нашей скудной группе CS-специалистов, что собирается учить нас C, а не COBOL или Ada, потому что в целом это будет полезнее. В то время они были основными языками программирования, которые преподавали в колледжах (каждый крупный университет в этом районе со степенью CS преподавал один из этих двух). Зачем им учить старые языки? Потому что вы все еще можете получить работу по написанию кода в них. Это было примерно в то время, когда строилась МКС.

Причина появления Ada заключалась в том, что им нужно было надежное программное обеспечение для критически важных задач, и Ada была буквально создана, чтобы отвечать всем требованиям. НАСА до сих пор имеет одну из самых дорогостоящих программных ошибок в истории (еще в темные века перфокарт )

Ошибка, внесенная перфокартой, оказалась одной из самых дорогих программных ошибок в истории, когда она привела к разрушению космического корабля «Маринер-1» в 1962 году (стоимость в долларах 1962 года: 18,5 млн; стоимость в сегодняшних долларах: 135 млн долларов). ), прежде чем он смог завершить свою миссию полета к Венере.

Однако в программном обеспечении этой системы наведения имелся фатальный изъян: когда уравнения, которые должны были использоваться для обработки и преобразования данных слежения в полетные инструкции, кодировались на перфокартах, один критический символ упускался: черта или черта, часто в последующие годы перепутали с дефисом. Отсутствие этой перекладины, по сути, привело к тому, что компьютер наведения неправильно компенсировал какое-то нормальное движение космического корабля.

Основная черта Ады - стабильность

Акцентируя внимание на надежных принципах разработки программного обеспечения, Ada поддерживает разработку приложений с высокой степенью интеграции, в том числе тех, которые должны быть сертифицированы в соответствии со стандартами безопасности, такими как DO-178B, и стандартами безопасности, такими как Common Criteria. Например, строгая типизация означает, что данные, предназначенные для одной цели, не будут доступны через неподходящие операции; предотвращаются такие ошибки, как обработка указателей как целых чисел (или наоборот). А проверка границ массива в Ada предотвращает уязвимости переполнения буфера, распространенные в C и C++.

НАСА пыталось создать свой собственный язык в стиле Ада под названием (я не придумываю) HAL/S , который использовался космическим челноком и... не более того. К тому времени все наземное оборудование будет использовать Аду ( стандарты! )

Было предложено стандартную наземную версию HAL НАСА, названную HAL/G для «земли», но грядущее появление языка программирования, который вскоре будет называться Ада, способствовало отсутствию интереса Intermetrics к продолжению этой работы.

О, у HAL/S есть еще одна небольшая проблема

Слабость Hal/S заключается в том, что он легко доступен только при размещении на мейнфреймах серии IBM 360/370. Intermetrics также разместила Hal/S на миникомпьютерах Modcomp IV и Classic, а также на миникомпьютерах Data General Eclipse. Но реализация Modcomp используется только JPL, а разработка Eclipse больше не используется, поскольку ограничения адресного пространства снижают скорость компиляции примерно до 30 строк в минуту.

Таким образом, неудивительно, что в начале 90-х (когда ПК были на подъеме) было намного дешевле производить больше стандартных вычислительных устройств (держу пари, что IBM смогла заставить Ada работать на более стандартном оборудовании, поскольку они уже поставляли астронавтов с Thinkpads в то время ). Забавный факт: Thinkpads под управлением Linux используются для взаимодействия со станционным компьютером.

«Это были просто прикладные потребности», — сказал он, описывая, как программное обеспечение ноутбука, которое взаимодействовало с системами управления станцией в те первые дни, было разработано для работы в ОС на базе Linux.

Напротив, марсоход Curiosity (начало 2000-х) работал на C

Он выполняет 2,5 миллиона строк C на процессоре RAD750 производства BAE.

С веб-сайта :

Инструменты AdaCore можно использовать для достижения целей проверки, включая соответствие стандарту кодирования , точность кода ( предотвращение ошибок, таких как переполнение буфера, целочисленное переполнение и ссылки на неинициализированные переменные), а также структурный анализ покрытия вплоть до MC/DC . Специализированные высоконадежные библиотеки времени выполнения, в том числе та, которая реализует профиль задач Ravenscar, достаточно просты, чтобы их можно было включать в квалифицированные системы, но достаточно выразительны, чтобы поддерживать необходимую функциональность для жесткого космического программного обеспечения в реальном времени . Квалификационные материалы для библиотек времени выполнения могут быть разработаны для стандарта ECSS и адаптированы к новым контекстам проекта.

C и C++ не предотвращают эти ошибки (за исключением дорогостоящих надстроек ), а Java не требует жесткого режима реального времени (за исключением нестандартных виртуальных машин ).

Когда на кону стоит жизнь, лучше исключить ошибки времени выполнения и задержки по замыслу :

with Ada.Text_IO; use Ada.Text_IO;

procedure Learn is

   subtype Alphabet is Character range 'A' .. 'Z';

begin

   Put_Line ("Learning Ada from " & Alphabet'First & " to " & Alphabet'Last);

end Learn;

Здесь Alphabet не может содержать никакого значения, кроме A до Z. Эта довольно уникальная языковая особенность, среди прочих , помогла команде студентов выполнить миссию CubeSat 2013-2015 :

В качестве одного из примеров языка Ada в студенческой среде студенты Вермонтского технического колледжа в США использовали язык SPARK (формально поддающееся анализу подмножество языка Ada) для разработки программного обеспечения для спутника CubeSat, недавно завершившего успешную двухлетнюю орбитальную миссию. SPARK был выбран из-за преимуществ надежности. У студентов не было предыдущего опыта работы с Ada, SPARK или формальными методами, но они смогли быстро освоиться.

Из двенадцати CubeSat от академических учреждений, которые были включены в запуск, один из Vermont Tech был единственным, который завершил свою миссию. Многие другие погибли из-за программных ошибок. Группа Vermont Tech приписывает свой успех подходу SPARK, который, например, позволил им формально продемонстрировать отсутствие ошибок во время выполнения.

Из всех возможных языков, какие аспекты Ады делают выбор НАСА для такого важного приложения? Каков может быть вес между унаследованными причинами и внутренней пригодностью?

• Ада — это язык, разработанный именно для таких ситуаций , т. е. отказоустойчивых, работающих в реальном времени и (часто) встроенных систем, используемых для управления важным оборудованием или процессами.

• Эволюция Ады с самого начала была гораздо более целенаправленной и жестко управляемой. И его создатели, и его оценщики были отобранными экспертами в области языкового развития с сильным чувством долга как перед своей профессией, так и перед проектом Ада. Подобно тому, как ценности Западного побережья пронизывают Яву, бескорыстная скромность Ичбиа, Дьюара и Тафта задает тон для Ады, который до сих пор преобладает и который должен понравиться такой организации, как НАСА.

• В Ada есть формально определенный язык подмножеств под названием SPARK, который позволяет легко отображать формально проверенный дизайн системы в его код.

• Ада — один из самых быстрых языков , к тому же с параллельными процессорами.

• Индустрия Ada (такие компании, как AdaCore, Altran, Green Hills, Wind River и т. д.) разработала множество инструментов поддержки для разработки критически важных систем в Ada/SPARK.

• Есть несколько подходящих альтернативных языков для Ады

• Альтернативные языки, такие как формально определенный C, не имеют такой же глубины опыта или поддержки, как Ada/SPARK.

Я понятия не имею, каковы были подробные системные требования и насколько жесткими были правила проведения тендеров в отношении взвешивания наследия и внутренней пригодности. Но мне кажется рациональным, что Ada/SPARK получит высокие оценки в обеих категориях. Унаследованные факторы должны включать такие вещи, как

• НАСА было первоначальным спонсором проекта Ада и с самого начала использовало его в предыдущих системах.

• Компания, занимающаяся сборкой систем, скорее всего, лучше знакома с Ada/SPARK, ноу-хау в эффективном развертывании своих конструкций для требований новой критической системы.

• Вероятное существующее использование Ada/SPARK субподрядчиками, например, встроенные системы для вспомогательного оборудования, такого как радар, рентгеновские прицелы и т. д., для проекта и обмена данными между основной и подсистемами.

Ада — это SGMLязыков программирования (а Java/C# — это XML). Оба построены на новой базе для комплексного решения. И оба не стали популярными из-за своей сложности и странности. (Меньшинство знает SGML, но все понимают HTML: простота — это сила.) Мы изучили Аду в 91-м, и она нам понравилась, даже если мы пришли из Модулы-3, а не из дрянного Паскаля или С. (Не говоря уже о ассемблере.) Ада выглядела идеально встроенной. в целом и в деталях. Но никто из нас им не пользовался, потому что единственная среда Ады была для IBM 360 (или ее российского клона), а компилятора Ады для ПК не появлялось уже много лет. И он стал «сияющим бриллиантом в стеклянном шкафу», теоретически совершенным, но неприкосновенным. Мы написали код для Sieve of Eratosthenes, но не было ресурсов для его запуска с задачами log(log(10e9)) . (В тот день они считали оперативную память сотнями КБ. ) Тем временем появились хорошие среды C++ (с пригодными для использования библиотеками классов!), и большинство программистов использовали его в качестве основной платформы, пока десять лет спустя не появилась Java. И даже не было хороших инструментов разработки для Java, но были пригодные для использования, и их можно было запускать на дешевых ПК.