Scalable Verification of Industrial Embedded Control Systems (SAVES)

Grunddaten zu diesem Projekt

Beschreibung

Eingebettete Systeme umgeben uns in unserem Alltag überall. Ihre Funktionalität reicht von einfachen Mikrocontrollern in einem Kühlschrank bis hin zu komplexen Systemen mit Millionen von Codezeilen, zum Beispiel in Autos, Flugzeugen oder intelligenten Fabriken. Bei solchen Systemen hat ein Ausfall oft schwerwiegende Folgen, wie große finanzielle Verluste oder sogar den Verlust von Menschenleben. Daher sind die Korrektheit und Zuverlässigkeit eingebetteter Systeme von entscheidender Bedeutung. Die Korrektheit eingebetteter Systeme zu gewährleisten, ist jedoch schwierig. Mit Trends wie Industrie 4.0, dem Internet der Dinge und dem autonomen Fahren nimmt die Komplexität eingebetteter Systeme stetig zu. Eine Voraussetzung, um die korrekte Funktion von industriellen eingebetteten Systemen unter allen Umständen sicherzustellen, ist ein klares Verständnis der Modelle und Sprachen, die im Entwicklungsprozess verwendet werden. Formale Methoden bieten eine Grundlage, um den Entwicklungsprozess systematisch, wohldefiniert und automatisiert zu gestalten. Für viele industriell relevante Sprachen und Modelle ist die Semantik jedoch nur informell definiert. Zusammen mit der begrenzten Skalierbarkeit von formalen Entwurfs- und Verifikationstechniken macht dies die formale Verifikation von industriellen eingebetteten Steuerungssystemen zu einer schwierigen Herausforderung, die mit den derzeit verfügbaren Methoden und Werkzeugen nicht zufriedenstellend gelöst werden kann. Gleichzeitig sehen wir, dass im Bereich der deduktiven Programmverifikation leistungsfähige Techniken und Werkzeuge entwickelt wurden, um auf Software mit unbeschränkten Parametern zu schließen, z.B. die VerCors Tool Suite. In diesem Projekt werden wir diese Techniken um Konzepte zur Bewältigung von Heterogenität, Nebenläufigkeit und Echtzeit erweitern, um sie für industrielle eingebettete Systeme geeignet zu machen.