analysis, and certification of safety-critical software.

ACM Software System Award Timing Stack Usage Runtime Errors Rule Checking Compilation automatisch berechnet sichere Grenzen für die maximale Ausführungszeit von Aufgaben in ausführbaren Binärdateien, unter Berücksichtigung des Cache- und Pipeline-Verhaltens des betreffenden Prozessors. TimeWeaver kombiniert statische Analysen mit Messungen aus Hardware-Traces. Und TimingProfiler ermöglicht es Ihnen, das Zeitverhalten in frühen Phasen der Softwareentwicklung zu überwachen. StackAnalyzer ermittelt automatisch den maximalen Stackverbrauch der Aufgaben in eingebetteten Anwendungen. Es analysiert direkt ausführbare Binärdateien und berücksichtigt alle möglichen Ausführungsszenarien. Eine enge Integration mit TargetLink und SCADE ist verfügbar, ebenso wie Qualifikationssätze für ISO 26262, DO-178B, IEC 61508 und andere Sicherheitsstandards. Astrée weist automatisch das Fehlen von Laufzeitfehlern und ungültigem parallelem Verhalten in C/C++-Anwendungen nach. Es ist präzise für Gleitkommaberechnungen, sehr schnell und außerordentlich genau. Der Analyzer überprüft auch MISRA-Codierungsregeln und unterstützt die Qualifikation für ISO 26262, DO-178C Level A und andere Sicherheitsstandards. Jenkins- und Eclipse-Plugins sind verfügbar. RuleChecker überprüft automatisch Ihren C- oder C++-Code auf Konformität mit MISRA-Regeln, CERT-Empfehlungen und anderen Codierungsrichtlinien, einschließlich eigener Regeln. Er kompiliert auch Code-Metriken und unterstützt eine einfache Qualifikation für ISO 26262, DO-178B/C und andere Sicherheitsstandards. Plugins für TargetLink, Jenkins, Eclipse und ARM Keil µVision sind verfügbar. CompCert ist ein formal verifizierter optimierender C-Compiler für sicherheitskritische und missionskritische Software. Im Gegensatz zu jedem anderen Produktionscompiler ist mathematisch nachgewiesen, dass er frei von Misskompilationsproblemen ist. Dieses Vertrauen in die Korrektheit des Kompilierungsprozesses ist beispiellos und hilft, die höchsten Ebenen der Software-Sicherheit zu erreichen. Automobil Luftfahrt Energie Raumfahrt Kommunikation Seit zwei Jahrzehnten setzt Airbus France unsere Tools bei der Entwicklung sicherheitskritischer Avionik-Software für mehrere Flugzeugtypen ein, einschließlich der Flugsteuerungssoftware des A380, des größten Passagierflugzeugs der Welt. Honda hat unsere Tools bei der Entwicklung der FADEC-Software eines Turbofan-Triebwerks verwendet. Die Technische Universität München verwendet unsere Tools bei der Entwicklung, Prüfung und Optimierung von Flugsteuerungs- und Navigationsalgorithmen. Daimler setzt unsere Tools in vielen Automobilsoftwareprojekten ein, einschließlich des Antriebsstrangsteuerungssystems des Actros-LKW. Bosch Automotive Steering hat ihre Legacy-Tools durch Astrée und RuleChecker ersetzt, was zu erheblichen Einsparungen durch schnellere Analysen, höhere Genauigkeit und geringere Lizenzkosten führt. Continental verlässt sich seit Jahren auf unseren Stack-Analyse-Service, um Überläufe im Stack ihrer Airbag-Steuerungssysteme zu vermeiden. NASA hat unser Timing-Analyse-Tool zur Demonstration des Fehlens von zeitbezogenen Softwarefehlern bei der Untersuchung des Toyota-Falles von 2010 verwendet. OHB verwendet unsere Tools bei der Entwicklung von Bordsoftware, die für den Missionserfolg der SmallGEO-Plattform für geostationäre Kommunikationssatelliten und der GALILEO FOC+++ Plattform für Satellitennavigation unerlässlich ist. ESA hat unseren Runtime-Fehleranalysator verwendet, um das Fehlen von Laufzeitfehlern in der automatischen Andocksoftware des Jules Verne Automated Transfer Vehicle nachzuweisen, sodass es Nutzlasten zur Internationalen Raumstation transportieren konnte. Seit 2003 arbeiten wir mit dem Deutschen Zentrum für Luft- und Raumfahrt an acht verschiedenen mitt