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).
Verificación de código mediante matemáticas formales
Alcance niveles altos de calidad y seguridad sin falsos negativos.
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 y mejora del código
Reduzca el tiempo dedicado a revisiones, depuración y pruebas de solidez del código.
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.
Funcionalidades más recientes
Gestión de autorizaciones para proyectos
Cree y aplique políticas de autorización para acceder a los proyectos.
Soporte de AUTOSAR
Compruebe las discordancias en tiempo de ejecución entre las especificaciones de AUTOSAR y la implementación de código.
Cálculo del tamaño de pila
Determine el uso máximo de la pila por un programa en C y funciones individuales.
Configuración a partir del sistema de compilación
Genere automáticamente módulos de configuración de Polyspace a partir del sistema de compilación.
Configuración de verificación de código multitarea
Especifique tareas cíclicas e interrupciones inapropiables directamente como opciones de verificación.
Consulte las notas de la versión para obtener detalles sobre estas características y las funciones correspondientes.
