Startseite > Automotive > Neue Plattformvarianten-Spezifikation für die Systemverifikation

Systemvariabilität bewältigen

Neue Plattformvarianten-Spezifikation für die Systemverifikation

2. Mai 2016, 9:42 Uhr | Von Andreas Burger, Sebastian Reiter, Alexander Viehl, Oliver Bringmann und Wolfgang Rosenstiel

▶ Diesen Artikel anhören

Fortsetzung des Artikels von Teil 1

Constraint-Formalisierung und -Auflösung

Nachdem der Anwender die strukturellen und parametrischen Constraints spezifiziert hat, werden diese als SMT/SAT-Ausdrücke formalisiert und mit einem SMT/SAT-Solver die zulässigen Systemvarianten ermittelt. Der SMT/SAT-Solver berechnet die gültigen Lösungen inkrementell. Ist eine zulässige Systeminstanz identifiziert, wird diese aus dem Variantenraum herausgenommen. Anschließend arbeitet der SMT/SAT-Solver weiter, bis alle zulässigen Instanzen ermittelt sind. Die folgende Regel zeigt exemplarisch die Formalisierung eines OVCL-Constraint zu einem SMT/SAT-Ausdruck. Ein Bitvektor drückt das <vp_alternative_template> aus, wobei die Vektorbreite gleich der Zahl der unabhängigen Alternativen innerhalb des Template ist. Die Funktion conv() bildet eine natürliche Zahl auf einen Bitvektor ab.

$c o n v thin space colon space N space rightwards arrow B to the power of n space m i t space N equals left square bracket 0 comma 2 to the power of n minus 1 end exponent right square bracket space space u n d space space c o n v left parenthesis <a href=$ stack b with rightwards arrow on top right parenthesis colon space begin inline style sum from i equals 0 to i equals 1 of end style space sum b subscript i 2 to the power of i with blank on top" align="middle" src="https://wor.wfmdev.de/js/ckeditor/plugins/ckeditor_wiris/integration/showimage.php?formula=a8f47c30ca3b5801a36aa4f0b90446df" />

Jobangebote+ passend zum Thema

Regional Key Account (m/w/d) für Elektronische Bauteile

KOA Europe GmbH, Dägeling

Alle Jobangebote im Elektroniknet Karrierebereich anzeigen

Regel 1.1: Die Menge VT enthält alle <vp_template> und <vp_alternative_template> einer Variantenspezifikation MVM. Die Abbildung des Template

$T space element of space V subscript T$

auf quantorenfreie Bitvektor-Logik lässt sich wie folgt ausdrücken:

$T identical to space rightwards arrow for X of element of space B to the power of b w end exponent$

wobei die Vektorbreite bw den unabhängigen Alternativen G des Templates T entspricht. Das impliziert, dass

$b w space equals space open vertical bar G close vertical bar u n d space c o n v space left parenthesis open vertical bar G close vertical bar plus 1 greater than x with rightwards arrow on top greater or equal than space c o n v space left parenthesis 0 right parenthesis$

Eine Varianten-Alternative wird ausgewählt, wenn das zugehörige Bit gesetzt ist. Auf die Auswahl der Alternativen kann in einem Constraint durch den active()-Operator Bezug genommen werden. Der active()-Operator dient zum Spezifizieren von Constraints abhängig von der Template/Modul-Auswahl in der generierten Plattformvariante. Zum Beispiel stellt Exclusive_Constraint1 in Bild 3 sicher, dass bei der Auswahl von netBlckApp im Template altCCEvalNetBlckApp0 in der zweiten Instanz (altCCEvalNetBlckApp1) die Auswahl von cCEvalApp erfolgt. Ähnlich der Template-Auswahl gibt es auch Regeln für die Abbildung von Parameterbelegungen, beschränkten Parametern oder Wahrscheinlichkeitsverteilungen auf quantorenfreie Bitvektor-Logik. Nach erfolgter Transformation werden alle Constraints als SMT-Instanz kodiert und vom Z3-Solver [3] aufgelöst. Der Solver gibt die Belegung der Bitvektoren in Bezug auf die spezifizierten Constraints aus. In einem abschließenden Schritt werden die Bitvektoren erneut auf die Parameterwerte oder Template-Instanzen abgebildet.

Soll die Struktur der generierten Plattform dynamisch geändert werden, müssen die Modulverknüpfungen angepasst werden. Die Template-Verknüpfung erfolgt, sobald der SMT-Solver eine Lösung erzeugt. Diese Lösung gibt die Anzahl der neu generierten Modul/Template-Instanzen der Plattform an. Anschließend erfolgt die Verbindung der Instanzen gemäß bestimmten Verknüpfungsregeln, die wiederum auf Template Constraints, UML-Port-Kardinalitäten und UML-Konnektoren basieren. Jede neu generierte Modul/Template-Instanz einer Plattform kann mit den jeweiligen Modulen/Templates der Zielplattform verknüpft werden, solange die Kardinalität des Ziels dabei nicht überschritten wird. Wird die Kardinalität des Ziels überschritten, so wird die neu generierte Modul/Template-Instanz der Plattform mit der zuvor generierten Instanz desselben Typs verbunden. Plattform-Module/Templates, die von Constraints als variabel spezifiziert sind, dürfen ausschließlich mit nichtvariablen Plattform-Modulen und -Templates verbunden werden. Das bedeutet, dass jede über Template-Grenzen hinausreichende Variabilität in einem Template zusammengefasst werden muss.

Bild 2 demonstriert den Verknüpfungsprozess für zwei Beispiele gemäß den oben definierten Verknüpfungsbedingungen. In beiden Fällen muss das Template T1 dreimal in die finale Plattformvariante integriert werden. Das lässt sich mit dem Constraint

Bag {3}"includes(self.allInstances()" size())

erzwingen. Hierbei referenziert self T1. Außerdem ist T1 mit den Zielplattform-Modulen/Templates S1 und S2 verbunden. Im Beispiel der Ringtopologie hat die Target-Port-Instanz von Konnektor C2 die Kardinalität 1. Deshalb muss jede neu generierte Instanz von T1 mit der nächsten neu generierten Instanz verbunden werden. Die Bustopologie wird generiert, weil die Kardinalität des Konnektors C1 des Target-Ports bei S1 unbegrenzt ist [1..*]. Somit wird jede neu generierte Instanz von T1 mit S1 verbunden.