Übersicht
Auf diesem Workshop werden die beiden großen deutschen Forschungs- und Entwicklungsprojekte auf dem Gebiet der Verifikation und Analyse eingebetteter Systeme, AVACS und VERISOFT, ausgesuchte Ergebnisse aus dem ersten Jahr ihrer Forschungstätigkeit präsentieren. Als von der DFG geförderter Sonderforschungsbereich/Transregio liegt die Herausforderung für AVACS dabei in der Grundlagenforschung und insbesondere in der Entwicklung neuartiger Verifikationsalgorithmen für alle Bereiche des Entwurfsraums komplexer eingebetteter Systeme. Das vom BMBF geförderte langfristig angelegte Forschungsprojekt VERISOFT hat als Ziel, mit Hilfe von state-of-the-art Verifikationswerkzeugen vollständig verifizierte Komponenten für die Benutzung.
The foundational project AVACS (www.avacs.org) combines the expertise in formal verification at its three sites Freiburg, Oldenburg, and Saarbrücken to address the rigorous mathematical analysis of models of complex safety critical computerized systems, such as aircrafts, trains, cars, or other artifacts, whose failure can endanger human life. AVACS aims at raising the state of the art in automatic verification and analysis techniques of such complex systems from its current level of applicability to isolated points in the design space of such systems to a level allowing a comprehensive, holistic, and ultimately automatic verification of such systems, with research activities structured into three key project areas, addressing verification of real-time systems, hybrid systems, and holistic system verification, respectively.
The VERISOFT project (www.verisoft.de) combines the expertise of key industrial (BMW, Infineon, T-Systems) and academic teams to achieve fully verified key application components, covering the full design layer from applications to hardware, strengthening the competitive positioning in the addressed industrial sectors by being able to offer fully formally verified components. To this end, formal mathematical proofs will be rigorously established using a combination of state-of-the-art interactive and automatic verification methods.
Carl von Ossietzky Universität Oldenburg
Universität des Saarlandes
Download this text and the workshop program as PDF