Polyspace Code Prover analiza todas las rutas de código frente a todas las entradas posibles para demostrar la ausencia de ciertos errores de tiempo de ejecución, como desbordamiento, división por cero y acceso a arreglos fuera de los límites en código C/C++. También proporciona análisis de flujo de control y datos, y demuestra que el acceso concurrente a variables globales compartidas entre tareas (hilos) es correcto.
Polyspace Code Prover emplea análisis estático mediante interpretación abstracta basada en métodos formales. Produce resultados sin necesidad de ejecutar el programa, instrumentar el código ni realizar pruebas. Los resultados son fáciles de comprender y de aplicar: se muestran directamente en el código fuente, con hallazgos codificados por colores, información sobre el rango de variables y funcionalidades de navegación por el código. Polyspace Code Prover se puede utilizar con cualquier combinación de código C/C++, escrito manualmente o generado por Simulink o un asistente de IA.
El soporte para estándares del sector está disponible a través de IEC Certification Kit (for IEC 61508 and ISO 26262) y DO Qualification Kit (for DO-178).
Comprobación de ausencia de errores críticos en tiempo de ejecución
Analice todas las rutas de código con todas las posibles entradas sin necesidad de ejecutar código. Identifique instrucciones que nunca presentarán un error en tiempo de ejecución, independientemente de las condiciones en tiempo de ejecución, y encuentre las instrucciones que requieran atención.
Mejora del diseño de software y la comprensión de código
Utilice código C++ para examinar el flujo de control y datos, y vea información sobre los rangos relacionados con variables y operadores.
Optimización del rendimiento del software
Elimine la programación defensiva identificando operaciones seguras y protegidas, tales como la división por cero y los desbordamientos. Detecte ramas de código inaccesibles a través de una ruta de ejecución. Identifique errores de lógica y en la estructura de un programa, y elimínelos para así reducir la superficie de memoria.
Análisis del uso de variables globales
Reduzca el tiempo de depuración de operaciones de lectura/escritura en variables globales, incluidas las variables compartidas por tareas o subprocesos.
Utilice el gráfico de acceso simultáneo para comprender el flujo de control y datos que puede provocar problemas de carrera de datos. Identifique variables globales no utilizadas para optimizar el código.
Soporte para certificación
Cree los artefactos necesarios para completar el proceso de certificación de conformidad con estándares de la industria. Complete el proceso de certificación por TÜV SÜD para su uso con los estándares IEC 61508 e ISO 26262. Utilice informes y artefactos para procesos de DO-178C.
Integración de Simulink y Stateflow
Analice el código generado y rastree los resultados hasta los bloques de modelo de Simulink y los gráficos de Stateflow de origen. Inicie el análisis de Polyspace® desde el entorno de Simulink.
Análisis interactivo en equipos de escritorio
Ejecute análisis estático de código en proyectos de software completos o parciales. Utilice la herramienta de escritorio para generar informes, y revisar y clasificar los resultados.
Identifique la causa raíz de bugs complejos en una vista de depuración, investigando una por una las instrucciones que provocan un error en tiempo de ejecución. Organice y configure proyectos, con soporte nativo para más de 60 compiladores de C y C++, y configuración automática del análisis de Polyspace extraído del sistema de compilación del proyecto.
Pruebas estáticas de la seguridad de aplicaciones
Compruebe la ausencia de vulnerabilidades de seguridad críticas, tales como desbordamientos de buffer, acceso a memoria y desbordamientos numéricos. Reduzca la necesidad de realizar pruebas fuzzing analizando el código en todas sus rutas y entradas sin necesidad de ejecutarlo.
Recursos del producto:
Línea de productos Polyspace
Los productos Polyspace consiguen que el código crítico sea seguro y esté protegido probando y supervisando la calidad del software a lo largo del ciclo de desarrollo.
Polyspace Access
Identifique defectos de codificación, revise resultados de análisis estático y supervise métricas de calidad de software.
Polyspace Copilot
Asistente de IA optimizado para Polyspace.
Polyspace Test
Desarrolle, gestione y ejecute pruebas de código C y C++ en sistemas integrados.
Polyspace as You Code
Identifique infracciones de estándares de codificación y vulnerabilidades de software desde IDE.
Polyspace Test Server
Ejecute pruebas y analice la cobertura estructural de código C/C++ en servidores de automatización.
Polyspace Code Prover Server
Verifique continua y exhaustivamente instrucciones de código C y C++ críticas en flujos de integración continua.
Polyspace Bug Finder
Compruebe reglas de codificación, estándares de seguridad y métricas de código, y detecte bugs.
Polyspace Client for Ada
Verifique exhaustivamente unidades de instrucciones Ada críticas utilizando métodos formales.
Polyspace Bug Finder Server
Identifique defectos de software y aplique reglas de codificación en flujos de integración continua.
Polyspace Server for Ada
Realice verificación de código en clusters de escritorio y publique las métricas
Polyspace Code Prover
Verifique exhaustivamente las instrucciones C y C++ más críticas utilizando métodos formales.
Preguntas frecuentes sobre Polyspace Code Prover
Polyspace Code Prover demuestra la ausencia de errores críticos en run-time, como desbordamientos, división por cero y accesos a arreglos fuera de límites en código C/C++. También proporciona vistas arquitectónicas, como gráficos de llamadas e información sobre el uso de datos globales, para ayudar a comprender la estructura del software a partir del código.
Polyspace Code Prover utiliza análisis estático basado en métodos formales para explorar todas las rutas de ejecución y entradas en código C/C++ sin ejecutarlo.
Polyspace Code Prover muestra los resultados directamente en el código fuente mediante anotaciones codificadas por colores que indican si las operaciones están demostradas como libres de errores en run-time, demostradas como erróneas, inalcanzables o no demostradas. También proporciona información sobre los rangos de valores de las variables y los valores devueltos por las funciones para respaldar el análisis de causas raíz.
Contribuye a mejorar la seguridad del software demostrando la ausencia de vulnerabilidades críticas, como desbordamientos de búfer, accesos inválidos a memoria y desbordamientos numéricos, en todas las rutas de ejecución y para todas las entradas, sin ejecutar el código.
Polyspace Code Prover utiliza métodos formales para demostrar exhaustivamente la ausencia de errores seleccionados en run-time. Polyspace Bug Finder identifica errores, violaciones de reglas de codificación y métricas de calidad del código en proyectos completos durante la integración y la verificación. Polyspace as You Code ejecuta un subconjunto del análisis de Polyspace Bug Finder directamente en el IDE para ayudar a los desarrolladores a detectar problemas mientras escriben código.
Polyspace Code Prover se usa de manera interactiva en una interfaz de escritorio, mientras que Polyspace Code Prover Server está optimizado para análisis automatizados en workflows de integración continua (CI) y para compartir resultados a través de Polyspace Access.
Sí, puede analizar código generado automáticamente, con resultados trazables hasta los modelos de Simulink y los bloques dSPACE TargetLink. Al ejecutarlo desde Simulink, el análisis se configura automáticamente en función del modelo y de la configuración de generación de código.
Admite flujos de trabajo de certificación para IEC 61508, ISO 26262, EN 50128, EN 50657, IEC 62304, ISO 25119 y DO 178C/ED 12C mediante kits de certificación y calificación, con orientación adicional para ISO/SAE 21434 y Automotive SPICE.
¿Tiene interés en Polyspace Code Prover?
Siguientes pasos
Navegación de panel
ARTÍCULOS GRATUITOS
Notas de la versión de Polyspace
Navegación de panel
PRODUCTO
