Um die zunehmende Systemvariabilität zu meistern, hat das Forschungszentrum Informatik am Karlsruher Institut für Technologie ein Spezifikationskonzept entwickelt, das auf Constraints beruht. Welche Vorteile diese Methodik mit sich bringt, zeigt das Beispiel zur Verifikation eines MOST-Protokolls.
Design Reuse, also die Wiederverwendung bestehender Systemkomponenten, hält sowohl während des Entwurfs als auch während der Verifikation neue Herausforderungen bereit, die sich aus der Komplexität und Vielfalt der Komponenten-Merkmale ergeben. Der folgende Beitrag beschreibt ein Verifikationskonzept mittels automatisierter Festlegung der geeigneten Auswahl, Architektur und Parametrisierung der Komponenten. Das Konzept besteht aus einer neuartigen Verifikationssprache zur Definition des Variantenraums, welcher durch die Komponentenvielfalt aufgespannt wird, einem automatisierten Verfahren zur Bestimmung gültiger Instanzen in Bezug auf komplexe Design Constraints sowie der Integration in einen modellbasierten Entwurfsablauf. Anhand einer experimentellen Evaluierung zur Verifikation eines MOST-Protokolls mit virtuellen Prototypen wird schließlich die Tauglichkeit des beschriebenen Konzepts demonstriert.
Getrieben von der stetig zunehmenden Anzahl und Komplexität eingebetteter Systeme ist die Systementwicklung mittlerweile durch die Wiederverwendung existierender Systemkomponenten und die Integration von externer Intellectual Property (IP) geprägt [1]. Die IP-Elemente weisen häufig eine breite Palette von Parametern auf, die die Anpassung an unterschiedliche Anwendungsfälle gestatten und dadurch für vielseitigste Einsatzmöglichkeiten sorgen. Während des gesamten Entwurfsprozesses sind die Systementwickler mit der Herausforderung konfrontiert, eine passende IP-Auswahl zu bestimmen, die Systemarchitektur zu definieren, über die beste IP-Parametrisierung zu entscheiden und schließlich die getroffenen Entscheidungen zu verifizieren. Der Verifikation eines umfassenden Variantenraums, beispielsweise mit verschiedenen Topologien und Parametrisierungen oder unterschiedlichen Komponenten-Versionen, kommt deshalb eine stetig wachsende Bedeutung zu. An Wichtigkeit gewinnen daher auch die Verifikation von IP-Blöcken in verschiedenen Plattformvarianten sowie die Verifikation der Wechselwirkungen zwischen verschiedenen IP-Blöcken. Thema dieses Beitrags ist eine Methodik, die sich dieser Herausforderungen auf die folgende Weise annimmt:.
Bild 1 illustriert das entwickelte Framework, das sich in drei Teile gliedert: eine auf Templates basierende Plattformvarianten-Spezifikation, eine automatisierte Constraint-Formalisierung für einen SMT/SAT-Solver sowie ein Simulations-Framework für die generierten Systeminstanzen.
Plattformvarianten-Spezifikation
Die Plattformvarianten-Spezifikation deckt zwei Variabilitätsbereiche ab. Zum ersten ermöglicht sie dem Anwender das Spezifizieren struktureller Variabilität, also die Auswahl verschiedener Komponenten und Topologien sowie unterschiedlicher Anzahlen von Komponenten. Zum zweiten ermöglicht sie dem Anwender das Spezifizieren einer Vielfalt beschränkter Parameter für verschiedene Komponenten. Die zur Verfügung stehenden Komponenten, die grundlegende Systemarchitektur und die verfügbaren Parameter werden mit Hilfe einer UML-basierten Spezifikation angegeben. In den UML-Diagrammen sind die Freiheitsgrade des Systems annotiert. Die Fähigkeiten der bestehenden UML und der integrierten Object Constraint Language (OCL) [2] reichen jedoch nicht aus, um die komplexen gegenseitigen Abhängigkeiten zwischen den verschiedenen IPs und Plattformkomponenten zu modellieren. Deshalb wird vorgeschlagen, eine erweiterte Teilmenge der OCL zu verwenden, mit der der Anwender komplexe wechselseitige Abhängigkeiten zwischen Parametern und Struktur spezifizieren kann.
Die Object Variant Constraint Language (OVCL) ergänzt die OCL durch Features wie etwa Assignments (assign()), Schrittweiten für Parameterbereiche (OrderedSetExt{}), Wahrscheinlichkeitsverteilungen (gaussian(), invGaussian(), poisson()) sowie Unterstützung für strukturelle Templates (active()). Diese OVCL-Constraints werden den entsprechenden, mit UML-Diagrammen spezifizierten Plattformelementen hinzugefügt. Zusätzlich zu den UML-Standardprofilen, beispielsweise für Primitive-Datentypen, stehen Profilerweiterungen hauptsächlich für die strukturelle Definition verschiedener Varianten zur Verfügung. Die wichtigsten Profilerweiterungen sind <vp_entitiy>, <vp_template> und <vp_alternative_template>. Bei einer <vp_entitiy> handelt es sich um ein Plattformmodul, das von einer Klasseninstanz beschrieben wird. Es korreliert mit einem Modul in der Systemsimulation. Ein Plattform-Template (<vp_template>) abstrahiert ein Teilsystem im Hinblick auf Einfachheit, Variabilität oder Strukturierung. Es besteht aus mehreren Plattformmodulen oder Templates, die in einem zusammengesetzten Strukturdiagramm beschrieben sind. Das <vp_alternative_template> gibt Alternativen für bestimmte Plattformkomponenten an. Die alternativen Templates bestehen aus zwei oder mehreren nicht miteinander zusammenhängenden Plattform-Templates oder Modulen. Eine zulässige Plattformvariante muss genau eines davon enthalten.