Tool verifiziert Embedded Software

Das US-Software-Unternehmen Esterel Technologies hat seine ‘Scade Suite’ – eine Entwicklungsumgebung für sicherheitskritische Embedded Software – um ein neues Modul – das ‘Compiler Verification Kit’ (CVK) – erweitert. Die Scade-Software erlaubt es, eindeutige Spezifikationen von Softwaresystemen zu erstellen, zu simulieren und diese Designs mit formalen Methoden automatisch zu verifizieren.

Mit dem KCG – dem automatischen Code-Generator der ‘Scade Suite’ – kann direkt zertifizierbarer Code erzeugt werden. Das CVK ermöglicht Entwicklern eine Prüfung, ob dieser C-Code auf der Zielplattform korrekt ausgeführt wird. Das Tool ist prozessorunabhängig und laut Hersteller mit allen plattformübergreifenden C-Entwicklungssystemen kompatibel.

“Das CVK sichert den Zertifizierungsfluss zwischen den grafischen Scade-Modellen, dem KCG-generierten C-Code und dem Objektcode,” heißt es von Chip Downing, CEO von Esterel. Die Verifikation mit dem CVK müsse für jede Kombination aus Compiler, Linker und Prozessor damit nur einmal durchgeführt werden. Das spare Entwicklungs- und Testressourcen.