Комментарии 58
Процесс разработки ПО для авиационной техники определен квалификационными требованиями DO-178C или переведенный на русский КТ-178С. Тестирование ПО это лишь вершина айсберга процесса разработки ПО для авиации.
И рассматривали ли Escher C Verifier?
Сильный порыв ветра и кирдык.
Резеревирование 2 из 3 будете добавлять?
«пыльных трудах института системного программирования РАН, которые как будто бы от жизни отстают лет на 30, а то и 50» — это для красного словца, или можете привести хотя бы отдельные примеры (не говоря уж о «при этих словах люди начинают думать»)? Да-да, по теме «верификация ПО». Я наверно знаю про пару пожилых сотрудников (Е.Л.), которые наверное могут что-то совсем олдскульное написать, но вдруг реально проблема и с молодежью, и действительно все плохо, серьезно, просветите.
Видимо, под трудами ИСПРАН вы имели в виду любое творчество, как-то сводимое к сотрудникам ИСПРАН (ну да, есть пожилые сотрудники, у них были относительно олдскульные курсы для младшекурсников, возможно вы наткнулись на курсы Л×××ва, или Л×××вой) — именно это предпредложение я добавил в комментарий (не хотел дробить). Но Труды ИСПРАН это вполне определенный рецензируемый журнал, и если там проходит дичь и древности по верификации, мне это было бы интересно — я смог бы найти рецензентов, ну и повлиять, чтобы никогда. А так, по моим данным, уровень проектов, тем, технологий по верификации там вполне на уровне.
Презентованное там почти всегда применяется в каких-то проектах и продуктах, институт ведет множество таковых, «чистой науки для души» там практически нет. Есть и проекты для верификации ОСРВ и сертифицированной авионики в частности… но тут я только знаю, что они есть (тут я не очень в теме, а для меня верификация это пока хобби и в основном в части автоматических доказательств).
К чему это я — может стоит убрать риторический абзац о «пыльных трудах института системного программирования РАН»? По моему мнению, условных 95% открывших эту статью, прочтут пару первых вводных абзацев с игривым тоном, и не полезут в скучные подробности, не говоря уже о комментариях. Но где-то этот абзац отложится, с меткой «на хабре считают что…». Это же нехорошо.
«Затем наступают «темные века», которых найти не удается, и потом в 2017 году снова появляются материалы»
— возможно вы зашли на страницу «последних выпусков» (там номера с 2017), но не прошли по ссылке «полный архив» ← там номера с 2000 → и вот так, появилась «хронология Скалигера с темными веками». На всякий случай, для прохожих — это не так, проекты и темы (особенно по верификации), в ИСПРАНе развивались методично и равномерно. Кроме статей, часто получалось, когда я снимал разные доклады, что именно по темам верификации, включая весьма прикладные аспекты, именно ИСПРАНовские ребята попадались чаще всего.
Привет (если меня помните)!
Ну вместо названий наверно интересней конкретные фамилии, давайте зацепимся в поиске за http://www.mathnet.ru/php/person.phtml?option_lang=rus&personid=125232 например.
(наверно это группа Петренко… но не уверен).
Ну и в целом там наверно больше Isabelle, что-то там совместно с микрософтом по Z3.
Могу поспрашивать, наверно, если что, как я уже сказал, я в этом не специалист, только сам пытаюсь разобраться…
Курс по алгоритмам, 6 курс, ФУПМ. Или я ошибся?
ну только JetBrains Research в голову приходит, на самом деле, и то относительно мало.
Что-то в тиньков банке даже, судя по курсам, в хуавее русском… не только жетбрейнс.
а можно слоупокам отдельно разжевать — почему же всё таки не Раст?
Как я понял из статьи, SPARK позволяет больше инвариантов обеспечить. Например, в Rust нет возможности ограничения и compile-time проверки допустимых значений, compile-time проверки выхода за границы массива итп.
alastairreid.github.io/rust-verification-tools
хочется привести табличку, показывающую, что “старичок» Ada еще огого:Табличка хороша, но в ней слишком много языков, далеких от embedded. Поэтому сравнивать Ada с ними в данном случае некорректно.
Впервые встретил список литературы в формате [XXX].
Это Ваше изобретение, или новый тренд?
В любом случае, хотелось бы услышать про обоснование и преимущества перед классическим [1].
Источники в списке литературы, на мой взгляд, лучше расположить по алфавиту, а не по мере их упоминания в тексте. Так их можно быстрее найти.
Я пока только собираю и изучаю. Просто подумалось, что может что то от россиян в этом деле появится. Свое, так сказать, сермяжное, скрепное. А то детали все китайские, прошивки забугорные, воздух только родимый))
Внешний цикл это цикл опроса периферии (CMD task на рисунке) в ожидании команд с радиопередатчика. Если команды нет, он передает признаки «сохраняем высоту, держим горизонт». Если команда с пульта есть, передаем ее — целевой угол наклона, целевую мощность на пропеллеры. Частота внешнего цикла 20 Гц.
Внутренний цикл — цикл опроса гиро-акселерометра и распределения мощности на двигатели. Цикл оборудован 3 PID-регуляторами, и математикой Махони для расчета текущего положения по сигналам с гироскопов.
Я уверен, что, раз вы смотрели исходники xxxflight'ов, то вы это и без меня знаете, ну да ладно. Насколько мне известно, в xxxflight'ах стабилизация осуществляется по угловой скорости (acro/air режим), а режим удержания горизонта прикручен уже поверх. Возможно, ваше решение лучше для стабилизации в горизонт.
Так как у нас нет ни баровысотомера, и другого способа измерить высоту, то для грубого удержания высоты используем интеграцию вертикальной скорости.
Интересно. Я когда-то (лет 6 назад, когда еще был MultiWii) хотел что-то такое сделать, но так и не сделал. На бумаге гладко, но я предполагаю очень большие накопленные ошибки из-за шумов акселерометра и погрешностей определения ориентации. Можете сказать пару слов об этой фиче?
Мы: Нужно сделать одну нормальную, а не как эти 5 багоделов
Стало: 6 обычных прошивок для полетных контроллеров
- А вы видели Ada + SPARK Crazyflie 2.0 firmware?
- Ещё было продолжение выигравшее приз на Make with Ada 2021
- А ещё был планер на SPARK
- Приходите к нам в телеграм канал по Аде!
- Добавьте, если можно, тег #ada, чтобы статья легче находилась.
Кто ошибся?
Но AdaMagic из коробки для Linux и Windows, а на других надо что-то думать с механизмом исключений, портировать рантайм. Нет исключений — нет рантайма — нет проблем.
Тут еще xrEon понимаете ли накинул, оказывается проектов на Аде больше, чем три с половиной! ЧСХ писать на Аде под писюк наверное станет только псих (когда есть элитный шарп), а вот в эмбеде оно и правда хорошо.
К слову, раз тут знатоки собрались, переспрошу кое-что, что я не понял — есть аспект, с помощью которого можно задать минимальный размер типа в битах, но как задать точный размер?
ЧСХ писать на Аде под писюк наверное станет только псих (когда есть элитный шарп)
Помню, Delphi сначала начали делать под .NET. Настоящее унижение, что моё любимое число 8, в долгожданной версии Delphi 8 стало проклятьем, эта Delphi ничего другого не умела. Потом какая-то муха покусала многих разработчиков, они к мёду нативных программ начали подмешивать дёготь дотнета. И МатКАД, и АвтоКАД, и не обошла беда стороной RAD Studio. Подсказки кода почему-то надо было сделать в дотнетовской части. К счастью, нашлись народные умельцы. В Delphi 10 Lite вырезано всё, что связано с дотнетом.
Вот так нативной частью программы, без трассирующей сборки мусора, народ с удовольствием пользуется, а дотнетовскую дрянь отпилит первый же риппер. А какую часть хотите писать вы?
на шарпе писать хорошо, очень хорошо
Я говорю про Служение Пользователю, а не самоудовлетворение разработчика.
И Ада ещё больше, чем Delphi, про Служение Пользователю.
достаточный объем платформы для Ады под ПиСи
Не понял. Чего не хватает. Вот есть задачи, которые надо решать. На шарпе будет дико тормозить, особенно, на офисных компах старинных, закупленных сотнями, в которые ещё принудительно антивирус воткнут. На плюсах будет дико глючить. На Аде и Делфи будет работать хорошо.
Как мы верифицированный полетный контроллер для квадрокоптера написали. На Ada