Polyspace Client for Ada

Nachweis der Abwesenheit von Laufzeitfehlern im Quellcode

Polyspace Client™ für Ada weist die Abwesenheit von Fehlern durch Überlauf, Division durch Null, Array-Zugriff außerhalb der Grenzen und bestimmte weitere Laufzeitfehler in Ada83- und Ada95-Quellcode nach. Diese Ergebnisse erfordern weder eine Programmausführung noch eine Code-Instrumentierung oder Testfälle. Polyspace Client for Ada nutzt abstrakte Interpretationsmethoden für die Codeverifizierung, die auf formalen Methoden beruhen. Analyseergebnisse werden im Quellcode angezeigt. Jede Anweisung im Code ist farblich markiert, um zu verdeutlichen, ob sie frei von Laufzeitfehlern ist, nachweislich fehlschlagen wird, nicht erreichbar oder unbewiesen ist. Polyspace Client for Ada zeigt Bereichsinformationen für Variablen und Ausgabewerte von Funktionen an und prüft, welche Variablen festgelegte Bereichsgrenzen überschreiten.

Sie können Polyspace Client for Ada auf Ihrem Desktop nutzen, um vor der Kompilierung und den Tests Codeanalysen durchzuführen und zu überprüfen.

Polyspace Client for Ada nutzt unterschiedliche Farben zur Kennzeichnung statistisch geprüfter Ada-Anweisungen.

Nachweis der Abwesenheit kritischer Laufzeitfehler

Prüfen Sie Ada83- oder Ada95-Codevorgänge auf korrektes Laufzeitverhalten. Identifizieren Sie Anweisungen, die unabhängig von den Laufzeitbedingungen nie Laufzeitfehler aufweisen. Analysieren Sie Schwachstellen in der Laufzeit, unterstützt durch Event-Traces, Wertebereiche für Variablen und Aufrufbäume, die mit den Ergebnissen verknüpft sind. Polyspace Client for Ada verwendet formale Methoden, um Fehler zu finden, die anderen Testmethoden entgehen. Analysieren Sie alle Codepfade hinsichtlich aller potenziellen Eingaben, ohne Code ausführen zu müssen.

CSEE Transport sorgt für zuverlässige Software für Hochgeschwindigkeits-Schienennetze

Dokumentation

Drei geöffnete Fenster. Ein Fenster mit farblich codierten Anweisungen, ein Fenster mit Parametern und eines mit grafischen Elementen.

Interaktive Analysen auf Desktop-Computern

Organisieren und konfigurieren Sie Ihre Projekte und führen Sie statische Codeanalysen für Teilmengen von Softwareprojekten aus, um Codeänderungen zu qualifizieren, bevor Sie den Quellcode an das Quellcode-Repository übergeben. Nutzen Sie Polyspace Client for Ada für die Erstellung von Berichten sowie zum Überprüfen und Vorsortieren der Ergebnisse. Ermitteln Sie die Ursache komplexer Programmierfehler mithilfe Debugger-ähnlicher Ansichten, um Schritt für Schritt durch jede Anweisung zu navigieren, die zu einem Laufzeitfehler führt.

Dokumentation

Polyspace Client for Ada stellt eine Liste aller globalen Variablen der analysierten Software bereit.

Besseres Software-Design und besseres Codeverständnis

Überprüfen Sie die Kontroll- und Datenflüsse in der Software und sehen Sie Wertebereichsinformationen, die mit Variablen und Operatoren verbunden sind.

NATO HAWK Management Office beschleunigt die Analyse geschäftskritischer Anwendungen

Dokumentation

Polyspace Client for Ada hebt Code, der nicht erreichbar ist, grau im Quellcode hervor.

Optimierung der Softwareleistung

Identifizieren Sie sichere Vorgänge und entfernen Sie defensiven Code wie die Division durch Null. Erkennen und entfernen Sie Fehler in Logik und Programmstruktur sowie Codezweige, die von Ausführungspfaden nicht erreicht werden können, um den Speicherbedarf gering zu halten.

Dokumentation

Polyspace Client for Ada kann einen Graph des Pfads anzeigen, der zu einem potenziellen Data Race führt.

Analyse der Verwendung globaler Variablen

Beschleunigen Sie das Debugging von Lese-/Schreibvorgängen mit globalen Variablen, einschließlich Variablen, die von Tasks oder Threads gemeinsam genutzt werden. Der Mehrfachzugriffs-Graph bietet Einblicke in den Kontroll- und Datenfluss, der zu einem Data Race führt. Identifizieren Sie ungenutzte globale Variablen für die Codeoptimierung.

Dokumentation

Statische Anwendungssicherheitstests

Weisen Sie nach, dass die Anwendung keine kritischen Sicherheitsschwachstellen aufweist, indem Sie potenziell schwachstellenbehaftete Ada-Anweisungen umfassend auf Faktoren wie Speicherzugriff, Pufferüberlauf oder numerischen Überlauf testen. Unterstützung von 20 CWE-Schwachstellenregeln. Nutzen Sie die Analyseergebnisse des Polyspace Client for Ada als Fuzzing-Ergänzung oder -Ersatz und konzentrieren Sie sich stattdessen auf Vorgänge, die als anfällig identifiziert wurden.

Sicherheit für Embedded-Systeme mit der statischen Polyspace-Analyse (1:52)

Polyspace Client for Ada berechnet die komplette Aufrufhierarchie für Ada-Anwendungen.

Optimierung und Ergänzung von Robustheits- und funktionalen Tests

Verwenden Sie Polyspace Client for Ada für Robustheitstests, indem Sie sich bei Tests auf Anweisungen wie Division durch Null oder Überläufe konzentrieren, die als unsicher eingestuft wurden. Nutzen Sie die Ergebnisse von Polyspace Client for Ada zur Erstellung und Pflege von Grenzwert- und Partitionstests, für die Kontroll- und Datenflussanalyse und den berechneten Bereich von Funktionsparametern und globalen Variablen.

EADS gewährleistet die Zuverlässigkeit von Trägerraketen

Dokumentation

Produktressourcen:

Dokumentation Beispiele Videos Anforderungen Versionshinweise

Interessiert an Polyspace Client for Ada?

Testversion anfordern Preisangebot anfordern

Haben Sie Fragen?

Wenden Sie sich an das technische Team für Polyspace Client for Ada.