Polyspace Code Prover
Demostración de la ausencia de errores en tiempo de ejecución en el software
Polyspace Code Prover™ es una sólida herramienta de análisis estático que demuestra la ausencia de desbordamientos, división por cero, acceso a arrays fuera de límites y otros errores en tiempo de ejecución en el código fuente C y C++. Produce resultados sin necesidad de ejecutar programas, instrumentación de código o casos de pruebas. Polyspace Code Prover emplea el análisis semántico y la interpretación abstracta basados en métodos formales para verificar el comportamiento interprocedimental, de control y de flujo de datos del software. Se puede emplear para verificar código escrito a mano, código generado o una combinación de ambos. Las instrucciones de código muestran una codificación por colores para indicar si están libres de errores en tiempo de ejecución, presentan errores, no se puede acceder a ellas o no se han comprobado.
Polyspace Code Prover muestra información de rango sobre variables y valores de devolución de función, y puede indicar qué variables superan los límites de rango especificados. Los resultados de la verificación de código se pueden usar para rastrear métricas de calidad y comprobar la conformidad con los objetivos de calidad del software. Puede utilizar Polyspace Code Prover con el IDE de Eclipse™ para verificar el código en su equipo de escritorio.
El soporte para estándares del sector está disponible a través de IEC Certification Kit (para IEC 61508 e ISO 26262) y DO Qualification Kit (para DO-178).
Comience:
Demostración de la ausencia de errores en tiempo de ejecución críticos
Identifique las operaciones del código C/C++ y Ada que nunca presentarán un error en tiempo de ejecución, independientemente de las condiciones.
Detección de errores en tiempo de ejecución.
Detección de errores que eluden otros métodos de comprobación
Analice todas las rutas de código con respecto a todas las posibles entradas sin necesidad de ejecutar código.
Jerarquía de llamadas.
Creación de artefactos de certificación
Complete el proceso de certificación en el caso de objetos basados en estándares del sector.
DO Qualification Kit.
Comprensión de la causa raíz de los problemas y mejora del diseño
Examine el flujo de control y de datos a través del software y vea información de rango asociada con variables y operadores.
Descripción emergente que muestra los posibles rangos de todas las condiciones en tiempo de ejecución.
Elusión del comportamiento de software imprevisto
Localice todas las secciones de código a las que no se puede acceder a través de ninguna ruta de ejecución y los errores en la lógica y la estructura del programa.
Localización de código no ejecutable.
Rastreo de resultados de verificación de código en modelos de Simulink
Ejecute la verificación en el código generado y rastree los hallazgos hasta el bloque de modelo de origen en Simulink.
Rastreo de resultados de verificación de código hasta el modelo de Simulink.
Automatización del proceso de verificación de código
Use Polyspace Code Prover Server™ para ejecutar el motor de análisis estático de Polyspace Code Prover en un equipo servidor con herramientas de automatización de compilaciones como Jenkins y Bamboo.
Automatización del proceso de verificación de código.
Notificación y carga de resultados para la revisión colaborativa
Asigne automáticamente los defectos a los propietarios de los componentes, envíe notificaciones por correo electrónico y cargue los resultados en Polyspace Code Prover para clasificar y resolver los problemas.
Envío de notificaciones por correo electrónico con los resultados de Polyspace Code Prover.
Revisión de resultados de Polyspace Code Prover para clasificar y resolver problemas
Polyspace Code Prover Access™ proporciona una interfaz de navegador web para los resultados de verificación de código y las métricas de calidad de Polyspace almacenados en un repositorio central. Utilice las herramientas de navegación del navegador web para investigar los resultados de la verificación de código, que se muestran junto con este.
Detección de errores en tiempo de ejecución.
Objetivos de calidad de proyectos y software
Los paneles muestran información que se puede utilizar para supervisar la calidad del software, el estado del proyecto, el número de defectos, las métricas del código y los objetivos de calidad del software.
Panel de visión general del proyecto.
Integración con las herramientas de rastreo de errores existentes
Utilice la interfaz de navegador web para crear y asignar tickets en herramientas de rastreo de errores como Jira.
Creación de un ticket.
Soporte para compiladores
configure el análisis de Polyspace para emular los compiladores de Microchip MPLAB XC16 y XC32
Comprobación del código de inicialización
verifique el código de inicialización solo antes de comprobar el resto del programa y comprobar si todas las variables globales están explícitamente inicializadas
Soporte para Simulink
analice el código personalizado llamado desde bloques Function C
Consulte las notas de la versión para obtener detalles sobre estas características y las funciones correspondientes.
