Учёные МГУ имени М. В. Ломоносова представили алгоритм для разработки и проверки программного обеспечения в критических системах, в том числе в бортовых комплексах самолётов. Смысл простой: ускорять код, не теряя предсказуемости его работы. Для авиации это часто важнее лишних процентов производительности. Авторы рассчитывают, что технология пригодится и при создании ПО и позже — на сертификации.
Разработку сделали специалисты факультета вычислительной математики и кибернетики МГУ. Они взяли методы безопасной компиляции и приспособили их для встроенных систем реального времени. Там любая мелкая правка в коде может отразиться на работе оборудования. И ещё одна жёсткая вещь: важна не только правильность результата, но и то, сколько именно времени займёт выполнение команды.
Проблема знакома отрасли давно. Обычные компиляторы умеют заметно ускорять программы, но их оптимизации иногда мешают формальной проверке кода и делают поведение системы менее прозрачным для инженеров. Для авиации, автопилотов, промышленных контроллеров и медицинской техники это особенно чувствительно: сертификация такого ПО требует доказать, что программа ведёт себя одинаково в заданных условиях и укладывается в жёсткие временные рамки.
На этом фоне инструмент, который учитывает требования безопасности прямо во время оптимизации, выглядит полезным не только для университетской лаборатории. Похожие задачи решают крупные поставщики авиационного софта и компиляторов — AdaCore, Wind River, Siemens. Но в России спрос на локальные решения вырос после ухода части зарубежных вендоров и курса на импортонезависимые инструменты разработки. Если метод МГУ удастся встроить в реальные цепочки проектирования, выигрыш будет не в «быстром коде», а в меньшем числе трудноуловимых ошибок на самых дорогих этапах проверки.