НовостиСобытияКонференцииФорумыIT@Work
Идеи и практики автоматизации:

Блог

Чтобы спутники не падали

Сергей Бобровский
01.09.2011 10:41:41

Главным трендом на рынке систем верификации ПО становятся технологии математического доказательства правильности программ. Дополняют они системы статического анализа кода и динамического тестирования работы софта. Об этом изданию Military & Aerospace Electronics поведал Robert Dewar, CEO компании AdaCore Technologies.

Подобные технологии разрабатываются давно, и наработки существуют неплохие, но пока они не стали массовой практикой -- например, из-за сложности и ограниченности применения. Некоторые особо строгие стандарты сертификации защищенных систем подразумевают подобную формальную проверку, но пока удавалось проверять объемы кода в ограниченных пределах, до 10 тыс. строк кода (по кр. мере, официально сообщалось о таких объемах).
Чипы сегодня встраиваются куда только можно -- и в современном автомобиле программного кода уже больше, нежели в коммерческом авиалайнере (цикл проектирования самолетов гораздо дольше). И, соответственно, по мере всеобщей автоматизации растет и потенциальная опасность программных ошибок (например, известны случаи трагических сбоев медицинской цифровой аппаратуры).

Одна из компаний, наиболее активно инвестирующих в сферу математического доказательства -- MathWorks. Она готовит, по словам ее менеджера по аэрокосмической и оборонной индустрии Джона Фридмана, "новый класс верификационных инструментов", которые потенциально способны обеспечить абсолютную корректность кода. Еще один из редких игроков в этой узкой из-за высокого порога вхождения, но крайне перспективной нише -- компания LDRA, предлагающая верификационный софт для всего жизненного цикла. 20-го августа она, кстати, отметила юбилей своего индийского офиса, который активно взаимодействует с местными государственными структурами -- оборонными, космическими, ядерными, транспортными и др. Занимается она в Индии, что немаловажно, интенсивным обучением, семинарами по IEC 61508, DO-178B, IEC 62304, ISO 26262, MISRA C++, CERT C, работает в организациях, занимающихся стандартизацией программной инженерии...

А почему в России ее представительства нету? Сомневаюсь, что у нас имеются продвинутые компании схожего профиля -- судя хотя бы по падающим в океаны ракетам...

Комментариев: 4

Только зарегистрированные и авторизованные пользователи могут добавлять комментарии

Alexey Khoroshilov
02.09.2011 10:08:17

Насчет коммерческих компаний не знаю, а несколько команд занимающихся этим направлением в России есть. Например, у нас, в Институте системного программирования РАН, ведется активная работа и по статическому анализу кода, и по model checking, и по аналитическому доказательству корректности программ.

Из открытых результатов можно привести деятельность Центра верификации ОС Linux, в которой некоторые наши инструменты применяются для анализа ядра и библиотек Linux. Для примера можно посмотреть на список обнаруженных проблем в драйверах: http://linuxtesting.ru/results/ldv

Знаю, что LDRA использовался в Ульяновском УКБП при разработке концентратора данных для СуперДжета. Что касается спутников ничего сказать не могу, с космической промышленностью у нас контактов не было.

02.09.2011 10:53:10

Интересно, а расскажите, в каких еще прикладных проектах ваши наработки применяются, на каком они уровне, в сравнении с той же LDRA? Пост можете в этот блог написать, было бы здорово.
Спасибо про Ульяновск! Попробую с ними связаться.

Владимир.
05.09.2011 01:21:45

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

Её обитатели собираются оперативно принять поправки к Закону всемирного тяготения.

Владимир
11.02.2012 23:13:34

Если кого-то заинтересует более подробная информация по существующим верификационным инструментам в области разработки критичных приложений пишите мне на почту cmex81@gmail.com

Только зарегистрированные и авторизованные пользователи могут добавлять комментарии