Polyspace Code Prover Server è un solido motore di analisi statica che dimostra l’assenza di overflow, divisione per zero, accesso agli array fuori limite e altri errori di run-time nel codice sorgente C e C++. Esegue l’analisi interprocedurale di tutti i possibili flussi di controllo e di dati, incluso il codice multi-thread, per identificare ogni operazione come sempre sicura, sempre difettosa, irraggiungibile o vulnerabile. Polyspace Code Prover Server identifica i segmenti di codice privi di errori di run-time, con difetti comprovati, irraggiungibili o non verificati.
Polyspace Code Prover Server può essere eseguito su una macchina di classe server e integrato in sistemi di build e integrazione continua per la verifica automatizzata utilizzando strumenti come Jenkins®. I risultati dell’analisi possono essere pubblicati su Polyspace Access per la categorizzazione e la risoluzione.
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 di codice con tutti i possibili input senza esecuzione di codice. Identifica le istruzioni che non subiranno mai un errore di runtime indipendentemente dalle condizioni di run-time e individuane altre che devono essere esaminate con attenzione.
Automazione e integrazione di DevOps
Supporta le moderne pratiche di sviluppo del software inserendole nei workflow e negli strumenti DevOps esistenti. Polyspace® è compatibile con i più comuni strumenti di integrazione continua come Jenkins e Bamboo®.
Esecuzione dell'analisi statica del codice su qualsiasi piattaforma
Esegui Polyspace Code Prover Server su un server di automazione on premise o nel Cloud. Utilizza le architetture di riferimento MathWorks per la distribuzione su piattaforme quali Docker, AWS® e Azure®.
Assistenza per certificazione
Crea gli artefatti necessari per completare il processo di certificazione per gli standard del settore. Certificato TÜV SÜD per i livelli più elevati di sicurezza funzionale di IEC 61508 e ISO 26262. Supporta la qualificazione secondo lo standard DO-178C.
Prevenzione dei comportamenti software indesiderati
Identifica tutte le sezioni di codice che non possono essere raggiunte tramite alcun percorso di esecuzione e gli errori nella logica e nella struttura del programma.
Analisi dell’utilizzo delle variabili globali
Risparmia il tempo dedicato al debug dei problemi delle operazioni di lettura/scrittura su variabili globali. Identifica le variabili condivise e inutilizzate non protette.
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.
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 Code Prover Server
Dimostrazione dell’assenza di errori di run-time nel software.
Polyspace Bug Finder
Identificazione dei bug del software utilizzando l'analisi statica.
Polyspace Test
Sviluppo, gestione ed esecuzione di test per il codice C e C++ in sistemi embedded.
Polyspace Bug Finder Server
Identificazione di difetti software tramite analisi statiche in esecuzione su computer server.
Polyspace Client for Ada
Dimostrazione dell’assenza di errori di run-time nel codice sorgente.
Polyspace Code Prover
Dimostrazione dell’assenza di errori di run-time nel software.
Polyspace Server for Ada
Esecuzione della verifica del codice su cluster di computer e pubblicazione delle metriche.