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

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


Опубликовано руководство по применению 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 для тяжелых условия эксплуатации