WWW.NEW.PDFM.RU
БЕСПЛАТНАЯ  ИНТЕРНЕТ  БИБЛИОТЕКА - Собрание документов
 


«Polyspace Code Prover™ используется для проверки на отсутствие ошибок при выполнении в исходном коде C и C++ — таких, как переполнение, деление на ноль, доступ за пределы ...»

Polyspace Code Prover

Доказательство отсутствия ошибок при выполнении кода в программном обеспечении

Polyspace Code Prover™ используется для проверки на отсутствие ошибок при выполнении в

исходном коде C и C++ — таких, как переполнение, деление на ноль, доступ за пределы массива

и других. Результаты создаются без запуска программы, инструментального оснащения кода

или тестовых векторов. Polyspace Code Prover использует статический анализ и абстрактную

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

Polyspace Code Prover также отображает информацию о диапазонах переменных и значениях, возвращаемых функциями, и может показать условия, при которых переменные нарушают указанные диапазоны. Результаты могут быть опубликованы в веб-панели для отслеживания метрик качества и обеспечения соответствия целям качества программного обеспечения .

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

Поддержка промышленных стандартов доступна с использованием IEC Certification Kit (для IEC 61508 и ISO 26262) и DO Qualification Kit (для DO-178). Также доступна поддержка языка Ada .

Основные возможности • Доказательство отсутствия определенных ошибок при выполнении кода C и C++ • Выделение ошибок различными цветами при выполнении непосредственно в коде • Расчет диапазонов для переменных и значений, возвращаемых функциями • Идентификация переменных, нарушающих указанные диапазоны • Метрики качества для отслеживания соответствия целям качества программного обеспечения • Веб-панель, представляющая метрики кода и состояние качества проекта • Управляемый процесс рассмотрения кода для классификации результатов и ошибок при выполнении • Графическое представление операций чтения и записи в переменные Ошибки при выполнении кода, отображаемые в Polyspace Code Prover .

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

Использование Polyspace Code Prover позволяет:

• доказывать отсутствие ошибок в коде — проводить верификацию того, что при выполнении кода не возникают ошибки;

• получать результаты без ложных срабатываний — все потенциальные ошибки при выполнении тщательно идентифицируются;

• повышать уверенность в качестве кода — измерять количество проверенного кода относительно непроверенного .





Получить доступ к Polyspace Code Prover можно из командной строки, графического интерфейса пользователя или при помощи плагинов для Visual Studio® и Eclipse™.

Поддерживается критически важные мероприятия процесса разработки программного обеспечения, включая:

• выявление ошибок при выполнении;

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

• определение диапазонов переменных и установление того, что эти пределы не нарушаются;

• обеспечение выполнения соответствующих целей качества программного обеспечения;

• трассирование ошибок при выполнении к блокам Simulink или моделям IBM® Rational® Rhapsody®;

• создание артефактов для сертификации .

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

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

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

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

Зеленый: доказано отсутствие ошибок при выполнении Красный: доказано наличие ошибки при каждом выполнении этой операции Серый: доказана недостижимость операции (может указывать на функциональную проблему) Оранжевый: недоказанная операция (ошибка может произойти при определенных условиях)

Ошибки при выполнении, идентифицированные Polyspace Code Prover

Определяются следующие типы ошибок:

• переполнение, исчезновение порядка, деление на ноль и другие арифметические ошибки;

• доступ за пределы массива и некорректное разыменование указателя;

• выражение, всегда возвращающее истину или ложь;

• неинициализированные члены класса (C++);

• чтение неинициализированных данных;

• доступ по нулевому указателю (C++);

• мертвый код;

• динамические ошибки, относящиеся к объектно-ориентированному программированию, наследованию и обработке исключений (C++) .

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

В приведенном ниже примере Polyspace Code Prover определил, что в операции деления левый операнд находится в диапазоне от –1701 до 3276, а правый операнд равен 9. Результат деления находится в диапазоне от –189 до 364 .

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

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

Отображение метрик качества программного обеспечения в веб-браузере .

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

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

Polyspace Code Prover также поддерживает трассирование результатов к блокам dSPACE® TargetLink® и моделям IBM Rational Rhapsody .

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

Автоматизация верификации кода Polyspace Code Prover может использоваться как часть целостного процесса разработки и встраиваться в ваш процесс построения кода. Имеется возможность автоматизировать выполнение задач верификации и настроить почтовые уведомления. Можно назначить Polyspace Code Prover для передачи верификации на компьютерный кластер (с использованием MATLAB Distributed Computing Server), и получать почтовые уведомления о готовности результатов .

Результаты содержат отличия по сравнению с предыдущей версией кода, которые сервер определяет автоматически .

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

Создание артефактов для сертификации Polyspace Bug Finder и Polyspace Code Prover совместно с IEC Certification Kit (для IEC 61508 и ISO 26262) и DO Qualification Kit (для DO-178) могут использоваться в процессе сертификации проектов по этим промышленным стандартам .

Отчеты и артефакты показывают финальное качество кода, демонстрируют рассмотренные секции кода, рассчитанные метрики кода, документируют применение правил кодирования и отображают результаты поиска ошибок при выполнении. Отчеты могут создаваться в PDF, HTML, RTF и других форматах.



Похожие работы:

«ОАО "ИнфоТеКС Интернет Траст" Инструкция по настройке автоматизированного рабочего места для работы в информационной системе Росаккредитации Листов 12 ОГЛАВЛЕНИЕ I. ВВЕДЕНИЕ II. СОСТАВ ПРОГРАММНОГО ОБЕСПЕЧЕНИЯ АРМ III. ПОЛУЧЕНИЕ И УСТАНОВКА VIPNET CSP IV. УСТАНОВКА ДРАЙВЕРОВ ДЛЯ КЛЮЧЕВОГО НОСИТЕЛЯ ETOKEN V. УСТАНОВКА VIPNET CSP ДЛЯ РАБОТЫ С ЭЛЕК...»

«передовое капиталистическое производство на основе этого месторождения. Этот богатейший рудник эксплуатировало Белорецкое заводоуправление. Гора Магнитная является примером контактово-метасоматических месторождений. Среди гранатовых,...»

«Скачать руководство для дальномера cp 25-03-2016 1 Отдавливание пропалывает худеньких пересборки срывающимся прополаскиванием . Феноменальное моделирование помогает открепиться по — над свинцом. Преизрядность учащенно не аннигилирует. Недальновидно отворачивающееся осваивание — немного...»

«ISSN 2075-1486. Філологічні науки. 2016. № 23 УДК: 821.161.1-82 Ахматова ВЛАДИМИР КАЗАРИН МАРИНА НОВИКОВА (Симферополь) ". ГРОЗНАЯ АНАФЕМА ГУДИТ" (ЗАГАДКИ ОДНОГО АХМАТОВСКОГО ВОСЬМИСТИШИЯ) Ключові слова: А. А. Ахматова, М. М. Зощенко, М....»

«52. ICHNEUMONIDAE: 24. COLLYRIINAE 677 Длина ножен яйцк. 0.4–0.65 длины задн. голеней. Яйцк. слабо изогнут книзу, сравнительно широкий в основании и постепенно сужен к тонкой вершине, почти по всему нижнему краю с рядом редких зазубрин; вершина яйцк. без субапи...»

«В Савеловский районный суд г. Москвы ИСТЕЦ: Слепцов Владимир Владимирович, проживающий по адресу 644089 г. Омск, ************************* Представитель: Фролов Михаил Александрович, 125284 г. Москва ОПС 284, а/я 17 тел.8-915-4******** ОТВЕТЧИК: Закрытое акционерное общество "Экспресс газета" 127287 г....»

«ВЫ МОЖЕТЕ ДЕЛАТЬ ТО, ЧТОВАМ НУЖНО NexION 300 ИСП-МС Три режима работы. Два способа устранения наложений. Один революционный прибор. БЕЗ КОМПРОМИССОВ. НЕТ РАВНЫХ. РЕВОЛЮЦИЯ ДОБРО Разработанный для достижения беспрецедентного уровня стабильности, гибкости, характеристик и отмеченный наградой NexION ® 300 представляет самое значим...»

«Содержание I Аналитическая часть... 4 1 Общие сведения об образовательной организации.. 4 1.1 Федеральное государственное бюджетное образовательное учреждение высшего образования "Мурманский арктический государственный университет". 4 1.2 Филиал федерального государственного бюд...»







 
2018 www.new.pdfm.ru - «Бесплатная электронная библиотека - собрание документов»

Материалы этого сайта размещены для ознакомления, все права принадлежат их авторам.
Если Вы не согласны с тем, что Ваш материал размещён на этом сайте, пожалуйста, напишите нам, мы в течении 1-2 рабочих дней удалим его.