Entwicklung eines durchgängigen Verifikationsablaufes für den ESL Entwurf

• Antragsteller: Professor Dr. Rolf Drechsler
• Fachliche Zuordnung: Rechnerarchitektur, eingebettete und massiv parallele Systeme
• Förderung: Förderung von 2011 bis 2018
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 188461301

• Erstellungsjahr: 2018

Zusammenfassung der Projektergebnisse

Die durch das Format als Reinhart Koselleck-Projekt geplanten Ziele konnten bisher zur vollsten Zufriedenheit des Antragstellers erreicht werden. So stand hier nicht die Bearbeitung von explizit vorgegebenen Arbeitspaketen im Vordergrund, sondern die Erarbeitung und Entwicklung von grundsätzlich neuen Paradigmen, die zur Lösung der perspektivischen Forschungsfragen geeignet schienen. Die Möglichkeiten und Freiheiten, welche Reinhart Koselleck-Projekte dem/der geförderten Wissenschaftler/-in bieten, erlaubten die Entwicklung von Visionen anstatt der sonst üblichen Betrachtung „kleinerer Schritte“. Sie bot Zeit und Ressourcen, sich in Themen aus anderen Disziplinen einzuarbeiten und dort Beiträge zu leisten bzw. Expertise von dort in den eigenen Bereich zu übertragen. Dadurch gelang es, Paradigmen und Methoden aus anderen Feldern wie dem agilen Entwurf, der natürlichen Sprachverarbeitung sowie dem Softwareentwurf in die Domäne der eingebetteten und cyber-physischen Systeme zu übertragen. Dies begründet die Basis für einen komplett neuen Verifikationsablauf, der die Probleme und Grenzen bisheriger Ansätze überwindet. Zeitgleich konnten z.B. mit dem Completeness- Driven Development oder der Hardware/Software Co-Visualisierung komplett neue Forschungsgebiete geschaffen werden. Dieser Fortschritt wäre mit „regulären“ Förderprogrammen so nicht möglich gewesen.

Projektbezogene Publikationen (Auswahl)

• Assisted Behavior Driven Development Using Natural Language Processing. In International Conference on Objects, Models, Components, Patterns (TOOLS), 2012
  M. Soeken, R. Wille, and R. Drechsler
  
• Completeness-Driven Development. In International Conference on Graph Transformations (ICGT), 2012
  R. Drechsler, M. Diepenbeck, D. Große, U. Kühne, H. M. Le, J. Seiter, M. Soeken, and R. Wille
  
• Formal Specification Level: Towards Verificationdriven Design Based on Natural Language Processing. In Forum on Specification and Design Languages (FDL), 2012
  R. Drechsler, M. Soeken, and R. Wille
  
• Verifying SystemC using an intermediate verification language and symbolic simulation. In Design Automation Conf. (DAC), 2013, pp. 116:1–116:6
  H. M. Le, D. Große, V. Herdt, and R. Drechsler
  
• A Generic Representation of CCSL Time Constraints for UML/MARTE Models. In Design Automation Conference (DAC), pages 122:1-122:6, 2015
  J. Peters, R. Wille, N. Przigoda, U. Kühne, and R. Drechsler
  
• Verifying SystemC using Stateful Symbolic Simulation, In Design Automation Conference (DAC), pp. 49:1-49:6, 2015
  V. Herdt, H. M. Le, R. Drechsler
  
• Formal verification of integer multipliers by combining Gröbner basis with logic reduction. In Design Automation and Test in Europe (DATE), pages 1048–1053, 2016
  A. Sayed-Ahmed, D. Große, U. Kühne, M. Soeken, and R. Drechsler
  
• Verifying the Structure and Behavior in UML/OCL Models Using Satisfiability Solvers. Cyber-Physical Systems: Theory & Applications, 1(1):49-59, 2016
  N. Przigoda, M. Soeken, R. Wille, and R. Drechsler
  
• Towards a Verification Flow Across Abstraction Levels: Verifying Implementations Against Their Formal Specification. IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems (TCAD), 36(3):475-488, 2017
  P. Gonzalez de Aledo, N. Przigoda, R. Wille, R. Drechsler, and P. Sanchez
  
• Towards fully automated TLM-to-RTL property refinement. In Design Automation and Test in Europe (DATE), 2018
  V. Herdt, H. M. Le, D. Große, and R. Drechsler