В данной публикации представлена транскрипция вебинара «Всесторонний статический анализ с применением продуктов Polyspace». Вебинар проводил Михаил Песельник, инженер ЦИТМ Экспонента).

Цель всех процессов разработки и верификации ПО заключается в том, чтобы убедиться в том, что в финальном программном обеспечении больше нет дефектов. Почему так важно убедиться, что ПО является надежным? Давайте подумаем о последствиях и затратах, связанных с ошибками в программном обеспечении.

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

• Первое – это разработка кода (если вы пишете новый код) и рассмотрение кода (если вы повторно используете существующий код).
• Второе – это модульное тестирование и интеграционное тестирование, когда вы осуществляете верификацию робастности вашего приложения или программного обеспечения.
• И третье – это сертификация и документация, когда вы документируете метрики качества кода и генерируете артефакты для таких стандартов, как DO, IEC и других.

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

Давайте посмотрим еще на несколько примеров.

Семь с половиной миллиардов долларов. Это оцениваемая стоимость разработки программы запуска ракеты Ariane 5. Простая ошибка переполнения, которая произошла в системе навигации ракеты, привела к катастрофе.

Ноль. Ноль узлов – это скорость боевого крейсера USS Yorktown, когда в результате деления на ноль в компьютеризированной управляющей системе крейсера Военно-морского флота США произошло отключение всех машин в системе, в результате чего прекратила работу двигательная установка корабля.

Шесть. Таким было число инцидентов, связанных с облучением пациентов повышенной дозой радиации из-за программных дефектов в аппарате лучевой терапии Therac-25. Этот аппарат был причиной как минимум шести передозировок радиации, некоторые пациенты получили дозы в десятки тысяч рад. Как минимум двое умерли непосредственно от передозировок.

Что общего у всех этих систем?

• Все эти системы содержат сложное программное обеспечение, при разработке которого применяются жесткие индустриальные стандарты.
• Это программное обеспечение подвергается интенсивному рассмотрению, анализу и тестированию.
• И тем не менее, все равно в этих системах случаются дорогостоящие ошибки.

Вот результаты нескольких недавних исследований, подчеркивающих проблему. Исследование IBM показало, что 40% всех дефектов, обнаруженных во время стадии поддержки – это ошибки времени выполнения.

Университет Патрас провел исследование и обнаружил, что 33% всех медицинских устройств, проданных в США между 1999 и 2005 годами, были отозваны из-за программных сбоев.

Вот некоторые примеры дефектов в программном обеспечении, которые могут привести к сбоям.

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

Это может быть связано с ошибками программирования или неправильной работой с памятью. Но это также может быть связано проблемами с многозадачностью, когда речь идет о многозадачных приложениях. Также интересно знать, что 30% мертвого кода приводят к проблемам во время выполнения.

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

Polyspace – это инструмент статического анализа кода, использующий формальные методы, такие, как абстрактная интерпретация, для того, чтобы адресовать эти проблемы, связанные с робастностью. Всесторонняя верификация и способность доказывать отсутствие ошибок времени выполнения помогают вам обеспечить безопасность и надежность программного обеспечения.

Polyspace обладает уникальной возможностью доказывать отсутствие ошибок времени выполнения. Позвольте вам это продемонстрировать на небольшом примере.

Вот пример кода, содержащего одну функцию с двумя входами. Здесь чуть больше двадцати строк кода, и давайте проведем рассмотрение кода с целью обнаружения потенциальных дефектов. До того, как мы это сделаем, позвольте мне запустить верификацию Polyspace на этом же самом файле, используя командный скрипт, который использует инструменты командной строки Polyspace.

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

Если мы посмотрим внимательней, то увидим, что на строке 21 происходит операция деления, и потенциально на этой строке может произойти ошибка.

На самом деле, в этой строке кода могут произойти три потенциальных ошибки времени выполнения:

1. Переменные х и у могут быть не инициализированы.
2. Есть возможность переполнения или исчезновения порядка на арифметических операциях и в присваивании.
3. Также может произойти деление на ноль, если х равен у.

В традиционном процессе рассмотрения кода, вы, возможно, сможете отметить эти операции как потенциальные источники ошибок. Но как вы можете с уверенностью заключить, присутствует или отсутствует определенная ошибка времени выполнения?

Конечно, вы создаете тесты. Но если бы вы захотели написать тест для полного тестирования или тестирования робастности, то вам бы пришлось бы создать 4.61 на 10 в 18 степени тестов! И это – для простой функции с двумя входами, где оба входа находятся в диапазоне инт32. Если вы посчитаете время, которое потребуется для полного тестирования, то прогон всех этих тестов займет примерно 339 тысяч лет.

Таким образом, полное тестирования не является решением проблемы.

Давайте посмотрим на другие различные аспекты верификации в Polyspace. Как вы видите, мы начинаем с исходного С или С++ кода.

И Polyspace использует разные цвета для раскрашивания исходного кода, и каждый цвет имеет определенное значение.

Зеленый цвет, как мы видели, означает безопасный и надежный код. И когда большая часть кода отмечена зеленым, это существенно сокращает число мероприятий по тестированию робастности, которые вам надо провести. Это отличается от того, как в традиционном процессе операция вообще никак не отмечается или о ней ничего не говорится. На самом деле, это ровно противоположная ситуация, поскольку у вас есть доказательство, подтверждающее то, что операция, отмеченная зеленым, является безопасной. Таким образом, вам не нужно делать дополнительную работу.

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

Серым цветом отмечается мертвый или недостижимый код.

А оранжевым цветом отмечаются проверки, которые не доказаны. Это означает, что эти операции могут привести к ошибкам при определенных сценариях выполнения.

Сиреневым цветом обозначаются нарушения правил кодирования – таких, как MISRA-C/C++
или JSF++.

Мы также видели всплывающую подсказку, которая дает вам информацию о диапазонах переменных и операций во всем коде. Это аналогично тому, что у нас была бы отладочная информация, но только не для этого конкретного запуска кода, а для всех возможных сценариев запуска.

Позвольте мне подвести итоги возможностей Polyspace по верификации, которые мы увидели до этого момента. Polyspace осуществляет статическую верификацию всех возможных вариантов выполнения кода, с учетом всех возможных значений входов и параметров. Он доказывает, что определенные операции всегда безопасны при любых условиях выполнения и использует зеленый цвет для обозначения этих операций.

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

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

Серым цветом отмечается мертвый код – и все это делается без запуска каких-либо тестов.

Polyspace также дает вам лучшее представление о поведении вашей программы, представляя вам информацию о диапазонах операций и переменных в коде. Это математически тщательные методы, поскольку они основаны на формальных методах абстрактной интерпретации и результаты верификации Polyspace не содержат ложных срабатываний. Информация, полученная в результате верификации Polyspace, может быть использована для того, чтобы сделать процесс рассмотрения более эффективным, а также уменьшить объем тестирования на робастность вашего кода.

Доказательство безопасности кода – это тщательный процесс, который может запускаться регулярно для верификации надежности вашего кода. Но вы также можете достичь очевидных целей, применяя быстрый анализ кода для поиска дефектов и проверки на стандарты кодирования прямо во время написания нового кода. В дополнение к доказательству того, что ваш код является безопасным, Polyspace также предлагает возможности для поиска дефектов.

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

MISRA – это широко распространенный стандарт кодирования в автомобильной и авиационной промышленностях.

JSF также является одним из распространенных стандартов кодирования.

Polyspace проверяет код на соответствие MISRA Вы также можете настроить его и выбрать правила, которые подходят для вашего процесса разработки. MISRA AC AGC – описывает применение MISRA в контексте автоматически сгенерированного кода и также поддерживается Polyspace. Кроме того, вы можете реализовать собственные правила кодирования – например, правила именования переменных и другие.

Поиск дефектов в коде при помощи Polyspace позволяет определить дефекты в коде, такие, как ошибки программирования, ошибки потоков данных, ошибки при работе с памятью и другие ошибки времени выполнения по мере того, как вы разрабатываете новый код в вашей среде разработки. Инструмент помогает вам искать ошибки на ранних стадиях разработки, когда гораздо проще и дешевле эти ошибки исправить. При использовании автоматической генерации кода, Polyspace позволяет трассировать результаты анализа кода напрямую к оригинальным моделям, позволяя вам искать и исправлять ошибки на стадии проектирования.

Вот некоторые типы дефектов, выявляемых при помощи Polyspace.

• Численные ошибки – такие, как деление на ноль, переполнение и т.д.
• Или ошибки при работе со статической памятью – например, доступ за границы массива, null pointer.
• Проблемы динамической памяти – такие, как утечки памяти.
• А также ошибки программирования, потоков данных и так далее.

Я хотел бы рассказать о том, как Polyspace накладывается на процесс модельно-ориентированного проектирования, который является широко применяемым методом разработки на основании моделей и автоматической генерации кода при помощи таких инструментов как Simulink Embedded Coder, Target Link или IBM Rhapsody. Вы можете использовать Polyspace и интегрировать его в ваш процесс разработки.

Есть несколько причин, почему это надо делать. Ваши модели могут содержать S-функции, т.е. код, написанный вручную. Ваш сгенерированный код может интегрироваться с ручным кодом или системным ПО – таким, как драйвера или операционная система. Обычно это так и происходит, и эти интерфейсы могут вызывать последующие ошибки времени выполнения.

Верификации только на уровне модели недостаточно, и требования по сертификации определенно требуют от вас верификации на уровне кода, что может потребовать от вас использования такого инструмента, как Polyspace.

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

Вы также можете проверять сгенерированный код на соответствие стандартам кодирования, что является требованием таких стандартов, как DO-178 и IEC. Таким образом, я бы хотел указать на это тем, кто применяет модельно-ориентированное проектирование.

Наконец, давайте посмотрим, как Polyspace помогает с точки зрения поддержки документации и сертификации.

Это веб панель для отслеживания состояния проекта и различных метрик качества проекта. Как вы видите, каждая строка показывает отдельный запуск верификации и графики показывает, как показатели качества нашего проекта улучшается с течением времени. Число ошибок времени выполнения сокращается, число оранжевых проверок и нарушений правил кодирования сокращается. Вы также можете осуществлять анализ влияния, показывающий, как изменения, которые вы вносите в код, повлияли на ошибки времени выполнения или нарушения стандартов кодирования. В дополнение, вы можете генерировать такие отчеты, включающие проверки на ошибки времени выполнения, проверки на стандарты кодирования и другие для ваших индивидуальных файлов. Отчеты генерируются автоматически, с использованием опции Run – Run Report. Я могу выбрать один из встроенных шаблонов для отчета или создать свой собственный шаблон, а также выбрать формат генерируемого отчета.

Все эти отчеты помогают вам получить сертификационные зачеты по стандартам разработки систем повышенной надежности, таким, как DO, IEC и другие.

Polyspace помогает вам при разработке систем по DO-178, и MathWorks предоставляет DO Qualification Kit – набор, содержащий документацию, тестовые вектора и процедуры тестирования, которые помогают вам квалифицировать продукты верификации Polyspace для использования в проектах, разрабатывающихся в соответствии с DO-178B/C, DO-254 и соответствующих расширений.

Этот набор также содержит план квалификации инструмента, эксплуатационные требования к инструменту и другие материалы, требующиеся для квалификации инструментов верификации. Используя этот набор, вы можете упростить процесс верификации вашей встраиваемой системы.

Похожим образом, мы предлагаем IEC Certification Kit, содержащий артефакты для квалификации инструментов, сертификаты TUV SUD и другие материалы.

IEC 61508 является базовым стандартом для нескольких других производных стандартов, таких, как ISO 26262 для автомобильного транспорта, EN 50128 для железных дорог и IEC 62304 для медицинских устройств.

Например, если посмотреть в стандарт IEC 62304 для медицинских устройств, то он ссылается на IEC 61508 в части, касающейся мероприятий разработки и верификации ПО.

Подводя итоги, семейство продуктов Polyspace представлено Polyspace Code Prover, который предоставляет возможность доказывать безопасность и надежность кода.

Polyspace Bug Finder дает вам возможность поиска программных дефектов и проверки кода на стандарты кодирования и может использоваться ежедневно программистами в качестве инструмента верификации.

Таким образом, возвращаясь к тем областям, где может помочь Polyspace и которые мы описали вначале. Он позволяет вам обеспечить отсутствие дефектов в коде и проводить эффективные, повторяемые рассмотрения кода. Вы можете существенно сократить объем тестов на робастность, которые вы проводите. Возможности по автоматическому созданию документации и отчетов позволяют документировать метрики кода и получать зачеты по сертификации.

В конце я расскажу вам несколько историй успеха заказчиков, которые используют Polyspace.

Elektrobit – это автомобильный поставщик и они используют Polyspace для поиска ошибок времени выполнения в компонентах AUTOSAR. Преимущества, которые они получили с использованием Polyspace, заключаются в отсутствии ошибок времени выполнения, сокращение времени верификации и достижение сертификации в соответствии с ISO26262.

Nissan использует Polyspace для проверки программных компонентов, которые они получают от поставщиков. Это позволило улучшить надежность поставляемой продукции. Nissan также требует от поставщиков использование Polyspace для того, чтобы убедиться, что код является надежным.

Alenia достигли сертификации по DO-178 и они использовали Polyspace при разработке автопилота для соответствия стандартам кодирования и получения сертификационных зачетов за верификацию исходного кода путем автоматической генерации артефактов для сертификации.

Автор материала — Михаил Песельник, инженер ЦИТМ Экспонента.

Ссылка на данный вебинар https://exponenta.ru/events/vsestoronniy-staticheskiy-analiz-s-primeneniem-produktov-polyspace