Могу в свч чат кстати кинуть, может у ребят каких есть ?

👍🏻🔥

🎄

Это очень чувствительная и дорогая хренька..

и мне надо штук пять, а лучше 10.

Я в таком месте раньше работал. Купили сертифициированный генератор ansys scade за овердофига денег, чтобы пройти сертификацию и  любая обезьяна могла писать безопасный код. Оказалось, что этот сертифицированный генератор выдает программум с UB. А еще он графический. Рисуешь блоки и связи между ними. А к блоку можно вставить комментарий, который попадет в выходной с-код, экранированный /* */, но не до конца. Так вот к блоку можно написать такой комментарий: */ insert your code here  /* и да, он позволяет творить удивительные вещи.

Эти генераторы используют для того, чтобы удовлетворять каким-то том стандартам функциональной безопасности. Забыл номера. Потому что процесс должен быть сертифицирован, тулчейн должен быть сертифицирован, рабочее место должно быть сертифицировано компьютер, клавиатура, стол и стул должны быть сертифицированы. А прокладку между стулом и мониторам можно не сертифицировать.

есть же элитный, менее мартыханский formal verification - frama c например

Есть. Но, он без сертификата

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

хотя, можно же абьюзить как угодно, да

Обычно сертификатами прям на главной светят. Я пробежался по сайту и не увидел.

В целом, я верю в такое. Но про широкое распространение матлаба в авто знаю не понаслышке, хоть сам пока сам так не работал. Код, полученный из генератора, не должен редактироваться: в случае проблем редактируется сама модель. Потому что при изменении модели код опять надо исправить руками, чего и хотят избегать по максимуму.

Я видел применение формальной верификации только к плисам. Вроде как выполнение кода на ядре МК сложно поддаётся таким методам.

Да это  клёво, при разработке нажал кнопку код улетел в контроллер и сразу проверил

Это разные вещи

свч чат?

У эльпрога на каждую область знания есть чат в заначке ;-)

А для чего оно?