Мобильная версия
Войти

Все форумы
Авиационный
Сослуживцы
Авторские

На каких язіках пишут ПО для ЛА и БПЛА, и космичесских аппаратов?

2 пользователя сделали закладку на эту тему форума
 ↓ ВНИЗ

123

Baalu
Старожил форума
15.03.2017 09:48
Termi Nemo
На самом деле, как следует из нижеприведенной цитаты, автор не использует SPARK в чистом виде:

In SPARK, things are more complicated: PID functions do some calculations over the inputs, like calculating the error between the measured angle and the desired one. We’ve seen that, without any information about input ranges, it’s very difficult to prove the absence of runtime errors on calculations, even over a basic one like an error calculation (Error = Desired – Measured). In other words, we can’t implement a general PID controller using the Ada Float type if we intend to prove it with SPARK.

The good practice here is to use Ada generics: by creating a generic PID package using input, output and PID coefficient ranges as parameters, SPARK will analyze each instance of the package with all information needed to prove the calculations done inside the PID functions.

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

Как я понял, SPARK работает на этапе сборки кода, и поскольку он полностью исключает ошибки времени выполнения, exceptions тогда действительно не нужны.
На этапе сборки работает подмножество языка а на runtime полная Ada? Сомнительно как-то.
Но ладно, это его выбор :)

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

Поглядите внимательно на следующие строки:
253 Rate_Change_Gy : T_Float_4 := Rad_Gy;
254 Rate_Change_Gz : T_Float_4 := Rad_Gy;

Функция вычисления скоростей изменений координат по осям. Начальная инициализация Gy и Gz делаются одним значением текущего роложения по оси Y. Это может так дрон крутануть, что мало не покажется :)

А если здесь для оси Z применить выделенный тип - то компилятор легко отследит подобную описку. Тем более, что это оправданно. X и Y могут меняться в пределах 0..2*Pi, а для Z вполне разумно сделать ограничение по отрицательным отклонениям, что бы дрон вверх ногами в землю не пошел.
Termi Nemo
Старожил форума
16.03.2017 09:14
Действительно, для Z стоило бы сделать отдельный тип, потому что граничные условия будут другие. Видимо автор не стал копать слишком глубоко )

У него есть другая статья, где он написал Тетрис на Аде на встраиваемой платформы. Там он уже развернулся хорошо
Sergey
Старожил форума
16.03.2017 14:21
Коллеги,

Все зависит от уровня критичности системы. Уровень критичности определяется, как правило, сертификатором, описаны они в DO-178B/C.

Для наиболее критичных систем, логика описывается в моделях, то, с чем я имел дело, реальный код для дисплеев, мы использовали MATLAB/Simulink. Далее по моделям проходит автогенерация кода.

Кому интересно, вот мое выступление: https://vimeo.com/133744623

Вопросы лучше в e-mail: sglaletin@gmail.com
Phil.K
Старожил форума
17.03.2017 00:53
to Baalu
«Поглядите внимательно на следующие строки:
253 Rate_Change_Gy : T_Float_4 := Rad_Gy;
254 Rate_Change_Gz : T_Float_4 := Rad_Gy;
»
Это говорит, что данное ПО скорее всего даже не имело стендовых испытаний.
Есть два похожих языка с разными судьбами Pascal и C++. Первый имеет избыточную протоколированность (ясность) синтаксиса, за что он очень удобен в обучении, второй высокую лаконичность, за что он трудно доступен студентам. Для профессионалов избыточная многописность и функциональная рыхлость текста Pascal ведет к потере фокуса, с сути на формальные конструкции, и большему допуску банальных опечаток.

«в коде присутствует потенциально критическая ошибка, которую как раз можно было отловить средствами типизации»
А вот для языков с переделено жесткой типизацией опять будет "UPS"!
Компилятор Ada, Pascal позволит вам выполнить операцию над числом типа Gy_Type и константой 0х12 (как пример), так как он ее автоматически приведет к типу Gy_Type, если она, конечно выходит в диапазон. Но вот формулу accMAG = (acc.x*acc.x) + (acc.y*acc.y) + (acc.z*acc.z); Вы не вычислите, так как она складывает несовместимые типы (Gx_Type + Gy_Type + Gz_Type) и присваивает ее результат опять не совместимому типу.

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


«Как я понял, SPARK работает на этапе сборки кода, и поскольку он полностью исключает ошибки времени выполнения»
Ошибки "времени выполнения", исключает только программист, чей код не должен допустить условия их генерации. Run time library с исключениями только может предоставить механизм для их обработки, уж если они случились, и локализовать место (модуль) сбоя, возможно сохранив работоспособность остальных функций устройства.
Run time library без исключений просто остановит программу или даже ОС. Без возможности сигнализации отказа устройства.

Присутствие версии и числа Run time library определяет компилятор кода, сборщик обязан собрать все в одну кучу, затребованное объектными файлами.
Присутствие в одной программе более одной Run time library является серьезным риском заложить скрытый критический конфликт, ниже всех механизмов исключений. Сборка должна быть чистой.
J-Z
Старожил форума
30.03.2017 17:12
Вопрос в догон- кроме АДА, Оберона, С++, используют ли С#?
Termi Nemo
Старожил форума
30.03.2017 19:54
C# ассоциируется с виндой, которую в промышленных системах используют не очень
Phil.K
Старожил форума
30.03.2017 23:46
C# является аналогом Java от компании Microsoft.
Оба языка основаны на C++, и самое главное, целевым образом предназначены для стандартизированной среды исполнения (C# - .Net). "Среда выполнения" является фактически виртуальной операционной системой, которая может работать поверх другой OS.
Собственно связки Java - Java Virtual Machine, и C# - .Net разработаны как средства аппаратно независимого выполнения программ (компиляция программы в код CPU на самом устройстве), в том числе и на малых ЭВМ.

C# - .Net использует автоматическую сборку "мусора", динамически выделенных областей памяти и более неиспользуемых программой. Данное свойство делает эту систему номинально непригодной как Real Time & Critical, так как, заранее неизвестно время сборки "мусора", ее продолжительность и доступный объем памяти в определенные моменты времени.
Главная особенность этих систем Just In Time компилятор является обратным свойством требованию "заморозки" исполняемого кода систем специального назначения.

«Вопрос в догон- кроме АДА»
Прежде всего, используются те языки, которые предлагаются в системах разработки ПО, разработчиками данных CPU.
Вся экзотика будет гипердорогой, и не совершенной.
J-Z
Старожил форума
31.03.2017 13:00
А как насчет simit?
123




 

 

 

 

← На главную страницу

Чтобы публиковать комментарии, вы должны войти на сайт.
Все форумы
Авиационный
Сослуживцы
Авторские

Реклама на сайте Обратная связь/Связаться с администрацией
Рейтинг@Mail.ru