Polyspace Code Prover analizza tutti i percorsi del codice rispetto a tutti i possibili input per dimostrare l'assenza di determinati errori di runtime come overflow, divisione per zero e accesso fuori dai limiti degli array nel codice C/C++. Fornisce inoltre informazioni sul controllo e sul flusso dei dati e dimostra la correttezza dell'accesso concorrente alle variabili globali condivise tra i task (thread).
Polyspace Code Prover utilizza l'analisi statica attraverso un'interpretazione astratta basata su metodi formali, producendo risultati senza richiedere l'esecuzione del programma, la strumentazione del codice o casi di test. I risultati sono facili da comprendere e utilizzabili: vengono visualizzati direttamente nel codice sorgente con segnalazioni codificate a colori, informazioni sull’intervallo delle variabili e strumenti di navigazione del codice. È possibile utilizzare Polyspace Code Prover su qualsiasi combinazione di codice C/C++, scritto manualmente o generato da Simulink o da un assistente IA.
Grazie all’IEC Certification Kit (per IEC 61508 e ISO 26262) e al DO Qualification Kit (per DO-178) sono supportati numerosi standard industriali.
Dimostrazione dell’assenza di errori critici di run-time
Analizza tutti i percorsi del codice rispetto a tutti i possibili input senza l’esecuzione del codice. Identifica le istruzioni che non subiranno mai un errore di run-time indipendentemente dalle condizioni di run-time e individuane altre che devono essere esaminate con attenzione.
Miglioramento della progettazione software e comprensione del codice
Analizza il flusso di controllo e di dati attraverso il codice C/C++ e scopri le informazioni di intervallo associate alle variabili e agli operatori.
Ottimizzazione delle prestazioni del software
Rimuovi il codice difensivo identificando operazioni sicure come la divisione per zero e gli overflow. Rileva i rami di codice che non possono essere eseguiti attraverso qualsiasi percorso di esecuzione. Identifica e rimuovi eventuali errori nella logica e nella struttura del programma al fine di ridurre il footprint di memoria.
Analisi dell’utilizzo delle variabili globali
Riduci il tempo dedicato al debug delle operazioni di lettura/scrittura sulle variabili globali, incluse le variabili condivise da attività o thread.
Usa il grafico ad accesso simultaneo per comprendere il flusso di controllo e di dati che può portare a problemi di corse di dati. Identifica le variabili globali inutilizzate al fine di ottimizzare il codice.
Assistenza per certificazione
Crea gli artefatti necessari per completare il processo di certificazione per gli standard industriali. Certificazione completata da TÜV SÜD per l’uso con gli standard IEC 61508 e ISO 26262. Utilizza report e artefatti per i processi DO-178C.
Integrazione con Simulink e Stateflow
Esegui l’analisi sul codice generato e ricollega i risultati a blocchi del modello Simulink sorgente e grafici Stateflow. Avvia l’analisi Polyspace® direttamente dall’ambiente Simulink.
Analisi interattiva sul desktop
Esegui l’analisi statica del codice su progetti software interi o su un sottogruppo. Utilizza lo strumento desktop per generare report e per rivedere e classificare i risultati.
Individua la causa principale di bug complessi in viste debugger per analizzare gradualmente ciascuna istruzione che porta a un errore di run-time. Organizza e configura i tuoi progetti, grazie al supporto nativo di oltre 60 compilatori C e C++ e alla configurazione automatica dell’analisi Polyspace estratta dal sistema di compilazione del progetto.
Test statici di sicurezza delle applicazioni
Dimostra l’assenza di vulnerabilità di sicurezza critiche come overflow del buffer, accesso alla memoria e overflow numerici. Riduci la necessità di test Fuzz analizzando il codice in tutti i percorsi di codice e input senza l’esecuzione di codice.
Risorse di prodotto:
Famiglia di prodotti Polyspace
I prodotti Polyspace rendono il codice critico sicuro testando e monitorando la qualità del software lungo l’intero ciclo di sviluppo.
Polyspace Access
Identificazione dei difetti di codifica, revisione dei risultati delle analisi statiche e monitoraggio delle metriche di qualità del software.
Polyspace Copilot
Assistente di IA ottimizzato per Polyspace.
Polyspace Test
Sviluppo, gestione ed esecuzione di test per il codice C e C++ in sistemi embedded.
Polyspace as You Code
Individua violazioni degli standard di codifica e vulnerabilità del software direttamente dal tuo IDE.
Polyspace Test Server
Esegui test e analizza la copertura strutturale del codice C/C++ su server di automazione.
Polyspace Code Prover Server
Verifica in modo continuo ed esaustivo le istruzioni fondamentali del codice C e C++ nelle pipeline di CI.
Polyspace Bug Finder
Identificazione dei bug del software utilizzando l'analisi statica.
Polyspace Client for Ada
Verifica in modo esaustivo le unità fondamentali delle istruzioni Ada utilizzando metodi formali.
Polyspace Bug Finder Server
Identificazione di difetti software tramite analisi statiche in esecuzione su computer server.
Polyspace Server for Ada
Verifica in modo continuo ed esaustivo le istruzioni fondamentali del codice C e C++ nelle pipeline di CI.
Polyspace Code Prover
Verifica in modo esaustivo le istruzioni fondamentali di C e C++ utilizzando metodi formali.
FAQ su Polyspace Code Prover
Polyspace Code Prover dimostra l'assenza di errori critici a run-time, come overflow, divisione per zero e accessi ad array fuori dai limiti, nel codice C/C++. Fornisce anche viste architetturali, come grafi delle chiamate e informazioni sull'utilizzo dei dati globali, per aiutare a comprendere la struttura del software a partire dal codice.
Polyspace Code Prover utilizza un'analisi statica basata su metodi formali per esplorare tutti i percorsi di esecuzione e gli input nel codice C/C++ senza eseguirlo.
Polyspace Code Prover visualizza i risultati direttamente nel codice sorgente utilizzando annotazioni colorate che indicano se le operazioni sono dimostrate prive di errori a run-time, dimostrate come errate, irraggiungibili o non dimostrate. Fornisce inoltre informazioni sugli intervalli di valori delle variabili e sui valori di ritorno delle funzioni per supportare l'analisi delle cause radice.
Aiuta a migliorare la sicurezza del software dimostrando l'assenza di vulnerabilità critiche come buffer overflow, accessi a memoria non validi e overflow numerici, su tutti i percorsi di esecuzione e per tutti gli input, senza eseguire il codice.
Polyspace Code Prover utilizza metodi formali per dimostrare esaustivamente l'assenza di specifici errori a run-time. Polyspace Bug Finder individua bug, violazioni delle regole di codifica e metriche di qualità del codice su progetti completi durante integrazione e verifica. Polyspace as You Code esegue un sottoinsieme dell'analisi di Polyspace Bug Finder direttamente nell'IDE per aiutare gli sviluppatori a rilevare problemi mentre scrivono il codice.
Polyspace Code Prover viene utilizzato in modalità interattiva tramite un'interfaccia desktop, mentre Polyspace Code Prover Server è ottimizzato per analisi automatizzate nei workflow di integrazione continua (CI) e per la condivisione dei risultati tramite Polyspace Access.
Sì, può analizzare codice generato automaticamente, con risultati tracciabili fino ai modelli Simulink e ai blocchi dSPACE TargetLink. Quando l'analisi viene eseguita da Simulink, è automaticamente configurata in base al modello e alle impostazioni di generazione del codice.
Supporta i workflow di certificazione per IEC 61508, ISO 26262, EN 50128, EN 50657, IEC 62304, ISO 25119 e DO 178C/ED 12C tramite kit di certificazione e qualificazione, con supporto aggiuntivo per ISO/SAE 21434 e Automotive SPICE.
Vuoi saperne di più su Polyspace Code Prover?
Novità
Navigazione nel pannello
ARTICOLI GRATUITI
Note su Polyspace
Navigazione nel pannello
PRODOTTO
