Polyspace Code Prover

Dimostrazione dell’assenza di errori di run-time nel software

Polyspace Code Prover dimostra l’assenza di overflow, divisioni per zero, accesso agli array fuori limite e altri errori di run-time nel codice sorgente C e C++. Produce risultati senza la necessità di esecuzione del programma, code instrumentation o casi di test. Polyspace Code Prover utilizza l’analisi statica e l’interpretazione astratta basata su metodi formali. È possibile impiegarlo su codice scritto a mano, generato o una combinazione dei due. Ciascuna operazione è contrassegnata da un colore che indica se l’istruzione è priva di errori di run-time, dimostrata come fallimentare, non eseguibile o non dimostrata.

Polyspace Code Prover mostra inoltre le informazioni di intervallo per le variabili e i valori restituiti delle funzioni ed è in grado di dimostrare quali variabili superano i limiti di intervallo specificati. I risultati possono essere pubblicati su una dashboard per monitorare le metriche di qualità e garantire la conformità agli obiettivi di qualità del software.

Grazie all’IEC Certification Kit (per IEC 61508 e ISO 26262) e al DO Qualification Kit (per DO-178) sono supportati numerosi standard industriali.

Che cos’è Polyspace Code Prover?

Utilizzo dei risultati di Code Prover e dei colori del codice sorgente.

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.

Documentazione

Visualizzazione di un suggerimento con possibilità di intervalli per le condizioni di run-time.

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.

Documentazione

Rilevamento di codice morto nella logica e nella struttura del programma.

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.

Documentazione

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.

Documentazione

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.

Documentazione

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.

Documentazione

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.

Documentazione

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.

Analisi dell’impatto

Monitora e verifica formalmente l’impatto di una variabile specifica, locale o globale, su altre variabili o su costrutti specifici. Esegui l’analisi dei segnali per soddisfare i requisiti del CARB per i software OBD, comprova la libertà dalle interferenze nel contesto della ISO 26262 e analizza l’effetto dei parametri di calibrazione. Nel contesto della sicurezza software, esegui una taint analysis e il monitoraggio di un flusso di dati sensibili.