Попробовал поискать информацию о том, где использовались, используются или будут использоваться средства для анализа и верификации программ (по следам заметки у меня в блоге и в блоге “Алёна 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.)
4 комментария:
А Вы, Евгений, пользуетесь (пользовались) какими-нибудь инструментами для анализа и верификации программ? Например, для SObjectizer?
Нет, не пользовался.
В университете у нас был спецкурс по методам вычислений, в рамках которого несколько лекций было посвящено верификации программ. Единственное, что запомнил оттуда, так это рассказы преподавателя о том, какое это муторное, тяжелое и неблагодарное дело -- доказательство корректности программ. И его пример -- коллектив из трех человек написал программу на три или четыре страницы, после чего написали 50-ти страничное доказательство ее корректности. После чего в программе нашли ошибку.
Потом был довольно длительный период времени, когда всякие передовые инструменты до нас просто не доходили. А сейчас уже просто на это нет времени -- даже думать некогда, трясти надо.
Я пытался посмотреть на внутренности проекта Tokeneer. У меня создалось впечатление, что разработка на SPARK-е будет втрое дороже и медленнее обычной разработки. В наших условиях это неприменимо. Но мы и не пишем софт для ядерных реакторов.
Так что по историческим причинам не пользуюсь. Наверное, стоит попробовать. Но для этого нужно разорвать сложившийся "порочный" круг.
Так что по историческим причинам не пользуюсь. Наверное, стоит попробовать.
Если проект с открытым кодом, то можно попытать счастье здесь:
http://scan.coverity.com/
Они уже много чего проверили - и ядро Linux, и MySQL, и другие гораздо более мелкие проекты. Зато если проект получится качественным по результатам проверки, то это несомненный плюс в копилку проекта. И этим, безусловно, можно будет гордиться, как, например, разработчики Tcl/Tk (http://www.tcl.tk/, http://www.coverity.com/html/press_story54_01_08_08.html).
>Если проект с открытым кодом, то можно попытать счастье здесь:
http://scan.coverity.com/
Спасибо за наводку, нужно будет покурить эту тему.
Отправить комментарий