Многозадачный профиль Ravenscar языка Ada сертифицирован по европейским стандартам ПО для космоса

Компания AdaCore, производитель средств разработки и верификации ПО критически важных для безопасности встраиваемых систем, провела по заказу Европейского Космического Агентства ESA сертификацию исполнительных библиотек многозадачного профиля Ravenscar языка Ada для процессоров LEON2 и LEON3. Сертификация проведена по стандартам ECSS (European Cooperation on Space Standardization) E-ST-40C и Q-ST-80C на уровень критичности для безопасности Level B.

Язык программирования Ada создавался специально для разработки ПО систем реального времени, поэтому в него с самого начала, еще в первой редакции Ada83, была введена поддержка многозадачности: возможность создания параллельно исполняющихся процессов (задач) и организации обмена данными между ними с синхронизацией доступа. Фактически исполнительная среда языка Ada содержит микроядро, благодаря которому не требуется применение внешней операционной системы реального времени и обеспечивается лучшая переносимость программного обеспечения.

Реализация полной многозадачности стандарта языка оказалась сложной для сертификации в критически важных для безопасности системах реального времени, и было разработано сертифицируемое подмножество (профиль), которое назвали Ravenscar (Воронья скала) по названию городка Ravenscar в Англии, где прошла конференция рабочей группы по разработке профиля. Например, профиль Ravenscar запрещает создание вложенных «задач», а из механизмов коммуникации между задачами допускает только «защищенные объекты».

Применение в различных проектах ESA коммерчески доступного многозадачного профиля, сертифицированного для типовой (generic) платы на базе процессоров LEON, позволит поставщикам ESA сократить затраты на сертификацию и проводить только адаптацию и валидацию сертификационного пакета для их оригинальной аппаратной платформы.

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

Дистрибьютор компании AdaCore в России – компания АВД Системы, поставщик средств разработки программного обеспечения критически важных для безопасности сертифицируемых встраиваемых компьютерных систем. Предлагаем предприятиям, заинтересованным в получении дополнительной информации о языках Ada и SPARK и современных технологиях разработки и верификации ПО, проведение бесплатного семинара.

www.avdsys.ru/ada

Следите за нашими новостями в Телеграм-канале Connect


Поделиться:



Следите за нашими новостями в
Телеграм-канале Connect

Спецпроект

Медицинские задачи для ИИ

Подробнее
Спецпроект

Цифровой Росатом

Подробнее


Подпишитесь
на нашу рассылку