В данной публикации представлена транскрипция вебинара.
«Комплексный статический анализ с использованием продуктов Polyspace» .
Вебинар вел Михаил Песельник, инженер CITM Ээкспонента ).
Целью всех процессов разработки и проверки программного обеспечения является обеспечение отсутствия дефектов в конечном программном обеспечении.
Почему так важно убедиться в надежности программного обеспечения? Давайте подумаем о последствиях и издержках, связанных с ошибками в программном обеспечении.
Начнем с выделения ключевых областей, в которых Polyspace может помочь вам в контексте вашего процесса разработки и задач, которые вы выполняете ежедневно.
- Первый — это разработка кода (если вы пишете новый код) и проверка кода (если вы повторно используете существующий код).
- Второй — модульное тестирование и интеграционное тестирование, при котором вы проверяете надежность вашего приложения или программного обеспечения.
- И третий — это сертификация и документация, где вы документируете показатели качества кода и создаете артефакты для таких стандартов, как DO, IEC и других.
Подумайте об отозванных продуктах.
Вот недавние примеры отзывов некоторых автопроизводителей, связанных с ошибками программного обеспечения.
Отзыв не только обходится дорого, но и вредит репутации компании.
Давайте рассмотрим еще несколько примеров.
Семь с половиной миллиардов долларов.
Такова ориентировочная стоимость разработки программы запуска ракеты Ariane 5. К катастрофе привела простая ошибка переполнения, произошедшая в навигационной системе ракеты.
Нуль.
Ноль узлов — это скорость линейного крейсера USS Yorktown, когда в результате деления на ноль компьютеризированная система управления крейсера ВМС США отключила все машины в системе, в результате чего двигательная установка корабля перестала работать.
Шесть.
Именно столько произошло с участием пациентов, подвергшихся воздействию повышенной дозы радиации из-за дефектов программного обеспечения аппарата лучевой терапии Therac-25. Машина стала причиной как минимум шести передозировок радиации, при этом некоторые пациенты получили дозы в десятки тысяч рад. По меньшей мере двое умерли непосредственно от передозировки.
Что общего у всех этих систем?
- Все эти системы содержат сложное программное обеспечение, разработанное с использованием строгих отраслевых стандартов.
- Это программное обеспечение проходит интенсивную проверку, анализ и тестирование.
- И тем не менее, в этих системах по-прежнему случаются дорогостоящие ошибки.
Исследование IBM показало, что 40% всех дефектов, обнаруженных на этапе поддержки, являются ошибками времени выполнения.
Университет Патры провел исследование и обнаружил, что 33% всех медицинских устройств, проданных в США в период с 1999 по 2005 год, были отозваны из-за сбоев программного обеспечения.
Вот несколько примеров дефектов программного обеспечения, которые могут привести к сбоям.
Ошибки выполнения — это скрытые ошибки, которые трудно обнаружить.
Эти ошибки приводят к неожиданному поведению системы.
Это может быть связано с ошибками программирования или неправильным обращением с памятью.
Но это также может быть связано с проблемами многозадачности в многозадачных приложениях.
Также интересно знать, что 30% мертвого кода приводит к проблемам во время выполнения.
Хотя хорошая архитектура и тестирование помогают устранить функциональные ошибки, проблемы с надежностью все равно могут оставаться.
Отсутствие ошибок времени выполнения, как вы видели в предыдущих примерах, может иметь катастрофические последствия.
Полиспейс — это инструмент статического анализа кода, который использует формальные методы, такие как абстрактная интерпретация, для решения этих проблем надежности.
Комплексная проверка и возможность доказать отсутствие ошибок во время выполнения помогают вам обеспечить безопасность и надежность вашего программного обеспечения.
Polyspace обладает уникальной способностью доказывать отсутствие ошибок во время выполнения.
Позвольте мне продемонстрировать это на небольшом примере.
Вот пример кода, содержащий одну функцию с двумя входами.
Здесь чуть больше двадцати строк кода, и давайте посмотрим на него, чтобы найти потенциальные дефекты.
Прежде чем мы это сделаем, позвольте мне запустить проверку Polyspace для этого же файла с помощью командного сценария, использующего инструменты командной строки Polyspace. Поскольку Polyspace работает в фоновом режиме, давайте подробнее рассмотрим эту простую функцию и попытаемся выявить возможные дефекты.
Как видите, это функция с двумя входами и несколькими арифметическими операциями.
Здесь есть несколько условий, которые потенциально могут привести к неработающему коду или ошибкам потока управления.
Если мы присмотримся, то увидим, что в строке 21 есть операция деления, и в этой строке есть потенциальная ошибка.
На самом деле в этой строке кода могут возникнуть три потенциальные ошибки выполнения:
- Переменные x и y не могут быть инициализированы.
- Существует вероятность переполнения или исчезновения порядка в арифметических операциях и присваиваниях.
- Деление на ноль также может произойти, если x равно y.
Но как можно с уверенностью сделать вывод о наличии или отсутствии определенной ошибки времени выполнения? Конечно, вы создаете тесты.
Но если вы хотите написать тест для полного тестирования или проверки надежности, то вам придется создать тесты 4,61 на 10 в 18-й степени! И это для простой функции с двумя входными параметрами, где оба входных значения находятся в диапазоне int32. Если подсчитать время, необходимое для полного тестирования, то на проведение всех этих испытаний уйдет примерно 339 тысяч лет. Так что полное тестирование — это не решение проблемы.
Давайте посмотрим на другие аспекты проверки в Polyspace. Как видите, мы начинаем с исходного кода C или C++.
А Polyspace использует разные цвета для окраски исходного кода, и каждый цвет имеет определенное значение.
Зеленый цвет, как мы видели, означает безопасный и надежный код. А когда большая часть кода имеет зеленый цвет, это значительно сокращает количество необходимых действий по тестированию надежности.
Это отличается от того, как в традиционном процессе операция вообще не отмечается или о ней ничего не говорится.
На самом деле ситуация прямо противоположная, поскольку у вас есть доказательства того, что операция, отмеченная зеленым, безопасна.
Таким образом, вам не придется выполнять никакой дополнительной работы.
Красным отмечены проверенные ошибки времени выполнения — т. е.
ошибки, которые будут возникать каждый раз при запуске кода.
Серый код указывает на неработающий или недостижимый код. 
А проверки, которые не были доказаны, отмечены оранжевым цветом.
Это означает, что эти операции могут вызывать ошибки в определенных сценариях выполнения.
Сиреневый цвет указывает на нарушения правил кодирования, таких как MISRA-C/C++.
или JSF++.
Мы также видели всплывающую подсказку, которая дает вам информацию о диапазонах переменных и операциях в коде.
Это похоже на то, что у нас была бы отладочная информация, но не для этого конкретного запуска кода, а для всех возможных сценариев запуска.
Позвольте мне суммировать возможности проверки Polyspace, которые мы видели до сих пор.
Polyspace проводит статическую проверку всех возможных вариантов исполнения кода с учетом всех возможных значений входов и параметров.
Он доказывает, что определенные операции всегда безопасны при любых условиях выполнения, и для обозначения этих операций используется зеленый цвет. Polyspace использует красный цвет для выделения доказанных ошибок во время выполнения.
Оранжевый цвет обозначает непроверенный код, который может быть ненадежным при определенных сценариях выполнения.
Мертвый код отмечен серым цветом — и все это делается без проведения каких-либо тестов.
Polyspace также дает вам лучшее понимание поведения вашей программы, предоставляя вам информацию о диапазонах операций и переменных в вашем коде.
Это математически строгие методы, поскольку они основаны на формальных методах абстрактной интерпретации, а результаты проверки Polyspace не содержат ложных срабатываний.
Информация, полученная в результате проверки Polyspace, может быть использована для повышения эффективности процесса проверки, а также для сокращения объема тестирования вашего кода на надежность.
Проверка безопасности кода — это тщательный процесс, который можно запускать регулярно для проверки надежности вашего кода.
Но вы также можете достичь очевидных целей, используя быстрый анализ кода для поиска дефектов и проверки стандартов кодирования во время написания нового кода.
Помимо доказательства безопасности вашего кода, Polyspace также предлагает возможности поиска дефектов.
Начнем с правил кодирования.
Правила кодирования помогают разрабатывать высококачественное программное обеспечение и избегать небезопасных конструкций кода.
Вот пример.
Если вы используете разыменование вложенного указателя, то такой код можно скомпилировать.
Но является ли это качественным кодом или хорошей практикой? Это спорный вопрос.
Правила кодирования помогают избежать таких небезопасных конструкций, а также позволяют создавать более читаемый и удобный в сопровождении код. MISRA — широко используемый стандарт кодирования в автомобильной и авиационной промышленности.
JSF также является одним из распространенных стандартов кодирования.
Polyspace проверяет ваш код на соответствие MISRA, и вы можете настроить его и выбрать правила, соответствующие вашему процессу разработки.
MISRA AC AGC описывает использование MISRA в контексте автоматически генерируемого кода и также поддерживается Polyspace. Кроме того, вы можете реализовать свои собственные правила кодирования, такие как правила именования переменных и другие.
Поиск дефектов кода с помощью Polyspace позволяет выявлять дефекты кода, такие как ошибки программирования, ошибки потока данных, ошибки памяти и другие ошибки времени выполнения, когда вы разрабатываете новый код в своей среде разработки.
Инструмент помогает найти ошибки на ранних этапах разработки, когда исправить эти ошибки гораздо проще и дешевле.
При использовании автоматической генерации кода Polyspace позволяет отслеживать результаты анализа кода непосредственно до исходных моделей, что позволяет находить и исправлять ошибки на этапе проектирования.
Вот некоторые типы дефектов, обнаруженных с помощью Polyspace.
- Числовые ошибки – такие как деление на ноль, переполнение и т. д.
- Либо ошибки при работе со статической памятью — например, доступ за границы массива, нулевой указатель.
- Проблемы с динамической памятью, например утечки памяти.
- А также ошибки программирования, потоков данных и так далее.
Есть несколько причин, почему это следует сделать.
Ваши модели могут содержать S-функции, то есть рукописный код. Сгенерированный вами код можно интегрировать с ручным кодом или системным программным обеспечением, например драйверами или операционной системой.
Обычно это так, и эти интерфейсы могут вызвать последующие ошибки во время выполнения.
Проверки только на уровне модели недостаточно, и требования сертификации определенно требуют от вас проверки на уровне кода, что может потребовать от вас использования такого инструмента, как Polyspace. 
Ключевой особенностью инструментов модельно-ориентированного проектирования Polyspace является возможность отслеживания результатов анализа от кода до модели, на основе которой код был сгенерирован.
Вы также можете проверить сгенерированный код на соответствие стандартам кодирования, что является требованием таких стандартов, как DO-178 и IEC. Поэтому я хотел бы обратить на это внимание тех, кто использует модельно-ориентированное проектирование.
Наконец, давайте посмотрим, как Polyspace помогает с точки зрения поддержки документации и сертификации.
Это веб-панель для отслеживания статуса проекта и различных показателей качества проекта.
Как видите, каждая строка показывает отдельный прогон проверки, а графики показывают, как показатели качества нашего проекта улучшаются с течением времени.
Уменьшено количество ошибок во время выполнения, уменьшено количество оранжевых проверок и нарушений кодирования.
Вы также можете выполнить анализ воздействия, который покажет, как изменения, внесенные вами в код, влияют на ошибки времени выполнения или нарушения стандартов кодирования.
Кроме того, вы можете создавать отчеты, включающие проверки ошибок во время выполнения, проверки стандартов кодирования и другие, для ваших отдельных файлов.
Отчеты формируются автоматически с помощью опции «Выполнить» – «Выполнить отчет».
Я могу выбрать один из встроенных шаблонов отчетов или создать свой собственный шаблон, а также выбрать формат создаваемого отчета.
Все эти отчеты помогут вам получить сертификационные баллы по стандартам обеспечения надежности, таким как DO, IEC и другим.
Polyspace помогает вам разрабатывать системы в соответствии с DO-178, а MathWorks предоставляет комплект квалификации DO, набор, содержащий документацию, тестовые векторы и процедуры тестирования, которые помогут вам квалифицировать продукты проверки Polyspace для использования в проектах, разработанных для DO-178B/C, DO. -254 и связанные расширения.
Этот комплект также содержит план квалификации прибора, требования к характеристикам прибора и другие материалы, необходимые для квалификации приборов для поверки.
Используя этот комплект, вы сможете упростить процесс проверки вашей встраиваемой системы.
Аналогичным образом мы предлагаем комплект сертификации IEC, содержащий сертификаты квалификации приборов, сертификаты 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 в своей автопилотной разработке, чтобы соответствовать стандартам кодирования и получить сертификационные баллы для проверки исходного кода путем автоматического создания артефактов для сертификации.
Автор материала — Михаил Песельник, инженер CITM Ээкспонента .
Ссылка на этот вебинар https://exponenta.ru/events/vsestoronniy-staticheskiy-analiz-s-primeneniem-produktov-polyspace Теги: #программирование #C++ #Тестирование ИТ-систем #Идеальный код #iso 26262 #статический анализ #формальная проверка #надежность по #polyspace #polyspace #абстрактная интерпретация #КТ-178С
-
О Смете
19 Dec, 24 -
«Квант» Здесь И Сейчас (Часть 1)
19 Dec, 24 -
В Стране Закончились Новости
19 Dec, 24 -
Покупка На Amazon.com, Что Делать?
19 Dec, 24
