Polyspace Code Prover

BEDEUTENDES UPDATE

 

Polyspace Code Prover

Bestätigung der Abwesenheit von Laufzeitfehlern in Software

Polyspace Code Prover™ ist ein leistungsfähiges Tool für statische Analysen, mit dem die Abwesenheit von Fehlern wie Überlauf, Division durch null, Array-Zugriffe außerhalb des gültigen Bereichs und anderen Laufzeitfehlern in C- und C++-Quellcode nachgewiesen werden kann. Eine Ausführung des Programms, eine Code-Instrumentierung oder Testsituationen sind hierfür nicht erforderlich. Anhand von semantischer Analyse und abstrakter Interpretation basierend auf formalen Methoden überprüft Polyspace Code Prover das prozessübergreifende sowie das Kontrollfluss- und Datenflussverhalten der Software. Damit können Sie handgeschriebenen Code, generierten Code oder eine Kombination der beiden überprüfen. Jede Code-Anweisung ist farblich gekennzeichnet, je nachdem, ob der Code frei von Laufzeitfehlern, nachweislich fehlerhaft, unerreichbar oder unbewiesen ist.

Polyspace Code Prover zeigt Bereichsinformationen für Variablen und Funktionsrückgabewerte und kann nachweisen, welche Variablen vorgegebene Bereichsgrenzen überschreiten. Die Ergebnisse der Code-Verifikation können zur Überwachung von Qualitätsmesswerten und Überprüfung der Übereinstimmung mit Ihren Softwarequalitätszielen verwendet werden. Polyspace Code Prover kann für die Verifikation von Code auf Ihrem Desktop-Computer mit Eclipse™ IDE verwendet werden.

Die Unterstützung von Branchenstandards ist möglich über das IEC Certification Kit (für IEC 61508 und ISO 26262) und das DO Qualification Kit (für DO-178).

Verifikation von Code mithilfe formaler Mathematik

Erreichen Sie ein höheres Maß an Qualität und Sicherheit ohne falsch negative Ergebnisse.

Bestätigung der Abwesenheit von kritischen Laufzeitfehlern

Identifizieren Sie Operationen mit C/C++ und Ada-Code, bei denen es unabhängig von den Laufzeitbedingungen nie zu Laufzeitfehlern kommt.

Erkennen von Laufzeitfehlern.

Erkennung von anderweitig nicht nachweisbaren Fehlern

Analysieren Sie alle Code-Pfade auf mögliche Eingaben ohne Code-Ausführung.

Aufrufhierarchie.

Erstellung von Zertifizierungsdokumenten

Schließen Sie die Zertifizierungsverfahren für Ihre Projekte nach gültigen Indistriestandards ab.

DO Qualification Kit.

Verständnis und Verbesserung von Code

Verbringen Sie weniger Zeit mit Code-Prüfung, Debugging und Stabilitätstests.

Verstehen der Ursache von Problemen und Verbessern des Entwurfs

Überprüfen Sie den Steuer- und Datenfluss durch die Software und lassen Sie sich Details zu den Wertebereichen anzeigen, die Variablen und Operatoren zugewiesen wurden.

Tooltip, der die möglichen Bereiche für alle Laufzeitbedingungen anzeigt.

Verhinderung von unbeabsichtigtem Softwareverhalten

Ermitteln Sie alle Code-Abschnitte, die über einen Ausführungspfad nicht erreichbar sind, sowie Fehler in Logik und Programmstruktur.

Ermittlung von totem Code.

Nachverfolgung der Code-Verifikationsergebnisse zu Simulink-Modellen

Verifizieren Sie generierten Code und verfolgen Sie die Ergebnisse bis zum ursprünglichen Modellblock in Simulink zurück.

Rückverfolgung der Ergebnisse der Codeverifikation zum Simulink-Modell.

Automatisierung der Code-Verifikation mit Polyspace Code Prover Server

Sorgen Sie durch frühe und häufige Analysen des Codes für kontinuierliche Integration.

Automatisierung der Code-Verifikation

Verwenden Sie Polyspace Code Prover Server™, um die Engine für statische Analysen von Polyspace Code Prover mit Build-Automatisierungstools wie Jenkins und Bamboo auf einem Servercomputer auszuführen.

Automatisierung der Code-Verifikation.

Meldung und Upload von Ergebnissen für die gemeinsame Überprüfung

Lassen Sie Defekte automatisch den Besitzern der jeweiligen Komponente zuweisen, Benachrichtigungen per E-Mail versenden und Ergebnisse in Polyspace Code Prover Access hochladen, um Probleme vorzuselektieren und zu lösen.

Versenden von E-Mail-Benachrichtigungen mit Ergebnissen von Polyspace Code Prover.

Gemeinsame Überprüfung mit Polyspace Code Prover Access

Geben Sie Verifikationsergebnisse und Qualitätsmesswerte an das Softwareentwicklerteam weiter.

Überprüfen von Analyseergebnissen, um Probleme vorzuselektieren und zu lösen

Polyspace Code Prover Access™ bietet eine Webbrowser-Benutzeroberfläche für Ergebnisse der Code-Verifikation mit Polyspace und Qualitätsmesswerten, die in einem zentralen Repository gespeichert werden. Anhand der Navigationswerkzeuge in Ihrem Browser können Sie die Ergebnisse der Code-Verifikation, die zusammen mit dem Code angezeigt werden, überprüfen.

Erkennen von Laufzeitfehlern.

Projekt- und Softwarequalitätsziele

In Dashboards werden Informationen angezeigt, die Sie zur Überwachung der Softwarequalität, des Projektstatus, der Anzahl der Defekte, der Code-Metriken und der Softwarequalitätsziele nutzen können.

Dashboard mit Projektüberblick.

Einbindung in die bereits vorhandenen Bug-Tracking-Tools

Verwenden Sie die Webbrowseroberfläche zum Erstellen und Zuweisen von Tickets mit Bug-Tracking-Tools wie etwa Jira.

Erstellung eines Tickets.

Neue Funktionen

Verwaltung der Projektautorisierung

Erstellung und Umsetzung von Autorisierungsrichtlinien für den Zugriff auf Projekte

AUTOSAR-Unterstützung

Ermittlung von Laufzeitabweichungen zwischen AUTOSAR-Spezifikationen und der Code-Implementierung

Berechnung der Stack-Größe

Bestimmung der maximalen Stack-Nutzung durch ein C-Programm und einzelne Funktionen

Konfiguration aus Build-Systemen

Automatische Erzeugung von Polyspace-Konfigurationsmodulen aus Build-Systemen

Einrichtung der Multitasking-Code-Verifikation

Einfaches Einrichten zyklischer Tasks und nicht unterbrechbarer Interrupts direkt in den Analyseoptionen

Details zu diesen Merkmalen und den zugehörigen Funktionen finden Sie in den Versionshinweisen.

Kostenlose Testversion anfordern

Eine 30-tägige Erkundungsreise in greifbarer Nähe.

Jetzt downloaden

Bereit zum Kauf?

Angebot anfordern und entdecken Sie Erweiterungsprodukte.

Studieren Sie?

Fordern Sie die MATLAB und Simulink Student Software an.

Weitere Informationen