(openPR) Weltweit erste Anwendung von Satisfiability zur Beschleunigung von Software-Entwicklung jetzt in Coverity Prevent SQS verfügbar
Coverity, Inc., US- amerikanischer Spezialist für Quellcode-Analyse und Qualitätssicherung von Software, kündigt eine auf Boolescher Satisfiability (SAT) basierende Software-Analyse-Engine an. Wesentlicher Bestandteil der neuen SAT-Engine ist der ‚False Path Pruning Solver’, der die hochakkurate Software DNA-Map nutzt, um automatisch und mit unübertroffener Genauigkeit komplexe Defekte im Quellcode aufzudecken. Dazu wird jeder mögliche Software-Ausführungspfad in boolesche Werte (wahr und falsch) und boolesche Operatoren (wie z.B. und, nicht, oder) übersetzt und geprüft. Diese bit-genaue Software-Abbildung ermöglicht die Analyse von Quellcode erstmals im Bereich kommerzieller Computer-Programmierung mit Hilfe von auf SAT-Technologie basierten Solvern. Der False Path Pruning Solver reduziert die falsch positiven Ergebnisse erheblich, in einem Testprojekt über 2 Mio. Codezeilen um etwa 30 Prozent. Der neue ab sofort verfügbare False Path Pruning Solver ist der erste, den Coverity für seine Prevent SQS Lösung vorstellt, zwei weitere Solver sind für 2008 geplant.
Während sich das Konzept der Booleschen Satisfiability (SAT) in der EDA-Industrie zur Unterstützung der bei Chipdesign-Verifikation eingesetzten Technologie bewährt hat, blieb der Einsatz der SAT-Lösung im Bereich der Software-Analyse bislang aus. Jetzt setzt Coverity mit dieser gänzlichen neuen SAT-Engine neue Maßstäbe bei der Quellcodeanalyse und eröffnet Software-Entwicklern den Zugang zu hoch entwickelter Logik.
Derzeit gängige Engines für die statische Codeanalyse basieren auf der Untersuchung des Datenflusses und auf mehreren Checkern zum Erkennen von Software-Fehlern. Im Unterschied dazu beruht die SAT-Engine auf Boolescher Satisfiability und erkennt mit Hilfe von mehreren parallel arbeitenden False Path Pruning Solvern die Defekte. Dazu nutzt sie die zum Patent angemeldete Software DNA-Map von Coverity’s Prevent SQS. Sie erzeugt eine Bit-genaue Repräsentation des Software-Systems, in der jeder mögliche Software-Ausführungspfad in Boolesche Werte (wahr, falsch) und boolesche Operatoren (z.B. nicht, und, oder) übersetzt und evaluiert wird. Falsche Pfade werden identifiziert und aus den statischen Analyse-Ergebnissen aussortiert. Die Entwickler können sich auf das Testen und Analysieren von potenziellen Fehlern konzentrieren, die den Erfolg ihrer Projekte tatsächlich ernsthaft bedrohen. Der False Path Pruning Solver senkt die Zahl von falsch positiven Ergebnissen bei der statischen Code-Analyse erheblich: In einem Test von über 2 Mio. Codezeilen aus mehreren Anwendungen von Open Source Software aus dem Coverity Scan-Projekt konnte der neue Solver die falsch positiven Ergebnisse um durchschnittlich 30 Prozent reduzieren.
Der ab sofort verfügbare False Path Pruning Solver von Coverity ist der erste auf SAT-Technologie basierende Solver für Prevent SQS. Coverity plant für Anfang 2008 zwei weitere Solver, die Code-Behauptungen statisch überprüfen und kritische Fehlerkategorien einschließlich Ganzzahlüberläufe erkennen. Diese Solver sollen außerdem eine noch größere Anzahl an Pufferüberläufen aufdecken und zugleich die falsch positiven Ergebnisse niedrig halten.
„Coveritys neue SAT-Engine kommt zu einer Zeit, in der immer mehr Unternehmen im Bereich Software-Entwicklung auf leistungsfähigere Quellcode-Analysen setzen, um den Software-Entwicklungszyklus insgesamt zu beschleunigen“, so Theresa Lanowitz, Gründungsmitglied von voke Communications, einem Unternehmen von Technologie-Analysten.
Über 300 Kunden, darunter Branchengrößen wie HP, analysieren mit Coverity Prevent SQS jeden Pfad ihrer Anwendungen. Jetzt, mit dem Einsatz der SAT-Technologie, kann Prevent SQS jeden Wert in jeder Berechnung innerhalb dieser Programme genau untersuchen. Dank dieser gründlichen statischen Codeanalyse liefert Coverity industrieweit die genaueste Überprüfung von kritischen Leistungs- und Sicherheitsschwachstellen.
„Wir möchten unsere Kunden unterstützen, den zuverlässigsten und sichersten Code der Welt zu erzeugen“, betont Ben Chelf, CTO von Coverity. „Durch die Einführung der bewährten Fähigkeiten von SAT in die statische Code-Analyse erhalten Entwickler ein ganzes Arsenal neuer Solver, die hartnäckigste Code-Defekte finden. Indem sie eine Technologie nutzen, die die akkurate Erkennung von Defekten automatisiert, müssen sie nicht länger ihre kostbare Zeit damit vergeuden, Fehler aufzuspüren. Sondern sie können sich darauf konzentrieren, neue Software-Applikationen auf den Markt zu bringen.“
Preis und Verfügbarkeit:
Die neue Version von Coverity Prevent SQS mit dem integrierten False Path Pruning Solver ist ab sofort für C, C++ und Java verfügbar. Die Preise richten sich nach Projektumfang.
Coverity Ltd., Jim Shissler, Director PR; Tel: +1 (0) (415) 694-5342,
Agentur Lorenzoni GmbH, Public Relations, Beate Lorenzoni; Tel.: +49 (0) 8122 / 55917-22,
