SPARK - это формально определенный язык компьютерного программирования, основанный на языке программирования Ada , предназначенный для разработки программного обеспечения с высокой степенью целостности, используемого в системах, где важна предсказуемая и высоконадежная работа. Это облегчает разработку приложений, требующих безопасности, защищенности или целостности бизнеса.
Парадигма | Мультипарадигма |
---|---|
Разработчик | Альтран и AdaCore |
Стабильный выпуск | 17.1 / 14 марта 2017 г . |
Печатная дисциплина | статический , сильный , безопасный , именительный падеж |
Операционные системы | Кроссплатформенность : Linux , Microsoft Windows , Mac OS X |
Лицензия | GPLv3 |
Веб-сайт | О СПАРК |
Основные реализации | |
SPARK Pro, SPARK GPL Edition | |
Под влиянием | |
Ада , Эйфелева |
Изначально существовало три версии языка SPARK (SPARK83, SPARK95, SPARK2005), основанные на Ada 83, Ada 95 и Ada 2005 соответственно.
Четвертая версия языка SPARK, SPARK 2014, основанная на Ada 2012, была выпущена 30 апреля 2014 года. SPARK 2014 - это полностью переработанный язык и вспомогательные инструменты проверки .
Язык SPARK состоит из четко определенного подмножества языка Ada, который использует контракты для описания спецификации компонентов в форме, подходящей как для статической, так и для динамической проверки.
В SPARK83 / 95/2005 контракты закодированы в комментариях Ada и поэтому игнорируются любым стандартным компилятором Ada, но обрабатываются SPARK «Examiner» и связанными с ним инструментами.
SPARK 2014, напротив, использует встроенный в Ada 2012 синтаксис «аспекта» для выражения контрактов, привнося их в ядро языка. Основной инструмент для SPARK 2014 (GNATprove) основан на инфраструктуре GNAT / GCC и повторно использует почти весь интерфейс GNAT Ada 2012.
Технический обзор
SPARK использует сильные стороны Ada, пытаясь устранить все ее потенциальные двусмысленности и небезопасные конструкции. Программы SPARK по своей конструкции должны быть однозначными, и их поведение не должно зависеть от выбора компилятора Ada . Эти цели достигаются частично за счет отказа от некоторых наиболее проблемных функций Ada (таких как неограниченное параллельное выполнение задач ) и частично за счет введения контрактов, которые кодируют намерения разработчика приложения и требования к определенным компонентам программы.
Комбинация этих подходов позволяет SPARK достичь поставленных целей проектирования, а именно:
- логическая обоснованность
- строгое формальное определение
- простая семантика
- безопасность
- выразительная сила
- проверяемость
- ограниченные требования к ресурсам (пространству и времени).
- минимальные системные требования во время выполнения
Примеры контрактов
Рассмотрим спецификацию подпрограммы Ada ниже:
Процедура Приращение (Х: в из counter_type);
В чистом Ada это могло бы увеличить переменную X
на одну или одну тысячу; или он может установить некоторый глобальный счетчик X
и вернуть исходное значение счетчика X
; или он может вообще ничего не делать X
.
В SPARK 2014 в код добавляются контракты, чтобы предоставить дополнительную информацию о том, что на самом деле делает подпрограмма. Например, мы можем изменить приведенную выше спецификацию, чтобы сказать:
приращение процедуры (X: in out Counter_Type) с Global => null , Зависит => (X => X);
Это указывает, что Increment
процедура не использует (не обновляет и не читает) какие-либо глобальные переменные и что единственный элемент данных, используемый при вычислении нового значения, X
- это он X
сам.
В качестве альтернативы дизайнер может указать:
приращение процедуры (X: in out Counter_Type) с Global => (In_Out => Count), Зависит => (Счетчик => (Счетчик, X), X => ноль);
Это указывает, что Increment
будет использовать глобальную переменную Count
в том же пакете Increment
, что и экспортируемое значение, которое Count
зависит от импортированных значений Count
и X
, и что экспортируемое значение X
не зависит от каких-либо переменных вообще и будет получено только из константных данных. .
Если затем GNATprove запускается для спецификации и соответствующего тела подпрограммы, он проанализирует тело подпрограммы для построения модели информационного потока. Затем эта модель сравнивается с той, которая была указана в аннотациях и любых расхождениях, сообщаемых пользователю.
Эти спецификации могут быть дополнительно расширены путем утверждения различных свойств, которые либо должны сохраняться при вызове подпрограммы ( предварительные условия ), либо сохраняться после завершения выполнения подпрограммы ( постусловия ). Например, мы могли бы сказать следующее:
приращение процедуры (X: in out Counter_Type) с Global => null, Зависит => (X => X), Pre => X'last, Сообщение => X = X'Old + 1;
Теперь это указывает не только на то, что X
извлекается только из него самого, но также на то, что перед Increment
вызовом X
должно быть строго меньше, чем последнее возможное значение его типа, и что впоследствии X
будет равно начальному значению X
плюс один.
Условия проверки
GNATprove также может генерировать набор условий проверки или VC. Эти условия используются, чтобы установить, выполняются ли определенные свойства для данной подпрограммы. Как минимум, GNATprove сгенерирует VC, чтобы установить, что все ошибки времени выполнения не могут возникать в подпрограмме, например:
- индекс массива вне допустимого диапазона
- нарушение диапазона типов
- деление на ноль
- числовое переполнение.
Если в подпрограмму добавлено постусловие или любое другое утверждение, GNATprove также сгенерирует VC, которые потребуют от пользователя показать, что эти свойства сохраняются для всех возможных путей через подпрограмму.
Под капотом GNATprove использует промежуточный язык Why3 и генератор VC, а также средства доказательства теорем CVC4, Z3 и Alt-Ergo для разгрузки VC. Использование других программ доказательства (включая интерактивные средства проверки правописания) также возможно через другие компоненты набора инструментов Why3.
История
Первая версия SPARK (на основе Ada 83) была создана в Университете Саутгемптона (при спонсорской поддержке Министерства обороны Великобритании ) Бернаром Карре и Тревором Дженнингсом. Впоследствии язык был постепенно расширен и усовершенствован, сначала Program Validation Limited, а затем Praxis Critical Systems Limited. В 2004 году Praxis Critical Systems Limited изменила свое название на Praxis High Integrity Systems Limited. В январе 2010 года компания стала Altran Praxis .
В начале 2009 года Praxis заключила партнерство с AdaCore и выпустила SPARK Pro на условиях GPL. За этим в июне 2009 года последовала SPARK GPL Edition 2009, нацеленная на СОПО и академические сообщества.
В июне 2010 года Altran-Praxis объявила, что язык программирования SPARK будет использоваться в программном обеспечении американского лунного проекта CubeSat , завершение которого ожидается в 2015 году.
В январе 2013 года компания Altran-Praxis сменила название на Altran.
О первом выпуске Pro версии SPARK 2014 было объявлено 30 апреля 2014 года, а вскоре за ним последовала версия SPARK 2014 GPL, нацеленная на FLOSS и академические сообщества.
Промышленное применение
SPARK использовался в нескольких важных для безопасности системах, охватывающих коммерческую авиацию ( реактивные двигатели серии Rolls-Royce Trent , система ARINC ACAMS, Lockheed Martin C130J), военную авиацию ( EuroFighter Typhoon , Harrier GR9, AerMacchi M346), воздушную - управление движением (система UK NATS iFACTS), железнодорожные (многочисленные приложения для передачи сигналов), медицинские ( вспомогательное устройство для желудочков LifeFlow ) и космические приложения ( проект CubeSat Технического колледжа Вермонта ).
SPARK также использовался при разработке безопасных систем. Пользователи включают Rockwell Collins (междоменные решения Turnstile и SecureOne), разработку оригинального MULTOS CA, демонстратор NSA Tokeneer, многоуровневую рабочую станцию secunet, ядро разделения Muen и шифратор блочных устройств Genode.
В августе 2010 года Род Чепмен, главный инженер Altran Praxis, внедрил Skein , одного из кандидатов на SHA-3 , в SPARK. При сравнении производительности реализаций SPARK и C и после тщательной оптимизации ему удалось добиться того, чтобы версия SPARK работала всего на 5-10% медленнее, чем C. Позднее усовершенствование среднего уровня Ada в GCC (реализовано Эриком Ботказоу из AdaCore ) закрыл пробел, при этом код SPARK точно соответствовал C по производительности. [1]
Смотрите также
Заметки
- ↑ Handy, Alex (24 августа 2010 г.). «Криптовалюта Skein, производная от Ada, показывает SPARK» . SD Times . ООО "БЗ Медиа" . Проверено 31 августа 2010 . CS1 maint: обескураженный параметр ( ссылка )
Рекомендации
- Джон Барнс (2012). SPARK: проверенный подход к высоконадежному программному обеспечению . Altran Praxis. ISBN 978-0-9572905-1-8.
- Джон В. Маккормик и Питер С. Чапин (2015). Создание высоконадежных приложений с помощью SPARK 2014 . Издательство Кембриджского университета. ISBN 978-1-107-65684-0.
- Филип Э. Росс (сентябрь 2005 г.). «Истребители» . IEEE Spectrum . 42 (9): 36–41. DOI : 10.1109 / MSPEC.2005.1502527 . ISSN 0018-9235 .
Внешние ссылки
- Сайт сообщества СПАРК 2014
- Сайт SPARK Pro
- Веб-сайт SPARK Libre (GPL) Edition
- Альтран
- Правильность по конструкции: манифест для высоконадежного программного обеспечения
- Клуб критических систем безопасности Великобритании
- Сравнение с языком спецификации C (Frama C)
- Страница проекта Tokeneer
- Публичный выпуск ядра Muen
- Проект LifeFlow LVAD
- Проект VTU CubeSat