Polyspace matlab что это

Русские Блоги

PolySpace — инструмент статической проверки для встроенного программного обеспечения

очертание
PolySpace является продуктом MathWorks, который в основном используется для анализа инструментов ошибок времени выполнения программного обеспечения. Он включает в себя два модуля, PolySpace Bug Finder и PolySpace Code Prover.

Введение продукта
• PolySpace Bug Finder
PolySpace Bug Finder — это программа для статического анализа кода, которая может обнаруживать различные типы дефектов в коде C / C ++, включая ошибки времени выполнения, проблемы с потоком данных, проблемы программирования и другие типы дефектов кода. PolySpace Bug Finder анализирует программный контроль, поток данных и поведение процессов, используя методы статического анализа. Может помочь разработчикам найти и исправить дефекты программного обеспечения на этапе разработки программного обеспечения.
Средство поиска ошибок PolySpace может генерировать статический отчет об измерениях программного кода, включая найденные дефекты, элементы несоответствия спецификации кодирования и информацию о качестве кода, такую как цикломатическая сложность. Для удобства использования PolySpace Bug Finder также обеспечивает интеграцию со средой разработки Eclipse IDE и системой сборки пользователя. С помощью комплекта сертификации IEC (IEC 61508 и ISO 26262) и комплекта квалификации Q (DO178) PolySpace обеспечивает поддержку сертификации соответствующих отраслевых стандартов. В то же время PolySpace поддерживает проверку кода на языке Ada.

• PolySpace Code Prover
PolySpace Code Prover доказывает, что код C / C ++ не содержит определенных ошибок времени выполнения, таких как переполнение, деление на ноль и выход за пределы массива. Не требует запуска кода, инструментария кода и тестовых случаев. PolySpace Code Prover использует методы статического анализа и формальной абстрактной интерпретации, подходящие для рукописного кода, автоматически сгенерированного кода и смешанного кода того и другого. В результате используются цвета, чтобы указать, нет ли в коде ошибок времени выполнения, проверенных ошибок, недоступных кодов и непроверенных кодов.
PolySpace Code Prover использует методы абстрактной интерпретации и статического анализа для доказательства, выявления и анализа ошибок времени выполнения, таких как переполнение, деление на ноль и указатель вне границ. Эта технология всесторонне проверяет все рабочие условия и автоматически доказывает, что код проверен (безопасен, ошибочен, недоступен) и недоказан. Результаты проверки PolySpace Code Prover отмечены цветами.
Возможные ошибки:
♦ Переполнение, деление на ноль и другие математические ошибки
♦ Доступ к массиву за пределами границ и разыменование недопустимых указателей
♦ всегда верно / неверно
♦ Члены класса не инициализированы (C ++)
♦ Чтение неинициализированных данных.
♦ Доступ к нулю этого указателя (C ++)
♦ Мертвый код
♦ Динамические ошибки, связанные с объектно-ориентированным программированием, наследованием и обработкой ошибок (C ++)

Интеллектуальная рекомендация

javascript html js настраиваемое раскрывающееся меню многоуровневой связи, пользовательская связь выбора

где параметр 1 — это структура меню: Объект меню Параметр 2 — это выбранный набор идентификаторов (по порядку): Значение по умолчанию может быть установлено (по порядку): Источник: От: http://www.cnbl.

Navicat import .txt файл

Файл .txt, который необходимо импортировать в базу данных, показан на рисунке: Создайте таблицу на основе импортированного txt файла: Оптимизируйте файл .txt Примечание. Добавьте имена столбцов таблиц.

kafka

Will not attempt to authenticate using SASL (unknown error) (org.apache.zookeeper.ClientCnxn) .

Безопасность в Интернете Нажмите, чтобы угнать

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

IVIEW ЗАГРУЗИТЬ реализация ручной загрузки

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

Всесторонний статический анализ с применением продуктов Polyspace

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Конечно, вы создаете тесты. Но если бы вы захотели написать тест для полного тестирования или тестирования робастности, то вам бы пришлось бы создать 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 при разработке автопилота для соответствия стандартам кодирования и получения сертификационных зачетов за верификацию исходного кода путем автоматической генерации артефактов для сертификации.

Ит на основе Polyspace Matlab для отладки программного обеспечения встроенных микропроцессоров систем управления Текст научной статьи по специальности «Компьютерные и информационные науки»

Аннотация научной статьи по компьютерным и информационным наукам, автор научной работы — Понятский Валерий Мариафович, Федорищева Вера Георгиевна, Богданова Людмила Анатольевна, Игумнова Татьяна Алексеевна

В настоящее время актуально использование автоматизированных технологий тестирования и отладки программного обеспечения для встроенных вычислительных систем. Инструменты Polyspace программного комплекса MathWorks Matlab помогают обнаружить ошибки выполнения и подтвердить отсутствие специфических ошибок в исходном коде на языке C/C++ без исполнения кода.

Текст научной работы на тему «Ит на основе Polyspace Matlab для отладки программного обеспечения встроенных микропроцессоров систем управления»

Понятский В.М.1, Федорищева В.Г. 2, Богданова Л.А.3, Игумнова Т. 4

1 АО Конструкторское бюро приборостроения им. академика А.Г. Шипунова, г. Тула, начальник бюро, Тульский государственный университет, к.т.н., доцент кафедры Проектирование автоматизированных комплексов, pwmru@rambler.ru

2 АО Конструкторское бюро приборостроения им. академика А.Г. Шипунова, г. Тула, ведущий

3 АО Конструкторское бюро приборостроения им. академика А.Г. Шипунова, г. Тула, начальник

4 АО Конструкторское бюро приборостроения им. академика А.Г. Шипунова, г. Тула, ведущий

ИТ НА ОСНОВЕ POLYSPACE MATLAB ДЛЯ ОТЛАДКИ ПРОГРАММНОГО ОБЕСПЕЧЕНИЯ ВСТРОЕННЫХ МИКРОПРОЦЕССОРОВ СИСТЕМ

Системы управления, программное обеспечение, отладка, ошибки, модель. АННОТАЦИЯ

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

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

Инструменты Polyspace программного комплекса (ПК) MathWorks Matlab помогают обнаружить ошибки выполнения и подтвердить отсутствие специфических ошибок в исходном коде на языке C/C++. Коды при этом могут быть написаны вручную, автоматически сгенерированы или их комбинацией. При помощи методов математического анализа, реализованных в продуктах верификации Polyspace, можно подтвердить отсутствие ошибок переполнения, деления на ноль, обращения к элементам вне границ массивов и других ошибок выполнения в коде. Для этого не требуется исполнения кода, применения специальных средств измерения и тестовых процедур.

Polyspace Code Prover работает совместно с Polyspace Bug Finder для поиска дефектов и проверки соответствия стандартам кодирования. Совместно эти продукты предлагают сквозное решение для статического анализа на ранних стадиях разработки, которое охватывает поиск дефектов, проверку на стандарты кодирования и доказательство наличия или отсутствия ошибок выполнения кода. Такой подход обеспечивает качество встраиваемого программного обеспечения, которое должно функционировать на высочайших уровнях надежности и безопасности.

Получить доступ к Polyspace Code Prover и Polyspace Bug Finder можно из командной строки

Matlab, графического интерфейса пользователя или при помощи плагинов для Visual Studio и Eclipse.

С использованием продуктов Parallel Computing Toolbox и Matlab Distributed Computing Server можно ускорить статический анализ кода, передавая задачи анализа кода на вычислительные кластеры.

Polyspace Bug Finder и Polyspace Code Prover совместно с инструментами Matlab IEC Certification Kit и DO Qualification Kit могут использоваться в процессе сертификации проектов по промышленным стандартам IEC 61508, ISO 26262, DO-178. Отчеты, создаваемые в процессе тестирования, документируют применение правил кодирования и отображают результаты поиска ошибок выполнения программ. Отчеты могут создаваться в форматах PDF, HTML, RTF и других форматах.

ИТ отладки программного обеспечения встроенных вычислительных систем с использованием Polyspace комплекса Matlab

Этап 1. Тестирование и отладка разработанного программного обеспечения с использованием процедуры Polyspace Bug Finder

Основные возможности Polyspace Bug Finder:

■ выявление ошибок кодирования, проблем потоков данных и других дефектов в C и C++

■ быстрый анализ больших объемов кода;

■ проверка соответствия стандартам кодирования MISRA-C:2004, MISRA-C++:2008, JSF++ и настраиваемым правилам именования;

■ расчет цикломатической сложности и других метрик кода;

■ интеграция с Eclipse;

■ трассируемость результатов верификации кода к моделям Simulink;

■ доступ к результатам анализа Polyspace Code Prover;

■ низкий уровень ложных срабатываний при выявлении программных дефектов.

Поиск ошибок кодирования и выявление их причин

Polyspace Bug Finder выявляет ошибки и нарушения правил кодирования сразу после написания, изменения или генерации кода. Ошибки кодирования или логики могут порождать сбои и некорректное поведение программы.

Polyspace Bug Finder выявляет самые разные ошибки кодирования — такие, как:

■ численные (деление на ноль, переполнение, сдвиг, некорректное использование функций из стандартной библиотеки, переполнение при целочисленной конвертации);

■ ошибки программирования (некорректное использование операторов = или ==, несоответствие объявлению);

■ ошибки при работе со статической памятью (доступ за пределы массива, null pointer);

■ ошибки при работе с динамической памятью (использование освобожденного указателя, незащищенное динамическое выделение памяти);

Рис. 1 Переполнение, обнаруженное при помощи Polyspace Bug Finder

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

Верификация соответствия стандартам кодирования (MISRA, JSF, правила именования) Polyspace Bug Finder поддерживает обнаружение нарушений стандартов кодирования MISRA-C:2004, MISRA-C++:2008, MISRA-AC-AGC, JSF++ и настраиваемых правил именования в коде. Polyspace Bug Finder используется для установления стандартов кодирования, чтобы улучшить читаемость и качество кода. Можно настроить Polyspace Bug Finder для проверки на все правила стандарта, только требуемые правила стандарта или выбрать индивидуальные правила, которые требуется проверять. Также можно задать собственную конфигурацию для использования одинаковых правил кодирования во всей команде разработчиков.

ID III: * MfSftA С ЮЛ Itw чип* at mi upmiw Ofntftr typ« ilufnoc bi npkiv cartvwwd to » dffttM mtoVng ГУР*

й1шш of The *кфг«и>л Afmdtriyng typt 'iqnttl it»ft is Фе typ* im^red dw' thm ч пм л ndH fitter typ* of the mnt iijKKln«! f i

ICS С » 0 x F Г Г: /* MI* ct: comtinc vi«p«romid "/

ufl*ign*d chur ci

uniigntd slur round(void)

uncifn*4 chur ci

с • Oxrfj return с/

Рис.2 Идентификация нарушения стандарта кодирования MISRA

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

Рис.3 Трассирование нарушений правил кодирования по стандарту MlSRA к модели SimuIink

Метрики сложности кода включают в себя:

■ уровень вложенности вызовов;

■ количество возможных путей;

■ число параметров функции;

■ количество строк кода.

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

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

Трассирование результатов анализа кода к моделям Simulink

Результаты анализа ошибок в автоматически сгенерированном коде трассируются обратно к модели Simulink. Таким образом, можно определить, какие части модели являются надежными и исправить проблемы в модели, которые приводят к ошибкам в коде.

Этап 2 Тестирование и отладка разработанного программного обеспечения с использованием процедуры Polyspace Code Prover

Основные возможности Polyspace Code Prover:

■ доказательство отсутствия определенных ошибок выполнения в C и C++ коде;

■ расцветка ошибок выполнения непосредственно в коде;

■ расчет диапазонов для переменных и значений, возвращаемых функциями;

■ идентификация переменных, нарушающих указанные диапазоны;

■ метрики качества для отслеживания соответствия целям качества программного обеспечения;

■ веб панель, представляющая метрики кода и состояние качества проекта;

■ управляемый процесс рассмотрения кода для классификации результатов и ошибок выполнения;

■ графическое представление операций чтения и записи в переменные.

Верификация ошибок выполнения

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

По результатам верификации в Polyspace Code Prover, каждая операция в C или C++ коде отмечается цветом, обозначающим статус этой операции:

Зеленый: доказано отсутствие ошибок выполнения;

Красный: доказано наличие ошибки при каждом выполнении этой операции;

Серый: доказана недостижимость операции (может указывать на функциональную проблему);

Оранжевый: недоказанная операция (ошибка может произойти при определенных условиях) (рис.4).

Polyspace — Polyspace

Polyspace это инструмент статического анализа кода для крупномасштабного анализа. абстрактная интерпретация для обнаружения или доказательства отсутствия определенных ошибок времени выполнения в исходном коде для C, C ++, и Ада языки программирования. Инструмент также проверяет исходный код на соответствие соответствующим стандартам кода. [3]

Содержание

Общее использование

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

Стандарты кодекса или руководящие принципы, такие как MISRA C попытаться решить проблему качества, переносимости и надежности кода. Продукт проверяет исходный код C и C ++ на соответствие подмножеству правил этих стандартов кодирования. [6]

Возможности

Семейство продуктов состоит из Polyspace Code Prover и Polyspace Bug Finder. Модуль Code Prover аннотирует исходный код с помощью схемы цветового кодирования, чтобы указать статус каждого элемента в коде. [7] Оно использует формальные методы статический анализ кода для проверки выполнения программы на уровне языка. [5] Инструмент проверяет каждую команду кода, принимая во внимание все возможные значения каждой переменной в каждой точке кода, обеспечивая формальную диагностику для каждой операции в коде как в нормальных, так и в ненормальных условиях использования. [8]

Модуль Bug Finder выявляет программные ошибки, выполняя статический программный анализ исходного кода. Он обнаруживает такие дефекты, как числовые вычисления, программирование, память и другие ошибки. Он также выдает программные метрики, такие как плотность комментариев исходного файла, цикломатическая сложность, количество строк, параметры, уровни вызовов и т. Д. В функции, выявленные ошибки времени выполнения в программном обеспечении. [9]