Как стать автором
Обновить

Комментарии 57

Процесс разработки ПО для авиационной техники определен квалификационными требованиями DO-178C или переведенный на русский КТ-178С. Тестирование ПО это лишь вершина айсберга процесса разработки ПО для авиации.

Да, спасибо, планировал во второй части уточнить. КТ-178С не читал, а вот DO-178C, а точнее, DO-178B, не определяет, а, скорее, рекомендует. Конечно, для квадрокоптера-игрушки рассматривать квалификацию по этим гайдлайнам можно разве что из любви к искусству

Конечно, это только для такси, для эксплуатации придется получить одобрение авиационных властей.

Интересно, почему Frama-C отнесли к прототипам, а не зрелым промышленным решениям?
И рассматривали ли Escher C Verifier?
Escher C не рассматривали, наверняка, в нем можно много интересного найти. Но что касается Си, то не хотелось идти путем MISRA и определять для себя «хороший С» и «не очень хороший С» — по ощущениям, такие игры уведут нас в другом направлении. FramaC среди себя обозвали прототипом, потому что это, скорее, конструктор для построения собственного верификатора, а к такому трудовому подвигу готовы не были
В статье всё звучит более категорично.
И MISRA C — это не про «хороший С», его назначение перекликается со SPARK для Аda.
Есть какие-то сравнительные тесты качества вашего кода и бетафлай? Вы проводили, скажем, статическую проверку их кода, прежде чем начинать работу?
Перед нет, а в процессе разработки сравнивали, хотя целесообразность вызывает вопросы. Более детально архитектуру и результаты тестирования планируем во второй части опубликовать

«пыльных трудах института системного программирования РАН, которые как будто бы от жизни отстают лет на 30, а то и 50» — это для красного словца, или можете привести хотя бы отдельные примеры (не говоря уж о «при этих словах люди начинают думать»)? Да-да, по теме «верификация ПО». Я наверно знаю про пару пожилых сотрудников (Е.Л.), которые наверное могут что-то совсем олдскульное написать, но вдруг реально проблема и с молодежью, и действительно все плохо, серьезно, просветите.

Не очень понятно, с чего вы решили, что приемлема такая снисходительная панибратская риторика в комментариях. Или может быть, вы себя вообразили экзаменатором, а авторов студентами?

Уверяю, не хотел никого обидеть. Хотя ваше утверждение «пыльных трудах института системного программирования РАН, которые как будто бы от жизни отстают лет на 30, а то и 50» как раз является панибратским и менторским, и, по-моему мнению, действительно может кого-то обидеть.

Спасибо за пояснения. Я постарался ответить ниже картину взглядом инженера обычной прикладной лаборатории
О, вижу, вы добавили в комментарии. Большая часть материалов и учебных курсов ИСП РАН по верфикации ПО, доступные в паблике, ссылаются на опыт, методы и инструменты от условно 1978-1989 до 2000-2005 года. Затем наступают «темные века», которых найти не удается, и потом в 2017 году снова появляются материалы, наработки, семинары и презентации, но уже коммерческих инициатив либо отсылок к зарубежному опыту

Видимо, под трудами ИСПРАН вы имели в виду любое творчество, как-то сводимое к сотрудникам ИСПРАН (ну да, есть пожилые сотрудники, у них были относительно олдскульные курсы для младшекурсников, возможно вы наткнулись на курсы Л×××ва, или Л×××вой) — именно это предпредложение я добавил в комментарий (не хотел дробить). Но Труды ИСПРАН это вполне определенный рецензируемый журнал, и если там проходит дичь и древности по верификации, мне это было бы интересно — я смог бы найти рецензентов, ну и повлиять, чтобы никогда. А так, по моим данным, уровень проектов, тем, технологий по верификации там вполне на уровне.

Нет, именно никакой журнал не имеется в виду, тем более такой авторитетный. Как именно применить презентованное там, это другой вопрос

Презентованное там почти всегда применяется в каких-то проектах и продуктах, институт ведет множество таковых, «чистой науки для души» там практически нет. Есть и проекты для верификации ОСРВ и сертифицированной авионики в частности… но тут я только знаю, что они есть (тут я не очень в теме, а для меня верификация это пока хобби и в основном в части автоматических доказательств).


К чему это я — может стоит убрать риторический абзац о «пыльных трудах института системного программирования РАН»? По моему мнению, условных 95% открывших эту статью, прочтут пару первых вводных абзацев с игривым тоном, и не полезут в скучные подробности, не говоря уже о комментариях. Но где-то этот абзац отложится, с меткой «на хабре считают что…». Это же нехорошо.

Согласен, убрал
«Затем наступают «темные века», которых найти не удается, и потом в 2017 году снова появляются материалы»

— возможно вы зашли на страницу «последних выпусков» (там номера с 2017), но не прошли по ссылке «полный архив» ← там номера с 2000 → и вот так, появилась «хронология Скалигера с темными веками». На всякий случай, для прохожих — это не так, проекты и темы (особенно по верификации), в ИСПРАНе развивались методично и равномерно. Кроме статей, часто получалось, когда я снимал разные доклады, что именно по темам верификации, включая весьма прикладные аспекты, именно ИСПРАНовские ребята попадались чаще всего.

А какие научные группы в РАН занимаются формальной верификацией в смысле всяких коков и прочих агд?

Привет (если меня помните)!


Ну вместо названий наверно интересней конкретные фамилии, давайте зацепимся в поиске за http://www.mathnet.ru/php/person.phtml?option_lang=rus&personid=125232 например.
(наверно это группа Петренко… но не уверен).


Ну и в целом там наверно больше Isabelle, что-то там совместно с микрософтом по Z3.
Могу поспрашивать, наверно, если что, как я уже сказал, я в этом не специалист, только сам пытаюсь разобраться…

Привет (если меня помните)!

Увы, не помню :( Подкиньте ключевое слово или воспоминание!


В любом случае, спасибо за пример — что-то действительно происходит, и это хорошо.


У меня нет цели принизить как-то РАН, просто я сужу по своим впечатлениям от того, какие аффилиации авторов статей, которые мне попадаются на глаза. В США довольно много народу, в Британии есть народ, во Франции, естественно, много по этой теме (такая-то философско-математическая школа!), в Швеции пара человек наберётся, а в РФ — ну только JetBrains Research в голову приходит, на самом деле, и то относительно мало.

Вы не ошиблись! Я просто сначала только по нику пытался вспомнить, а теперь посмотрел, что у вас тут ещё и имя написано, и вспомнил :)


С моей стороны давать задачку для будущих поколений на квайны было, конечно, перебором.

ну только JetBrains Research в голову приходит, на самом деле, и то относительно мало.

Что-то в тиньков банке даже, судя по курсам, в хуавее русском… не только жетбрейнс.

Почему не раст — это понятно. Но почему не какой-нибудь кок с экстракцией в C? Если spark опирается на SMT-решатель, то понятно, что его выразительная сила сильно ограничена AMT-разрешимыми теориями.

Даже не думалось над вариантом Coq. А у вас есть варианты почитать что-то про создание ПО для automotive или aerospace на Coq?

Это надо BAE спрашивать (я даже видел пару лет назад какие-то их публикации на тему, но сейчас сходу найти не могу), и вроде у Boeing ещё что-то было.

а можно слоупокам отдельно разжевать — почему же всё таки не Раст?

Как я понял из статьи, SPARK позволяет больше инвариантов обеспечить. Например, в Rust нет возможности ограничения и compile-time проверки допустимых значений, compile-time проверки выхода за границы массива итп.

Из коробки не может, как и чистая Ада, без SPARK. Но вот тут какие-то инструменты вижу:
alastairreid.github.io/rust-verification-tools

Да, рядом правильно написали — потому что раст позволяет доказывать меньше вещей про код. Да, доказать что-то про отсутствие гонок (средствами компилятора! без обмазывания сепарационной логикой и вот этим всем!) — это круто и полезно, серьёзно, но это — лишь малая часть того, что можно доказывать на машине про код.

Кажется, я начинаю понимать, почему путаюсь в ваших комментариях :) Для меня, по складу ума императивщика, правильнее говорить не «доказать», а «описать порядок владения данными такой, что гонки отсутствуют». Т.е. доказательство как бы есть, но первичны все-таки действия программиста, а «академики» это немного замыливают.
что в итоге, упало, или нет?
Еще нет, но разобьем обязательно!
хочется привести табличку, показывающую, что “старичок» Ada еще огого:
Табличка хороша, но в ней слишком много языков, далеких от embedded. Поэтому сравнивать Ada с ними в данном случае некорректно.

Впервые встретил список литературы в формате [XXX].
Это Ваше изобретение, или новый тренд?
В любом случае, хотелось бы услышать про обоснование и преимущества перед классическим [1].
Источники в списке литературы, на мой взгляд, лучше расположить по алфавиту, а не по мере их упоминания в тексте. Так их можно быстрее найти.
Хм… тоже впервые вижу, но вроде удобно — семантические короткие названия. Чем-то напоминают семантические имена ссылок в *TeX. Если бы список был на 50-60 ссылок, то сортировка по алфавиту действительно была бы удобнее для поиска.
Я правильно понял из начала статьи, что betaflight это «страх и ужас», а из конца статьи, что после схода снега вы выкатите свою прошивку для полетных контроллеров?)
Таких планов не было — стоимость переключения на другую прошивку неподъемная, плюс разные cleanflight, betaflight предлагают значительно больший объем сервиса, которого в прототипе нет и не планируется. Но можно обсудить разработку безопасной прошивки конкретно под вашу плату
Нее, спасибо!
Я пока только собираю и изучаю. Просто подумалось, что может что то от россиян в этом деле появится. Свое, так сказать, сермяжное, скрепное. А то детали все китайские, прошивки забугорные, воздух только родимый))
В рамках текущей задачи вроде бы Вы говорите о некой комманде, употребляя «Мы». Расскажите, каким составом и численностью работали над этим? И в какой срок все вышло?
Делало 2 человека в свободное время, вышло чуть больше полутора месяцев, в общем часов 150-200, наверное
Внешний цикл это цикл опроса периферии (CMD task на рисунке) в ожидании команд с радиопередатчика. Если команды нет, он передает признаки «сохраняем высоту, держим горизонт». Если команда с пульта есть, передаем ее — целевой угол наклона, целевую мощность на пропеллеры. Частота внешнего цикла 20 Гц.
Внутренний цикл — цикл опроса гиро-акселерометра и распределения мощности на двигатели. Цикл оборудован 3 PID-регуляторами, и математикой Махони для расчета текущего положения по сигналам с гироскопов.

Я уверен, что, раз вы смотрели исходники xxxflight'ов, то вы это и без меня знаете, ну да ладно. Насколько мне известно, в xxxflight'ах стабилизация осуществляется по угловой скорости (acro/air режим), а режим удержания горизонта прикручен уже поверх. Возможно, ваше решение лучше для стабилизации в горизонт.


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

Интересно. Я когда-то (лет 6 назад, когда еще был MultiWii) хотел что-то такое сделать, но так и не сделал. На бумаге гладко, но я предполагаю очень большие накопленные ошибки из-за шумов акселерометра и погрешностей определения ориентации. Можете сказать пару слов об этой фиче?

Было: 5 обычных прошивок для полетных контроллеров
Мы: Нужно сделать одну нормальную, а не как эти 5 багоделов
Стало: 6 обычных прошивок для полетных контроллеров
А код открыт? Интересно было бы посмотреть.
Работа лицензирована по GPL v3, так что код пока посмотреть не получится
Статья бомба! Спасибо!

Да, спасибо, но там совсем другая платформа (два процессора), плюс код заброшен — я так понял, это была короткая работа силами студентов, а летает все равно сишная прошивка, плюс в сенсорфьюжне Махони также есть ошибки
В статье приведена ссылка на статью «Toyota: 81564 ошибки в коде». Переходим по ней и читаем её название «Toyota: 81 514 нарушений в коде».

Кто ошибся?
Применительно к таблице из [EFF], раз уж мы доказали отсутствие исключений, то можно исключать проверки из кода, и тогда скорость повыше. По такому пути шли в проекте CubeSat, попутно решая другую проблему. Родного транслятора Ады для National Instruments нет, взяли AdaMagic.

Но AdaMagic из коробки для Linux и Windows, а на других надо что-то думать с механизмом исключений, портировать рантайм. Нет исключений — нет рантайма — нет проблем.
Теперь вы в списке людей, которых я ненавижу. Вы лично, и все упомянутые в статье коллеги. Мало того, что вы там все пипец умные и пишете полетные контроллеры (а я занимаюсь непонятно чем и пятый год только мечтаю этим заняться), так еще и делаете это на Аде! Я недавно с крайним удивлением на Адакоре увидел чудесные разделы (клянусь, что джва года назад их не было) и запоем прочитал записки «как с С/С++ перейти на Аду». Отметил впрочем, что на плюсах все то же самое (и даже больше) можно сделать даже проще (но не очень), а еще чот кода готового маловато на Аде, и вербозно как-то (хотя я любитель длинных имен), и задрачивать новый язык все же придется сильно, и вообще слезы_боль_я_никто, в общем прочитал — и ничего на Аде писать не стал, даже никакой крохотной фитюлечки.

Тут еще xrEon понимаете ли накинул, оказывается проектов на Аде больше, чем три с половиной! ЧСХ писать на Аде под писюк наверное станет только псих (когда есть элитный шарп), а вот в эмбеде оно и правда хорошо.

К слову, раз тут знатоки собрались, переспрошу кое-что, что я не понял — есть аспект, с помощью которого можно задать минимальный размер типа в битах, но как задать точный размер?
ЧСХ писать на Аде под писюк наверное станет только псих (когда есть элитный шарп)


Помню, Delphi сначала начали делать под .NET. Настоящее унижение, что моё любимое число 8, в долгожданной версии Delphi 8 стало проклятьем, эта Delphi ничего другого не умела. Потом какая-то муха покусала многих разработчиков, они к мёду нативных программ начали подмешивать дёготь дотнета. И МатКАД, и АвтоКАД, и не обошла беда стороной RAD Studio. Подсказки кода почему-то надо было сделать в дотнетовской части. К счастью, нашлись народные умельцы. В Delphi 10 Lite вырезано всё, что связано с дотнетом.

Вот так нативной частью программы, без трассирующей сборки мусора, народ с удовольствием пользуется, а дотнетовскую дрянь отпилит первый же риппер. А какую часть хотите писать вы?
Признаться, я не понял, к чему вы клоните, я просто исхожу из того, что на шарпе писать хорошо, очень хорошо. Если вам нравится на Дельфи — не проблема. Но уж точно вряд ли есть достаточный объем платформы для Ады под ПиСи.
на шарпе писать хорошо, очень хорошо

Я говорю про Служение Пользователю, а не самоудовлетворение разработчика.

И Ада ещё больше, чем Delphi, про Служение Пользователю.

достаточный объем платформы для Ады под ПиСи


Не понял. Чего не хватает. Вот есть задачи, которые надо решать. На шарпе будет дико тормозить, особенно, на офисных компах старинных, закупленных сотнями, в которые ещё принудительно антивирус воткнут. На плюсах будет дико глючить. На Аде и Делфи будет работать хорошо.
Ну если речь про Служение, то тут наверное можно только согласиться.
Вот бы ещё Пользователям объяснить, что адаисты им Служить хотят, чтоб со стороны Пользователей осознанное финансовое давление шло.
Спешу напомнить, что пищат моторы независимо от прошивки полётного контроллера. Писк этот генерирует прошивка регулятора. для проверки можете подать питание на регулятор с мотором без подключенного контроллера. Не думаю, что люди из авиации в добром уме и здравой памяти посадят человека в машину под управлением Cleanflight и тому подобных ПО
Только полноправные пользователи могут оставлять комментарии. Войдите, пожалуйста.