Servicenavigation

Detailseite

Zurück

Projekt Druckansicht

TRR 14:  AVACS - Automatische Verifikation und Analyse komplexer Systeme

Fachliche Zuordnung Informatik, System- und Elektrotechnik
Förderung Förderung von 2004 bis 2015
Projektkennung Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 5485999
 
Erstellungsjahr 2017

Zusammenfassung der Projektergebnisse

Der SFB-Transregio AVACS hat Algorithmen zur automatischen Analyse und formalen Verifikation von komplexen Cyber-Physischen Systemen entwickelt. Derartige Systeme verwenden Software und Hardware zur automatisierten Steuerung, Regelung und Optimierung physischer Systeme wie Fahrzeuge, Flugzeuge, Züge oder kooperierender vernetzter Transportsysteme. Während der 12-jährigen Laufzeit von AVACS ist erwartungsgemäß die Komplexität dieser Systeme bezüglich Anzahl der verwendeten Hardwarebausteine wie Softwareumfang exponentiell gewachsen. Zu Projektbeginn nicht vorhersehbar war die damit einhergehende drastische Zunahme der Autonomie der Entscheidungsfindung, in der bisher von Menschen vorgenommene Abwägungen nunmehr durch in Software realisierte Entscheidungsfindung ersetzt wird. Dies ist prominent aktuell im Bereich des Hochautomatisierten Fahrens beobachtbar, betrifft aber alle "Smart Systems", wie etwa Smart Production, Smart Health, Smart Energy und eben auch Smart Mobility. Die domänenübergreifend zu beobachtenden Delegation von Entscheidungskompetenzen an technische Systeme stellt eine besondere Herausforderung in sicherheitsrelevanten Anwendungen dar. Die durch AVACS adressierte zentrale wissenschaftliche Herausforderung der Bereitstellung von formalen Methoden zum Nachweis von Sicherheits-, Stabilitäts-, Verfügbarkeits- und Echtzeitanforderungen könnte somit nicht besser gewählt worden sein, ist sie damit doch in ihrer Relevanz drastisch gestiegen: Nahezu jede industrielle Anwendungsdomäne wird durch solche hochautomatisierten Systeme kontrolliert werden, der Nachweis ihrer funktionalen Korrektheit, ihrer Sicherheit, und ihrer Verfügbarkeit ist somit von zentraler gesellschaftlicher Bedeutung. AVACS ist es gelungen, durch die standortübergreifende Vernetzung von fachlichen Kompetenzen eine Forschungsumgebung aufzubauen, deren Forschungsresultate dazu führen, dass wir heute • die mathematische Essenz von vernetzten Cyber-Physikalischen Systemen durch kompakte mathematischen Modellbildungen derart präzise gefasst haben, das diese im Prinzip eine vollständige Formalisierung hierarchischer ebenen-übergreifender Entwurfsprozesse solcher Systeme unterstützen, • die Ausdrucksstärke und Komplexität von Logiken charakterisieren können, die zur Formalisierung der Anforderungen der Verfügbarkeit, Sicherheit und Echzeitfähigkeit solcher Systeme auch in kooperativen Anwendungen erforderlich ist, • den Stand der Technik in vielen Klassen formaler Verifikationsalgorithmen und Syntheseverfahren definieren, • die Prinzipien des Entwurfs solcher vernetzter Cyber-Physischer Systeme so tief durchdrungen haben, dass wir Entwurfsregeln aufstellen können, deren Einhaltung die vollständige Analysierbarkeit solcher komplexen Systeme durch eine Kombination systematischer Dekompositionstechniken, kompositioneller Analysetechniken, Abstraktionstechniken und dedizierter in AVACS entwickelter Verifikationsalgorithmen gewährleistet. Während in der ersten Förderphase eine Fokussierung auf jeweils einzelne bekannter Systemaspekte erfolgte, wurde anschließend für solche Modelle von CPS Verifikationsverfahren entwickelt, die eine Vielzahl von Merkmalen solcher Systemklassen gleichzeitig aufweisen, wie etwa probabilistische hybride Automaten mit nicht-linearer Zustandsdynamik, Spiele über sich dynamisch rekonfigurierenden Arenen, dynamisch vernetzte Systeme linearer hybrider Automaten, oder parametrisierte Familien zeitbehafteter Automaten über komplexen Zustandsräumen. Modellklassen mit formal nicht entscheidbaren Verifikationsproblemen erwiesen sich als entscheidbar für Teilklassen, welche die aus industrieller Sicht ohnehin notwendigen Robustheitseigenschaften berücksichtigen. AVACS hat systematisch und nachhaltig den Stand der Forschung bei SMT-Entscheidungsverfahren durch Beiträge zu ihrer Skalierbarkeit und Übertragung auf zuvor unerreicht reichhaltige Fragmente von Arithmetik und Logik geprägt. Zahlreiche Transferaktivitäten greifen Ergebnisse von AVACS auf und führen sie näher an industrielle Anwendungen. Dies kann und wird erfolgreich sein, wenn die von AVACS aufgestellten Entwurfsrichtlinien industriell durchgesetz werden. Unter diesen Umständen werden unsere Resultate dazu beitragen, dass hoch automatisierte vernetzte Cyber-Physikalische Systeme robust und sicher sind.

Projektbezogene Publikationen (Auswahl)

 
 

Zusatzinformationen

© 2024 DFG Kontakt / Impressum / Datenschutz

Textvergrößerung und Kontrastanpassung