вторник, 8 декабря 2009 г.

[comp.prog] Где же используются системы анализа и верификации программ?

Попробовал поискать информацию о том, где использовались, используются или будут использоваться средства для анализа и верификации программ (по следам заметки у меня в блоге и в блоге “Алёна C++”).

Анализатор C-шных программ под названием ASTREE использовался для верификации частей бортового ПО Airbus A340 (2003-й год), ПО Airbus A380 (2004-й год) и ПО для управления стыковой космического аппарата Jules Vernes Automated Transfer Vehicle. (Все это написано на стартовой странице проекта).

Язык SPARK (специальное подмножество языка Ada о котором я когда-то уже упоминал) выбрали для реализации части ПО нового боевого вертолета в Англии. Ранее SPARK Ada был выбран в качестве инструмента для разработки ПО для планирования и управления полетами самолетов (eao197: если я не ошибся в переводе). Так же в 2007-м году Paraxis (разработчик SPARK-а) был назначен исполнителем £10-миллионного контракта на разработку новой системы контроля за авиатрафиком в Англии. В 2006-м году Paraxis выиграл контракт на разработку ПО для Engine Monitoring Unit для двигателя Rolls-Royce Trent 1000 (который планировалось использовать в Boeing 787). (Эта информация была найдена в разделе News компании Paraxis High Integrity Systems. Там же упоминалось, что они имеют опыт разработки ПО для нескольких поколений боевых самолетов-истребителей.)

Продукт Parasoft C++test использовался для тестирования ПО систем контроля и управления (компания Intermoco из Австрации), для тестирования ПО систем кондиционирования воздуха (компания Trane). для тестирования ПО для хирургического оборудования (компания Bovie Medical Corporation), для тестирования ПО в области телекоммуникаций и мобильной связи (компания NEC Telecom Software Philippines). (Эта информация была найдена в разделе С++test Case Studies. Все материалы очень поверхностные, обычный коммерческий bullshit, но последняя более-менее интересная.)

Продукт PolySpace использовался для проверки ПО сигнальной системы высокоскоростных поездов во Франции (язык Ada); для проверки ПО, управляющего впрыском топлива в дизельных двигателях (языки C/C++); для проверки ПО, управляющего срабатыванием автомобильных подушек безопасности (C/C++); для проверки ПО, обслуживающего ядерные реакторы (eao197: вот и ядрёные реакторы, как же без них ;)) – как я понял, там проверяется компонент, отвечающий за измерение потока нейтронов. (Эта информация была найдена поиском по сайту MathWorks.)

Отправить комментарий