Компания AdaCore (Франция) – производитель средств разработки и верификации ПО на языках Ada (стандарт ISO/IEC 8652) и SPARK (подмножество Ada, позволяющее проводить формальную верификацию ПО)

Журнал «Открытые Системы» №10-2003 :
"В СССР в начале 80-х годов была образована Рабочая группа по языку программирования Ада при Государственном комитете по науке и технике. Тщательно собиралась и анализировалась вся открытая информация о проекте, а усилиями специальных служб добывалась и закрытая информация. Были организованы проекты по реализации Ады для практически всех использовавшихся тогда архитектур ЭВМ, и некоторые из них оказались весьма успешными. Распад СССР положил конец этой деятельности. Сегодня Ада используется в России и СНГ отдельными энтузиастами. Если спросить отечественного ИТ-специалиста: «Что такое Ада?», большинство лишь удивленно пожмет плечами, а кто-то даже скажет, что это мертвый язык, когда-то придуманный Пентагоном, а ныне практически не используемый. На самом же деле Ада и сегодня — вполне благополучный и активно применяемый в различных областях язык программирования."
Цель данной страницы - подтвердить актуальность этого утвержения и в настоящее время.


DENSO применяет формальную верификацию автомобильного ПО для обеспечения требований ISO 26262
Компания AdaCore завершила исследовательский проект, проведенный по заказу корпорации DENSO – крупнейшего японского производителя автомобильных комплектующих. Целью проекта было продемонстрировать применение формальных методов для выполнения требований стандарта функциональной безопасности автомобильного ПО ISO 26262 в части обеспечения «Freedom from Interference» (Свободы от Вторжений) – защиты приложений с высоким уровнем критичности для безопасности ASIL (Automotive Safety Integrity Level) от влияния сбоев, возникших в приложениях с низким уровнем критичности ASIL, унаследованных (legacy) из предыдущих проектов и написанных на языке Си.

В качестве языка программирования для разработки защищенных высококритичных приложений был применен язык SPARK, позволяющий проводить формальную верификацию – доказательство корректности работы ПО с помощью математических методов. Язык SPARK является подмножеством языка Ada - международного стандарта ISO 8652. В последней редакции стандарта ISO 8652-2012 (Ada 2012) введена конструкция для задания «контрактов» - требований к результатам работы программного модуля, описанных непосредственно в тексте программы на языке Ada. «Контракт» предназначен для использования компилятором для выполнения динамических проверок или средствами статического анализа для формальной верификации.

В этом проекте компания AdaCore выступила не только поставщиком средств формальной верификации ПО на языке SPARK, но и разработчиком методологии создания «контрактов» для обеспечения требований Freedom from Interference в ISO 26262, а также технологии «гибридной верификации» - совмещения формальных методов с традиционной верификацией ПО, основанной на тестировании.


AdaCore GNAT Pro for QNX: комплекc средств разработки и верификации ПО на языке Ada для операционной системы QNX
Компания AdaCore анонсировала поддержку инструментального комплекса GNAT Pro для встраиваемой операционной системы реального времени QNX – одной из самых распространенных в мире и в России ОСРВ для ответственных встраиваемых применений.

Язык программирования Ada создавался специально для разработки ПО с повышенными требованиями к надежности, и в настоящее время Ada является основным языком для разработки ПО систем, критически важных для безопасности и сертифицируемых по стандартам функциональной (safety) и информационной (security) безопасности. Язык Ada является международным стандартом ISO 8652. В последней редакции стандарта ISO 8652-2012 (Ada 2012) введена конструкция для задания «контрактов» - требований к результатам работы программного модуля, описанных непосредственно в тексте программы на языке Ada. «Контракт» предназначен для использования компилятором для выполнения динамических проверок или средствами статического анализа для формальной верификации – доказательства математическими методами, что ПО делает то, что от него требуется и не делает того, что не требуется.

Комплекс инструментальных средств GNAT Pro включает в себя компилятор, поддерживающий все версии стандартов Ada (Ada 83, Ada 95, Ada 2005 и Ada 2012), интегрированную среду разработки, визуальный отладчик, средства автоматизации тестирования, средства статического анализа (контроль стандартов кодирования, сбор метрик программного кода, анализатор стека), средства формальной верификации (доказательства корректности работы ПО с помощью математических методов) и средства интеграции Ada и C/C++ программ.

В первой версии GNAT Pro for QNX будет поддерживать микропроцессоры с архитектурой ARM семейства Cortex A, в дальнейшем будут поддерживаться и другие микропроцессорные архитектуры. Инструментальный комплекс GNAT Pro выпускается также для операционных систем LynxOS, PikeOS, VxWorks, Embedded Linux и для систем без ОС (bare metal) и поддерживает микропроцессоры с архитектурами PowerPC, x86, ARM и LEON. Инструментальные средства компании AdaCore сопровождаются квалификационными материалами в соответствии со стандартами DO-178C (авионика), EN 50128 (ж/д системы), ISO 26262 (автоэлектроника) и ECSS-E-ST-40C/ECSS-Q-ST-80C (космическая техника).

Другие продукты AdaCore:
CodePeer - статический анализатор / детектор потенциальных ошибок и уязвимостей в программах на языке Ada,
SPARK Pro – комплекс средств верификации ПО на языке SPARK – формально верифицируемом подмножестве языка Ada,
QGen – квалифицируемый генератор программного кода на языках MISRA C и SPARK из моделей Simulink/Stateflow.


ПО на языке Ada управляет искусственным сердцем
Большинство больных с сердечной недостаточной четвертой степени, нуждающиеся в трансплантации сердца, не доживают до операции из-за длительного срока ожидания донорского органа. Искусственное сердце позволяет таким больным дождаться операции.

Шведская компания Scandinavian Real Heart AB ведет разработку искусственного сердца нового поколения TAH (Total Artificial Heart), которое полностью повторяет алгоритм работы сердца и позволит больным вести нормальный образ жизни за пределами клиники.

К контроллеру, управляющему насосами TAH, и к его программному обеспечению предъявляются высочайшие требования по надежности, и в качестве языка программирования этого контроллера был выбран язык Ada и инструментальные средства компании AdaCore.

Язык программирования Ada предназначен для разработки программного обеспечения высоконадежных, критических для безопасности встраиваемых компьютерных систем, подлежащих сертификации по стандартам безопасности, таким как DO-178 (авионика), EN 50128 (железнодорожные системы), ISO 26262 (автоэлектроника) и IEC 62304 (медицинская техника). В Российской Федерации действует ГОСТ Р МЭК 62304-2013 «Изделия медицинские. Программное обеспечение. Процессы жизненного цикла», идентичный международному стандарту IEC 62304. Язык Ada является международным стандартом ISO 8652.

Для разработки ПО управления искусственным сердцем TAH применены следующие инструментальные средства компании AdaCore:
GNAT Pro Ada for ARM – компилятор и комплекс средств разработки на языке Ada для микропроцессоров с архитектурой ARM;
SPARK Pro – комплекс средств верификации ПО на языке SPARK (формально-верифицируемое подмножество языка Ada)
GNATstack – средство статического анализа ПО на отсутствие ситуаций переполнения стека.


GNAT Pro Developer ARM: язык Ada становится доступнее для разработчиков ПО встраиваемых систем
В индустрии встраиваемых компьютерных систем наблюдаются две важные новые тенденции: (1) разработчики «железа» все чаще применяют микропроцессоры с архитектурой ARM и (2) разработчики ПО все чаще рассматривают в качестве альтернативы языку программирования C/С++ применение языка Ada с гораздо более широкими возможностями обнаружения ошибок в ПО.

Компания AdaCore отвечает на эти требования рынка и выпускает специальный вариант комплекса GNAT Pro средств разработки на языке Ada. Комплекс GNAT Pro Developer поддерживает два варианта целевых платформ с архитектурой ARM: с операционной системой Embedded Linux и без ОС (bare metal).

Комплекс GNAT Pro Developer поддерживает разработку ПО c использованием последней версии языка Ada 2012 - международного стандарта ISO 8652:2012. Стоимость GNAT Pro Developer значительно ниже стоимости других вариантов GNAT Pro в расчете на одного пользователя и включает в себя начальную конфигурацию средств формальной верификации – доказательства корректности работы ПО с помощью математических методов статического анализа.

Другие варианты GNAT Pro:
GNAT Pro Enterprise – для разработки ПО процессоров с архитектурами x86, PowerPC, ARM и LEON. Поддерживаются целевые платформы с операционными системами LynxOS, PikeOS, QNX, VxWorks и без ОС (bare metal).
GNAT Pro Assurance – для разработки ПО систем, сертифицируемых по стандартам безопасности DO-178B/C (авиационные системы), EN 50128 (ж/д системы) и ECSS-E-ST-40C/ECSS-Q-80C (космические системы). Поддерживаются целевые платформы с процессорами архитектур x86, PowerPC, ARM и LEON, с операционными системами LynxOS, PikeOS, QNX, VxWorks и без ОС (bare metal).

На странице www.adacore.com/resources можно посмотреть вебинар «Developing Embedded Systems in Ada - A C Programmers guide to safe, secure software».


Опубликовано руководство по применению SPARK
Компания AdaCore в соавторстве с Thales выпустила руководство "Implementation Guidance for the Adoption of SPARK" по применению языка SPARK - подмножества языка Ada, позволяющего проводить формальную верификацию.
Руководство посвящено эволюционному внедрению методов формальной верификации в текущие проекты и рассматривает на примере Thales Group пять уровней глубины интеграции этих методов в уже существующие на предприятиях процессы разработки программного обеспечения с высоким уровнем уверенности в надежности (high-assurance software).
Руководство можно загрузить на странице http://www.adacore.com/knowledge/technical-papers/implementation-guidance-spark/


Статья "Программное обеспечение без ошибок? Язык Ada 2012" опубликована в журналах
"Автоматика, Связь, Информатика" №4-2017
и
"Авиакосмическое Приборостроение" №5-2017


Опубликовано руководство "AdaCore Technologies for DO-178C/ED-12C"
В руководстве рассматриваются четыре сценария применения инструментальных средств AdaCore при разработке и верификации ПО по авиационным требованиям DO-178С/ED-12С:

1. Разработка на языке Ada 2012 без применения объектно-ориентированных технологий (OOT) согласно основному стандарту DO-178C/ED-12С

2. Разработка на языке Ada 2012 с применением объектно-ориентированных технологий (OOT) согласно дополнительному стандарту DO-332/ED-217 "Object-Oriented Technologies and Related Technologies"

3. Модельно-ориентированная разработка с применением квалифицированного кодогенератора QGen согласно дополнительному стандарту DO-331/ED-218 "Model-Based Development and Verification".

4. Использование языка SPARK и формальной верификации согласно дополнительному стандарту DO-333/ED-216 "Formal Methods".

Авторы Frederic Pothon и Quentin Ochem. Объем руководства - 150стр.
Загрузить руководство можно на странице www.adacore.com/tech-do-178c


Программное обеспечение миссии ЭкзоМарс разработано на языке Ada
ЭкзоМарс (ExoMars) – совместный проект европейского космического агентства ESA и российского агентства Роскосмос по исследованию Марса, запуск первой миссии которого состоялся в марте 2016г. В первой миссии два космических аппарата: орбитальный аппарат TGO (Trace Gas Orbiter) для исследования малых составляющих атмосферы и посадочный модуль EDM (Entry, Descent and Landing Demonstrator Module) для демонстрации возможности входа, спуска и посадки.

Разработчик TGO и EDM - компания Thales Alenia Space использовала для разработки программного обеспечения обоих аппаратов язык программирования Ada и средства разработки компании AdaCore. Программное обеспечение TGO работает на микропроцессоре ERC32, а ПО EDM – на микропроцессоре LEON2. Для разработки и верификации ПО применялись компилятор AdaCore GNAT Pro, среда разработки GNAT Programming Studio и анализатор использования стека GNATstack. Разработка ПО была выполнена в соответствии с требованиями стандартов ECCS (European Cooperation on Space Standardization) для уровня критичности для безопасности Level B.

Немного истории.
Язык программирования Ada был разработан в начале 80-х годов. Целью разработки было создание языка для встраиваемых систем реального времени с повышенными требованиями к надежности ПО. В 1983 году язык становится стандартом ANSI/MIL-STD-1815A, а в 1987 году - международным стандартом ISO 8652. Эта первая версия языка, называемая Ada 83, стала стандартом ГОСТ 27831-88 во времена бурного внедрения языка Ada в СССР при поддержке ГКНТ (Государственного Комитета по Науке и Технике Совета Министров СССР).

Потом язык развивался и совершенствовался (Ada 95, Ada 2005) и сегодняшняя версия Ada 2012 является действующим международным стандартом ISO 8652:2012. Во всем мире Ada является основным языком разработки ПО оборонных, авиационных и космических систем. К сожалению, в современной России язык программирования Ada практически не применяется. Наверное, отсутствует нужда в высоконадежном программном обеспечении.


Очередная, уже 21-я по счету конференция "RELIABLE SOFTWARE TECHNOLOGIES" ассоциации Ada-Europe
прошла с 13 по 17 июня в г. Пиза (Италия).
Программа конференции на www.ada-europe.org.
Спонсоры конференции Ada-Europe 2016: AdaCore, ANSYS Esterel, Ellidiss Software, PTC, Rapita Systems и Vector Software


10 декабря 2015г. исполнилось 200 лет со дня рождения Ada Lovelace,
в честь которой был назван язык Ada.
Августа Ада Лавлейс, дочь английского поэта Лорда Байрона, была математиком и считается первым в истории программистом, написавшим программу для Аналитической Машины Чарльза Беббиджа.
Компания AdaCore отметила это событие созданием сайта www.celebratingada.com с описанием жизни и карьеры Ады, а также c описанием основных этапов жизни языка Ada.

SPARK Pro 16 – новая версия среды разработки и формальной верификации ПО на языке SPARK
Язык SPARK – это подмножество языка Ada, которое позволяет проводить формальную верификацию с помощью математических методов доказательства отсутствия дефектов в ПО. Применение формальных методов при сертификации ПО определяется требованиями стандартов безопасности ПО, например приложением DO-333 Formal Methods Supplements к стандартам DO-178С (авиационное бортовое ПО) и DO-278A (авиационное наземное ПО). Формальная верификация является также обязательным требованием при сертификации по стандарту информационной безопасности ISO/IEC 15408 «Общие Критерии» на наиболее строгие Оценочные Уровни Доверия EAL6 и EAL7.
Cреда разработки и формальной верификации SPARK Pro - совместная разработка компаний Altran и AdaCore, выпущена как коммерческий продукт в 2014 году и поддерживает последнюю версию языка SPARK 2014 (www.spark-2014.org), который основан на последней редакции стандарта Ada ISO/IEC 8652:2012, известной как Ada 2012 (www.ada2012.org). Для доказательства корректности ПО используются «контракты» языка Ada 2012 - описания формальных требований, встроенные в текст программы на языке Ada.
Новая версия SPARK Pro 16 поддерживает профиль многозадачности Ravenscar языка Ada и расширяет область применения формальных методов доказательства корректности на область параллельного (concurrent) программирования.
Язык SPARK и среда SPARK Pro могут быть использованы не только для новых проектов «с нуля», но и «инкрементно» вводиться в существующие проекты с применением «гибридной» верификации – сочетания формальных методов с традиционным технологиями тестирования.

Свободно-распространяемая версия Ada-компилятора GNAT GPL for ARM,
доступная для загрузки с сайта libre.adacore.com, поддерживает одноплатный компьютер Raspberry Pi 2 (www.raspberrypi.ru) на базе четырехядерного микропроцессора ARM Cortex-A7, работающий под управлением Embedded Linux.
GNAT GPL – это полный комплект средств, поддерживающих разработку на языке Ada последней редакции Ada-2012, включая среду разработки GPS (GNAT Programming Studio).
Также на сайте libre.adacore.com доступна версия GNAT GPL для LEGO MINDSTORMS – набора для обучения программированию робототехнических систем.

На university.adacore.com новый курс – программирование на языке SPARK 2014
В курсе 5 уроков:
1. SPARK 2014 Overview
2. SPARK 2014 Flow Analysis
3. SPARK 2014 Proof of Program Integrity
4. SPARK 2014 State Abstraction
5. SPARK 2014 Proof of Functional Correctness

QGen: квалифицируемый кодогенератор для Simulink и Stateflow
Средства модельно-ориентированного проектирования (МОП) находят все более широкое применение, но далеко не всегда они могут быть использованы при разработке ПО сертифицируемых систем.
Новый продукт QGen фирмы AdaCore позволяет применять средства МОП Simulink/Stateflow фирмы Mathworks c генерацией программного кода, сертифицируемого по стандартам DO-178B/C, EN 50128 и ISO 26262.
Кодогенератор QGen поддерживает подмножество из примерно 100 блоков Simulink, отобранных по критерию сертифицируемости, и производит код MISRA C (подмножество языка C) и SPARK (подмножество языка Ada).
Кроме генерации кода QGen производит также верификацию на уровне моделей. Кодогенератор квалифицируем по DO-178C на уровень TQL1 (Tool Qualification Level), верификатор моделей - по DO-178C на уровень TQL5.
Для проведения PIL-тестирования (Processor-In-Loop) сгенерированный QGen код может быть откомпилирован компилятором AdaCore GNAT Pro и исполнен на эмуляторе целевой архитектуры AdaCore GNATemulator c последующим анализом тестового покрытия с помощью анализатора AdaCore GNATcoverage.

ПО испанского микроспутника UPMSat-2 разрабатывается на языке Ada
Микроспутник UPMSat-2 весом 50кг разрабатывается в Политехническом Университете Мадрида (Universidad Politecnica de Madrid – UPM) и планируется в конце 2015г. к запуску на гелиосинхронную орбиту на расстоянии ~600 км над Землей.
Бортовой компьютер построен на базе FPGA с процессорным ядром LEON3 и операционной системой Open Ravenscar Kernel, разработанными в UPM. Прикладное ПО спутника разрабатывается на языке Ada с применением средств разработки компании AdaCore и составит ~20000 строк Ada-кода. Также средства верификации и валидации компании AdaCore будут использованы для сертификации ПО по стандарту ECSS-E-ST-40C (European Cooperation for Space Standardization).

Новые курсы на university.adacore.com – онлайн-ресурсе для самостоятельного обучения программированию на языке Ada
Курс Ada003 “Programming in the large” - разработка больших проектов.
В курсе пять уроков: Exception Handling, Type Safety, Access Types, Encapsulation и Genericity.
Курс Ada 004 “Multi-Language Programming with Ada” – многоязыковые проекты.
В курсе четыре урока: Mixed Language Introduction, Ada and C, Ada and C++, Ada and Java.

GNAT Pro Safety Critical для микропроцессоров ARM Cortex
Микропроцессоры с архитектурой ARM становятся все более распространенными во встраиваемых системах, критических для безопасности и подлежащих сертификации (авиация/космос, транспорт, медицина и др). Комплекс средств разработки на языке Ada GNAT Pro Safety Critical компании AdaCore теперь поддерживает микропроцессоры ARM Corteх в дополнение к уже поддерживаемым PowerPC и LEON. Применение какой-либо встраиваемой операционной системы на ARM Cortex не требуется, что позволяет использовать язык Ada для разработки ПО систем с ограниченными ресурсами (bare board). GNAT Pro Safety Critical предназначен для разработки ПО систем, подлежащих сертификации по стандартам DO-178B/DO-178C (авиация), DO-278/DO-278A (системы УВД), EN 50128 (ж/д транспорт) и ECSS-E-ST-40C/ ECSS-Q-ST-80C (космос).

university.adacore.com – онлайн ресурс для самостоятельного обучения программированию на языке Ada
открыт компанией AdaCore. Ресурс будет содержать курсы обучения различного уровня с доступом к инструментальному комплексу GNAT Ada для написания и отладки программ. На день открытия ресурс содержит два курса: Ada 001 “Overview” и Ada 002 “Basic Concepts”. Эти начальные и последующие углубленные курсы применяют последнюю редакцию стандарта языка Ada 2012. Также на этом ресурсе появятся курсы по языку SPARK (подмножеству языка Ада, которое позволяет применять алгоритмы углубленного статического анализа исходного текста, вплоть до формального доказательства корректности поведения программы) и его новой редакции SPARK 2014.

Стандарт Ada 2012 утвержден и опубликован
Объединенный Технический Комитет ISO/IEC по информационным технологиям утвердил новую редакцию стандарта языка программирования Ada ISO/IEC 8652:2012, известную как Ada 2012. В стандарте языка появилась возможность «контрактного программирования» (contract-based programming). В тексте программы определяется «контракт» – набор логических условий, которые будут автоматически проверяться в ходе выполнения программы в определенные моменты, например перед вызовом процедуры (предусловия) или после выполнения процедуры (постусловия). Таким образом в текст программы на языке Ada встраиваются описания формальных требований, и при выполнении программы производится проверка соответствия этим требованиям. Эти и другие новые возможности Ada 2012 соответствуют требованиям приложения DO-332 «Object-Oriented Technologies and Related Techniques» новой версии стандарта DO-178C. Полная информация об Ada 2012 на сайте www.ada2012.org.

Terma A/S применяет GNAT Pro Safety Critical
для разработки бортового ПО комплекса научного оборудования ASIM (Atmosphere-Space Interactions Monitor), который будет установлен на европейском исследовательском модуле Columbus Международной Космической Станции.
В качестве центрального процессора ASIM будет использоваться микропроцессор Aeroflex Leon3. Сейчас программное обеспечение разрабатывается с использованием GNATemulator – программном эмуляторе системы команд Leon3. Применение многозадачного профиля Ravenscar, являющегося частью стандарта языка Ada, позволяет разработчикам ПО ASIM обойтись без дополнительной операционной системы реального времени.

GNAT Pro Ada в программе модернизации штурмовика AMX бразильских ВВС
Embraer Defence and Security выбрал инструментальный комплекс GNAT Pro Ada фирмы AdaCore для разработки ПО программы модернизации штурмовика AMX бразильских ВВС (в Бразилии он называется A-1). Всего в бразильских ВВС 53 самолета A-1, произведенных фирмой Embraer c 1989 по 2000 год. Модернизация будет проведена самой современной авионикой и системами вооружений, что обеспечит продление службы самолетов еще на 20 лет.
GNAT Pro будет использоваться совместно с операционной системой VxWorks фирмы Wind River.

Saab Electronic Defence Systems применяет CodePeer
для разработки программного обеспечения многоцелевого трехмерного радара наблюдения GIRAFFE.
CodePeer – средство статического анализа текста Ada-программ с целью раннего обнаружения в них потенциальных ошибок времени исполнения (run-time errors). CodePeer позволяет находить ошибки, которые ранее можно было выявить только на самом трудоемком этапе – этапе отладки ПО. Новая версия CodePeer 2.1 полностью поддерживает последнюю версию стандарта языка Ada-2012.

Ada в спутниковой системе Argos
Thales Airborne Systems выбрала систему GNAT Pro Safety Critical компании AdaCore для разработки программного обеспечения нового поколения аппаратуры спутниковой системы Argos, которая используется для определения местоположения объектов и мониторинга состояния окружающей среды. Новое поколение Argos-4 будет поддерживать в три раза большее число передатчиков, чем сегодня работающая Argos-3. В проекте Argos-4 применяется микропроцессор LEON2, и объем программного обеспечения составит около 25000 строк на языке Ada.

Rockwell Collins применяет GNAT Pro Safety Critical
для разработки программного обеспечения интерфейсного блока EIU-7001 систем EFIS/EICAS (Electronic Flight Instrument System/Engine Indication and Crew Alert System). Блок EIU-7001 построен на микропроцессоре PowerPC и применяет безОСовый (bare board) вариант GNAT Pro SC с сертифицируемым по DO-178B исполнительным профилем ZFP (zero footprint). Большая часть ПО на языке Ada переносится с предыдущей версии блока EIU, разработанного на базе платформы Rockwell Collins AAMP.

Siemens Mobility выбирает AdaCore GNAT Pro
Siemens Mobility, транспортное подразделение Siemes AG, выбрало Ada-компилятор GNAT Pro и анализатор исходного текста CodePeer компании AdaCore для разработки нового поколения информационно-управляющей системы для железнодорожного транспорта, удовлетворяющей европейским стандартам безопасности ж/д ПО. Текущая версия системы управляет движением поездов в большей части Швейцарии, а также в некоторых районах Австрии, Венгрии и Малайзии.

GNAT Pro в EADS CASA: коммуникационная подсистема беспилотника nEUROn
Испанское подразделение CASA европейского оборонного концерна EADS отвечает за разработку наземных станций управления и коммуникационного сегмента в проекте европейского ударного беспилотника nEUROn. Программное обеспечение наземных станций и каналов связи с БЛА разрабатывается на языке Ada c с помощью инструментального комплекса GNAT Pro High Integrity Edition компании AdaCore. В качестве операционной системы используется VxWorks 653 компании Wind River. Общий объем программного обеспечения на языке Ada составит более 500,000 строк кода.

Новые продукты для верификации ПО: GNATemulator и GNATcoverage
GNATemulator – эмулятор целевой аппаратной платформы (target), позволяет исполнять ПО, скомпилированное для target-платформы, на инструментальном компьютере. Применяется для отладки ПО в случае неготовности реальной аппаратуры или невозможности обеспечения экземпляром аппаратуры каждого из разработчиков проекта.
GNATcoverage – анализатор полноты тестового покрытия на уровне объектного и исходного кода. Исполняется на эмуляторе GNATemulator и не требует инструментирования прикладного кода для сбора информации о полноте покрытия (инструментирование производится на уровне эмулятора). Анализируется полнота покрытия на уровне объектного кода (покрытие инструкций и переходов) и на уровне исходного кода (операторов, ветвей и модифицированное покрытие условий/ветвей MC/DC) для сертификации на различные уровни безопасности. На GNATcoverage имеются квалификационные материалы DO-178B до уровня A.

GNATcheck в Airbus Military A330 MRTT
Airbus Military успешно сертифицировал систему дозаправки в полете ARBS (Aerial Refueling Boom System) многоцелевого танкера/грузовика A330 MRTT (Multi Role Tanker Transport). При сертификации программного обеспечения ARBS был использован инструмент AdaCore GNATcheck – верификатор стандарта кодирования, квалифицированный по DO-178B.

MBDA применяет язык Ada и cреду разработки AdaCore GNAT Pro
Корпорация MBDA, крупнейший европейский разработчик и производитель ракетных систем, приняла язык Ada и среду разработки GNAT Pro фирмы AdaCore в качестве корпоративного стандарта. В рамках трехлетнего контракта в MBDA будет установлено 80 рабочих мест среды GNAT Pro, а также среды SPARK Pro для разработки на языке SPARK – подмножестве Ada с возможностью включения системных спецификаций в текст программы.
Корпорация MBDA, совместное предприятие BAE Systems (37.5%), EADS (37.5%) и FINMECCANICA (25%) c годовым оборотом 2.7 млрд евро, поставляет 45 ракетных и противоракетных систем и более 15 систем находится в разработке.

Barco применяет язык Ada и cреду разработки AdaCore GNAT Pro
Новая дисплейная система для бизнес-самолетов фирмы Barco основана на открытой модульной архитектуре MOSArt и разработана на языке Ada с помощью среды разработки AdaCore GNAT Pro High Integrity Edition. Для анализа трассируемости между исходным и объектным (source-to-object) кодом Barco применила инструмент GNAT Pro Traceability Kit, который значительно облегчает доказательство трассируемости при сертификации по DO-178B.

EADS Astrium выбирает Ada и GNAT Pro для разработки ПО спутниковой системы экологического мониторинга
Среда разработки GNAT Pro для языка Ada будет применяться компанией Astrium UK концерна EADS для разработки программного обеспечения спутника Sentinel-1 программы GMES (Global Monitoring for Environment and Security) Европейского Космического Агентства ESA. Среда GNAT Pro будет применяться для разработки ПО системы управления радаром с синтезируемой апертурой SAR Electronics Sub-system на базе специализированного компьютера LEON2, принятого ESA к применению в спутниковых системах. Компания Astrium уже применяет GNAT Pro в нескольких космических проектах, включая TerraSAR-X – первый германский спутник-радар для наблюдения Земли.

Thales Aerospace выбирает Ada и GNAT Pro для разработки ПО самолета Airbus A350 XWB
Среда разработки GNAT Pro для языка Ada будет применяться компанией Thales Aerospace для разработки программного обеспечения блока ADIRU (Air Data Inertial Reference Unit) самолета Airbus A350 XWB (Xtra Wide-Body). Программное обеспечение будет работать под управлением операционной системы Thales MACS2 и будет сертифицироваться по DO-178B Level A.

BAE Systems проводит общекорпоративную унификацию среды разработки на языке Ada
BAE Systems UK заключила лицензионное соглашение с AdaCore, по которому среда разработки GNAT Pro становится унифицированным общекорпоративным инструментарием для разработки проектов на языке программирования Ada. Всего лицензировано более 600 рабочих мест GNAT Pro на 15-ти различных компьютерных платформах.
BAE Systems имеет давнюю историю успешных применений языка Ada в оборонных и авиакосмических проектах, включая многоцелевой истребитель Eurofighter Typhoon, тренажер операторов систем вооружений боевых кораблей MCTS (Maritime Composite Training System), модернизацию самолетов штурмовика Harrier и разведчика Nimrod и модернизацию корабельной системы обороны SWMLU (SeaWolf Mid-Life Update).

WWW.ADACORE.COM


AVD Systems
тел: (916) 194-42-71

Все наши страницы в сети:
www.avdsys.ru/pikeos PikeOS - операционная система/гипервизор для встраиваемых систем, критически-важных для безопасности (safety) и защищенности (security)
www.avdsys.ru/ada AdaCore – средства разработки и верификации ПО на языках Ada и SPARK
www.avdsys.ru/test Cantata - комплекс средств автоматизации тестирования программного обеспечения критически-важных для безопасности, сертифицируемых встраиваемых систем
www.avdsys.ru/gpu CoreAVI - сертифицируемые по стандарту DO-178B/C драйверы стандарта OpenGL SC (Safety Critical) для различных графических процессоров и графических ядер (GPU = Graphics Processing Unit)
www.avdsys.ru/gui DiSTI GL Studio - cреда разработки 3-D графического пользовательского интерфейса (GUI) критически важных для безопасности сертифицируемых дисплейных систем
www.avdsys.ru/wcet AbsInt - средства статического (по коду программы) анализа ПО критически-важных встраиваемых систем: времени исполнения наихудшего случая WCET (Worst-Case Execution Time), объема используемого стека, наличия потенциальных ошибок времени исполнения
www.avdsys.ru/mbd Средства модельно-ориентированного проектирования (MBD = Model-Based Design).
AdaCore QGen - квалифицируемый генератор программного кода из моделей Simulink и Stateflow.
www.avdsys.ru/debug Lauterbach - аппаратные средства отладки ПО встраиваемых систем
www.avdsys.ru/atr CM Computer - бортовые корпуса формата ATR (Air Transport Rack) для модулей VPX, VME64 и CompactPCI с кондуктивным охлаждением
www.avdsys.ru/DE TTTech - оборудование Deterministic Ethernet - сетевой Технологии с передачей по Временно́му Расписанию (Time-Triggered Technology), применяемой для построения распределенных систем жесткого реального времени с гарантированным временем передачи данных
www.avdsys.ru/rugged Aitech - модули и системы VPX, VME, CompactPCI для тяжелых условия эксплуатации