„Armada“ prüft komplexe Software auf „Bugs“

Forscher der University of Michigan und der Carnegie Mellon University haben zusammen mit Microsoft Research eine Technik entwickelt, um komplexe Computerprogramme ohne traditionelle Software-Tests auf "Bugs" zu prüfen. [...]

"Armada" findet Software-"Bugs"
"Armada" findet Software-"Bugs" (c) James Osborne / Pixabay

Bei diesem Verfahren setzen sie auf das System „Armada“, das auf Basis des Prinzips der formalen Verifikation arbeitet und mithilfe mathematischer Methoden feststellt, ob Algorithmen auch wirklich richtig funktionieren und genau das tun, was sie sollen.

Simultane Berechnungen

„Unser System zielt auf Software ab, bei der mehrere Aufgaben simultan berechnet werden. Diese sogenannte ‚concurrent execution‘ ist eine weitverbreitete Methode, um die Leistung zu erhöhen“, erklärt Manos Kapritsos, Assistant Professor für Computer Science & Engineering an der University of Michigan. Ein gängiges Beispiel hierfür sei etwa die Anwendung bei Multi-Core-CPUs. „Die große Herausforderung dabei ist, dass viele Code-Threads gleichzeitig koordiniert werden müssen“, erläutert Projekt-Mitarbeiter Upamanyu Sharma.

„Um die Korrektheit solcher Programme zu verifizieren, muss man auch die riesige Zahl von möglichen Verzahnungen in Betracht ziehen, die auftreten können, wenn multiple Berechnungen gleichzeitig ablaufen“, so Sharma. In der Praxis sei das schwierig und aufwändig. „Im Moment gibt es zwar eine Reihe von Ansätzen für concurrent executions. In unserem Projekt wollen wir aber ein einziges Framework entwickeln, über das User mehrere Prüftechniken anwenden können, um den Aufwand so stark wie möglich zu reduzieren.“

Vereinfachter Programmcode

Bei Armada wird ein Programmcode, der auf simultane Berechnungen setzt, zunächst durch eine Reihe von Transformationen auf eine viel einfachere Form gebracht. „Der Entwickler muss dann nur überprüfen, ob jeder Vereinfachungsschritt auch wirklich repräsentativ für das komplexere ganze Programm ist. Nach jeder Transformation kann man nachschauen, ob das System korrekt arbeitet und das gleiche tut wie im Schritt zuvor“, schildert Kapritsos.

Die Überprüfung selbst übernimmt Armada automatisch für jeden einzelnen Schritt der Vereinfachung. Wird ein Fehler gefunden, kann der Nutzer den letzten Schritt noch einmal ändern und neuerlich prüfen lassen. „Letztlich muss der Entwickler nur eine Spezifikation für das gesamte System vornehmen. Im Bereich der Prüfung von concurrent Programmen ist das die Methode, die mit Abstand am wenigsten Aufwand verlangt“, betont der Forscher.


Mehr Artikel

News

KI in der Softwareentwicklung

Der “KI Trend Report 2025” von Objectbay liefert Einblicke, wie generative KI entlang des Software Engineering Lifecycle eingesetzt wird. Dafür hat das Linzer Softwareentwicklungs-Unternehmen 9 KI-Experten zu ihrer Praxiserfahrung befragt und gibt Einblicke, wie der Einsatz von KI die IT-Branche verändert wird. […]

News

F5-Studie enthüllt Lücken im Schutz von APIs

APIs werden immer mehr zum Rückgrat der digitalen Transformation und verbinden wichtige Dienste und Anwendungen in Unternehmen. Gerade im Zusammenhang mit kommenden KI-basierten Bedrohungen zeigt sich jedoch, dass viele Programmierschnittstellen nur unzureichend geschützt sind. […]

News

VINCI Energies übernimmt Strong-IT

VINCI Energies übernimmt Strong-IT in Innsbruck und erweitert damit das Leistungsspektrum seiner ICT-Marke Axians. Strong-IT schützt seit mehr als zehn Jahren Unternehmen gegen digitale Bedrohungen, während Axians umfassende IT-Services einbringt. […]

Be the first to comment

Leave a Reply

Your email address will not be published.


*