CO­CO­NUT - A COr­rect-by-CON­strUc­Ti­on Work­bench for De­sign and Ve­ri­fi­ca­ti­on of Em­bed­ded Sys­tems

Bild vergrößern

Entwurf und Verifikation moderner eingebetteter HW/SW Plattformen sind stark ineinander verzahnt. Gegenwärtig werden beide Disziplinen mit separaten Methoden bewältigt. Dadurch wird zum einen die Effektivität des Entwurfsprozesses gemindert, zum anderen erschwert es den Entwurf qualitativer Systeme mit vorhersagbaren Eigenschaften. 

Das COCONUT-Projekt konzentriert sich daher auf die Definition eines formalen Frameworks, das den Entwurf und die Verifikation stärker integriert und darüberhinaus eine durchgängige Verifikation für alle Verfeinerungsschritte erlaubt, angefangen von der Spezifikation bis hin zur Logiksynthese und Software-Kompilierung. Dazu soll ein Modellierungs- und Verifikationsfluss beschrieben werden, durch den sowohl der Entwurf neuer Plattformen als auch die Konfiguration plattformbasierter Anwendungen, insbesondere gemischte Analog/Digital-Systeme (z.B. drahtlose Multimedianetzwerke oder Sensornetzwerke), erleichtert und beschleunigt werden kann.

Die wichtigsten Aktivitäten des COCONUT-Projektes sind in diesem Zusammenhang die Definition innovativer Methoden und Werkzeuge, zur

  • Definition und Validierung der Systemeigenschaften einer Spezifikation
  • automatischen Synthese von Systemeigenschaften in eine Implementierung
  • Abbildung hybrider auf diskrete Systemmodelle
  • Realisierung eines "Correct-by-Construction" Entwurfsprozesses
  • Verifikation von Entwurfsverfeinerungsschritten

Dazu sollen eine Reihe formaler Entwurfs- und Verifikationswerkzeuge implementiert werden, die übergreifend auf verschiedenen Abstraktionsebenen arbeiten. Zur Überprüfung der COCONUT Methoden und Werkzeuge sollen diese auf die Referenzplattform "FAUST" angewendet werden. Dabei handelt es sich um eine Network-on-Chip (NoC) Plattform für Multimedia- und Telekommunikationsanwendungen, die per Software konfiguriert werden kann.

Als universitärer Partner beschäftigt sich C-LAB mit der Verbesserung von Methoden und Werkzeugen zur Abstraktion und Verfeinerung von Real-Time Operating Systems (RTOS) Software (z.B., abstrakte Simulationen und Verfeinerung des Software Scheduling). C-LAB  untersucht darüberhinaus die Definition und Synthese von RTOS SW bezogenen Systemeigenschaften.

Projektförderer: EU
Projektlaufzeit: 01/2008 bis 06/2010


Beteiligte Partner:

 AeriLogic (FR), CEA-LETI (FR), EDAlab (IT), Graz University of Technology (AT), SpringSoft (FR), University College Dublin (IE), FBK-irst (IT), University of Southhampton (UK), University of Paderborn (DE), Verona University (IT)
Kontakt: Dr. Wolfgang Müller, C-LAB