polyspace code prover что это
Polyspace Code Prover
Prove the absence of run-time errors in software
Polyspace Code Prover™ is a sound static analysis tool that proves the absence of overflow, divide-by-zero, out-of-bounds array access, and other run-time errors in C and C++ source code. It produces results without requiring program execution, code instrumentation, or test cases. Polyspace Code Prover uses semantic analysis and abstract interpretation based on formal methods to verify software interprocedural, control, and data flow behavior. You can use it to verify handwritten code, generated code, or a combination of the two. Each code statement is color-coded to indicate whether it is free of run-time errors, proven to fail, unreachable, or unproven.
Polyspace Code Prover displays range information for variables and function return values, and can prove which variables exceed specified range limits. Code verification results can be used to track quality metrics and check conformance with your software quality objectives. Polyspace Code Prover can be used with the Eclipse™ IDE to verify code on your desktop
Support for industry standards is available through IEC Certification Kit (for ISO 26262 and IEC 61508) and DO Qualification Kit (for DO-178 and DO-254).
Get Started:
Verify Code Using Formal Mathematics
Achieve high levels of quality and safety with no false negatives.
Prove the Absence of Critical Run-Time Errors
Identify C/C++ and Ada code operations that will never experience a run-time error, regardless of the run-time conditions.
Всесторонний статический анализ с применением продуктов Polyspace
В данной публикации представлена транскрипция вебинара «Всесторонний статический анализ с применением продуктов Polyspace». Вебинар проводил Михаил Песельник, инженер ЦИТМ Экспонента).
Цель всех процессов разработки и верификации ПО заключается в том, чтобы убедиться в том, что в финальном программном обеспечении больше нет дефектов. Почему так важно убедиться, что ПО является надежным? Давайте подумаем о последствиях и затратах, связанных с ошибками в программном обеспечении.
Начнем с того, что обозначем ключевые моменты, в которых вам может помочь Polyspace в контексте вашего процесса разработки и задач, которые вы выполняете ежедневно.
Вспомните об отозванных продуктах. Вот недавние примеры отзывов у некоторых автомобильных производителей, связанных с программными ошибками. Отзывы не только являются дорогостоящими, но и также вредят репутации компании.
Давайте посмотрим еще на несколько примеров.
Семь с половиной миллиардов долларов. Это оцениваемая стоимость разработки программы запуска ракеты 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.
Я хотел бы рассказать о том, как 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 при разработке автопилота для соответствия стандартам кодирования и получения сертификационных зачетов за верификацию исходного кода путем автоматической генерации артефактов для сертификации.
Автор материала — Михаил Песельник, инженер ЦИТМ Экспонента.
Квалификация инструментов для разработки встраиваемого ПО
Отраслевые стандарты, такие как КТ-178 или ИСО 26262, описывают процессы создания ПО повышенной надежности. Если следовать этим описаниям, то создание такого ПО превратится в бюрократический ад, который будет длиться вечно. Но существует программное обеспечение, которое позволяет автоматизировать значительную часть этих процессов. Такое ПО называется инструментом. И если вы применяете инструмент, то он должен быть надежным (ИСО 26262 даже вводит термин «уверенность в инструменте»). Для подтверждения надежности инструмента проводится его квалификация.
В отраслевых стандартах есть понятие уровня безопасности. В разных стандартах они называются по-разному: Уровень ПО в КТ-178, Уровни Полноты Безопасности автомобиля в ИСО 26262. А для средств разработки применяются уровни квалификации инструментов (КТ-178) или уровни классификации инструментов (ИСО 26262). Эти уровни назначаются по критичности инструментов – чем больше влияния оказывает инструмент на разработку, тем более высокий уровень квалификации будет ему назначен. При этом одним из главных критериев по определению влияния инструмента является мера его влияния на результирующее ПО.
В качестве примера можно рассмотреть генератор исходного кода и статический анализатор кода. Сгенерированный код попадает в прошивку устройства, которое будет установлено на борт самолета или автомобиля. Таким образом, генератор кода оказывает непосредственное влияние на результирующее ПО. Так как генератор кода – сложная штука, и может генерировать код с ошибками, то к качеству этого генератора кода предъявляются строгие требования и уровень его квалификации будет максимальным. Другое дело – статический анализатор, результат работы которого не попадает в бортовое ПО и степень его влияния минимальна. Поэтому для статического анализатора уровень квалификации будет ниже, чем для генератора кода.
А еще уровень квалификации напрямую влияет на трудозатраты: так, для авиации, для квалификации инструмента по наивысшему уровню КТ-178С, требуется выполнение 76 контрольных мероприятий, а по низшему – только 14.
Еще один важный момент – квалификация инструментов проводится не разработчиком инструмента, а непосредственно разработчиком ПО, причем квалификация должна проводиться для каждого проекта!
Квалификация – заметки по практике
Как было сказано в теоретической части, квалификация инструментов – это затратный процесс, однако он упрощается несколькими способами:
Хотелось бы остановиться на втором пункте. Опять будем рассматривать генератор кода. Сгенерированный с его помощью код все равно должен тестироваться, будет собираться покрытие кода, проводится его анализ, т. е. верифицироваться.
Отраслевые стандарты говорят нам о том, что если мы будем квалифицировать инструменты, которые отвечают за верификацию кода, то квалификация самого генератора кода будет не нужна. Таким образом, сами стандарты содержат указания, следуя которым вы можете значительно сократить затраты на квалификацию.
Для квалификации инструментов верификации стандарты предписывают демонстрацию их поведения в нормальных условиях. На практике это выглядит следующим образом:
Инструменты MathWorks и их квалификация
Такие инструменты, как Simulink, DSP Toolbox, Control System Toolbox – это стандарт индустрии для разработки систем управления, цифровой обработки сигналов. Неудивительно, что их применяют в авиации, автомобилестроении и прочих отраслях. Из разработанных моделей генерируется C/C++ код, который ездит и летает. Естественно, что перед разработчиками встает вопрос квалификации инструментов. И квалификация инструментов MathWorks для КТ-178С осуществляется для инструментов верификации моделей и кода:
Вместо выводов
В данной статье был дан обобщенный обзор процесса квалификации инструментов в соответствии с отраслевыми стандартами. В ходе написания данной статьи я руководствовался следующими источниками:
polyspace-code-prover.exe: что это? и как его убрать
В вашей системе запущено много процессов, которые потребляют ресурсы процессора и памяти. Некоторые из этих процессов, кажется, являются вредоносными файлами, атакующими ваш компьютер.
Чтобы исправить критические ошибки polyspace-code-prover.exe,скачайте программу Asmwsoft PC Optimizer и установите ее на своем компьютере
Asmwsoft PC Optimizer — это пакет утилит для Microsoft Windows, призванный содействовать управлению, обслуживанию, оптимизации, настройке компьютерной системы и устранению в ней неполадок.
1- Очистите мусорные файлы, чтобы исправить polyspace-code-prover.exe, которое перестало работать из-за ошибки.
2- Очистите реестр, чтобы исправить polyspace-code-prover.exe, которое перестало работать из-за ошибки.
Как удалить заблокированный файл polyspace-code-prover.exe.
3- Настройка Windows для исправления критических ошибок polyspace-code-prover.exe:
Всего голосов ( 181 ), 115 говорят, что не будут удалять, а 66 говорят, что удалят его с компьютера.
Как вы поступите с файлом polyspace-code-prover.exe?
Некоторые сообщения об ошибках, которые вы можете получить в связи с polyspace-code-prover.exe файлом
(polyspace-code-prover.exe) столкнулся с проблемой и должен быть закрыт. Просим прощения за неудобство.
(polyspace-code-prover.exe) перестал работать.
polyspace-code-prover.exe. Эта программа не отвечает.
(polyspace-code-prover.exe) — Ошибка приложения: the instruction at 0xXXXXXX referenced memory error, the memory could not be read. Нажмитие OK, чтобы завершить программу.
(polyspace-code-prover.exe) не является ошибкой действительного windows-приложения.
(polyspace-code-prover.exe) отсутствует или не обнаружен.
POLYSPACE-CODE-PROVER.EXE
Проверьте процессы, запущенные на вашем ПК, используя базу данных онлайн-безопасности. Можно использовать любой тип сканирования для проверки вашего ПК на вирусы, трояны, шпионские и другие вредоносные программы.
процессов:
Cookies help us deliver our services. By using our services, you agree to our use of cookies.