Konzepte zur Absicherung der Variantenkonfiguration von
             eingebetteter Fahrzeugsoftware∗

                                       Hannes Holdschick †
                                          Daimler AG
                                 hannes.holdschick@daimler.com


       Abstract: Eine breite Fahrzeugpalette, spezifische Produktanforderungen aus globa-
       len Märkten und eine Vielzahl softwarebasierter Ausstattungsvarianten führen in der
       Automobilindustrie zu einer immer größeren Produktvielfalt. Um die entstehende Kom-
       plexität beherrschen zu können, wird die Methode des merkmalbasierten Variantenma-
       nagements eingesetzt.
           Der bei der Daimler AG verfolgte Ansatz sieht vor, dass variable Komponenten in
       Entwicklungsartefakten, wie beispielsweise einem Matlab / Simulink-Modell, mithil-
       fe von aussagenlogischen Formeln über Merkmalen konfiguriert werden. Fehler inner-
       halb dieser Konfigurationsformeln bzw. des Merkmalmodells können bei der Konfigu-
       ration zu inkonsistenten Systemvarianten führen. Wir präsentieren daher Konsistenz-
       bedingungen, um die Konfiguration abzusichern. Diese basieren auf SAT-Analysen
       des Merkmalmodells und der Konfigurationsformeln. Erste Implementierungen zei-
       gen, dass die Performanz solcher Analysen auf industriellen Variantenmodellen praxi-
       stauglich ist.


1    Einleitung

In der Automobilindustrie wird das Konzept der Software-Produktlinien [CN01] einge-
setzt, um der steigenden Variantenkomplexität in softwarebasierten Systemen zu begeg-
nen. Erreicht dabei die Variabilität in Entwicklungsartefakten, wie z.B. einem Simulink-
Modell oder einem Anforderungsdokument, eine hinreichende Komplexität, so wird sie
in einem merkmalbasierten Variantenmodell dokumentiert. Darin werden die gemeinsa-
men und unterschiedlichen funktionalen Eigenschaften der System-Varianten in einem
Merkmalmodell [KCH+ 90] festgehalten. Um auch die Konfiguration des Artefaktes zu
ermöglichen, muss zusätzlich das Mapping zwischen Merkmalen und den variablen Be-
standteilen des Artefaktes erstellt werden, welches im sogenannten Konfigurationsmodell
abgebildet wird.
Ist ein Variantenmodell im Einsatz, entwickelt es sich stetig weiter. Dadurch entsteht die
Herausforderung, dessen Konsistenz im Evolutionsprozess zu gewährleisten, welche auch
schon in anderen Arbeiten thematisiert wurde [LSB+ , Hol12]. Als einen Lösungsansatz
   ∗ Copyright c 2014 for the individual papers by the papers’ authors. Copying permitted for private and

academic purposes. This volume is published and copyrighted by its editors.
   † Dieser Beitrag wurde durch das BMBF im Projekt SPES 2020 XT (Förderkennz: 01IS12005) gefördert.


                                                   87
dafür präsentieren wir Analysen des Variantenmodells, um nach einer Änderung prüfen
zu können, ob Inkonsistenzen bzw. Fehlmodellierungen aufgetreten sind. Durch die aus-
sagenlogische Fundierung des Merkmalmodells können diese Konsistenzbedingungen auf
die Frage der Erfüllbarkeit einer aussagenlogischen Formel (SAT) zurückgeführt werden.


2     Beschreibung des Variantenmodells

In diesem Abschnitt wird näher auf die beiden Teilmodelle des Variantenmodells und den
Konfigurationsprozess eingegangen.


2.1    Das Merkmalmodell

Im Merkmalmodell sind die funktionalen Eigenschaften des Systems hierarchisch als Baum
strukturiert [KCH+ 90].
Definition: Sei zunächst M = (M, H ∪ C, r) ein 3-Tupel bestehend aus:

      • einer endlichen Menge M ,
      • der Menge H der hierarchischen Beziehungen:
             H := opt ∪˙ obl ∪˙ alt ∪˙ dis ⊂ M × M ,
      • der Menge C der Cross-Tree-Constraints:
             C := req ∪˙ con ⊂ M × M
      • und einem ausgezeichnetem Wurzelelement r ∈ M

Wir nennen M ein Merkmalmodell, falls gilt:

(M1) Für jedes m ∈ M \ {r} existiert genau ein x ∈ M mit (x, m) ∈ H
(M2) Es existiert kein x ∈ M mit (x, r) ∈ H
(M3) Für jedes x ∈ M existieren x1 , . . . , xn ∈ M mit (r, x1 ), . . . , (xn , x) ∈ H

Mit anderen Worten: Interpretiert man M als Knotenmenge und H als Kantenmenge, so
ist (M, H) ein Baum. Die Relationen in H beschreiben dabei die Variationstypen der
Merkmale. Wir unterscheiden in Anlehnung an bestehende Ansätze [Bat05, CE00] die
folgenden Typen: optional (opt), obligatorisch (obl), alternativ (alt) und disjunktiv (dis).
Ist ein Paar von Merkmalen in einer der Relationen enthalten, so stehen diese in einer
Vater-Kind-Beziehung und das Kindmerkmal hat den entsprechenden Variationstyp. Zum
Beispiel bedeutet (x, y) ∈ opt, dass x das Vatermerkmal des optionalen Merkmals y ist.
Dadurch definiert H eine Hierarchie auf der Menge M der Merkmale.


                                               88
                           Abbildung 1: Beispiel für ein Merkmalmodell


Mithilfe der Cross-Tree-Constraints lassen sich weitere Beziehungen zwischen Merkma-
len definieren. Wir beschränken uns hier auf die beiden Typen requires (req) und conflicts
(con), da sie in der Praxis am häufigsten verwendet werden. In Abb. 1 sieht man ein stark
vereinfachtes Beispiel für ein Merkmalmodell der Fahrerassistenzsysteme (FAS). Entspre-
chend der obigen Definition hat dieses Modell die folgende Struktur:

   • opt = {(FAS, Tempomat), (FAS, Bremsassistent) (Radarsysteme, Nahbereichsra-
     dar), (Radarsysteme, Fernbereichsradar)}
   • obl = {(FAS, Limiter), (FAS, Radarsysteme)}
   • alt = {(Tempomat, einstufiger Tempomathebel),
     (Tempomat, zweistufiger Tempomathebel)}
   • req = {(Bremsassistent, Nahbereichsradar)} bzw. dis = con = ∅

Ausgehend von der obigen Beschreibung des Merkmalmodells lässt sich nun dessen aus-
sagenlogische Repräsentation definieren. Mit F (M ) bezeichnen wir dabei hier und auch
im Weiteren die Menge aller aussagenlogischen Formeln über der Merkmalmenge M .
Definition: Sei M = (M, H ∪ C, r) ein Merkmalmodell mit H = {opt, obl, alt, dis} und
C = {req, con}. Dann bezeichnen wir mit φ(M) ∈ F (M ) die Formel des Merkmalm-
odells M. Sie ist definiert durch:


              def
      φ(M) =        r                                                                         (1)
                           ^
                    ∧               (y → x)                                                   (2)
                        (x,y)∈opt
                           ^
                    ∧               (x ↔ y)                                                   (3)
                        (x,y)∈obl

                                 ^                        k
                                                          _              ^
                    ∧                             ((x ↔         yi ) ∧         ¬(yi ∧ yj ))   (4)
                                 x∈M                      i=1            i<j
                        (x,y1 ),...,(x,yk )∈alt


                                                      89
                                   ^
                      ∧                             (x ↔ (y1 ∨ . . . ∨ yk ))                         (5)
                                   x∈M
                          (x,y1 ),...,(x,yk )∈dis
                             ^
                      ∧               (x → y)                                                        (6)
                          (x,y)∈req
                             ^
                      ∧               (¬x ∨ ¬y)                                                      (7)
                          (x,y)∈con


Die Idee, das Merkmalmodell mithilfe der Aussagenlogik zu formalisieren, wurde bereits
in verschiedenen Arbeiten beschrieben [Bat05, CW07]. Die Struktur der hier dargestellten
Formel ist angelehnt an die Darstellung in [SLB+ 11]. Nach dieser allgemeinen Definition
werfen wir nun einen Blick auf die Formel unseres Beispiel-Merkmalmodells. Sei M das
Merkmalmodell aus Abb. 1. Dann ist

       φ(M) =         F AS                                                                           (8)
                      ∧(T empomat → F AS)                                                            (9)
                      ∧(Bremsassistent → F AS)                                                      (10)
                      ∧(N ahbereichsradar → Radarsysteme)                                           (11)
                      ∧(F ernbereichsradar → Radarsysteme)                                          (12)
                      ∧(F AS ↔ Limiter)                                                             (13)
                      ∧(F AS ↔ Radarsysteme)                                                        (14)
                      ∧(T empomat ↔ (einstuf iger T H ∨ zweistuf iger T H))1                        (15)
                      ∧¬(einstuf iger T H ∧ zweistuf iger T H)                                      (16)
                      ∧(Bremsassistent → N ahbereichsradar)                                         (17)


Wir können nun das Merkmalmodell mithilfe einer aussagenlogischen Formel beschrei-
ben. Ist diese Formel φ(M) erfüllbar, so existiert eine gültige Variante für das Merk-
malmodell M. Genauer gesagt ist jede Belegung, die φ(M) erfüllt, eine gültige Variante
des Merkmalmodells. Dies führt uns zum Begriff der Selektion.
Definition: Sei M = (M, H ∪ C, r) ein Merkmalmodell mit M = {m1 , . . . , mn }. Dann
nennen wir S ∈ F (M ) eine Selektion von M, falls gilt:

       S = s1 ∧ . . . ∧ sn mit si = mi oder si = ¬mi für 1 ≤ i ≤ n.

Eine Selektion S ∈ F (M ) heißt gültig, falls die Formel S ∧ φ(M) ∈ F (M ) erfüllbar ist.
    1 Für eine übersichtlichere Darstellung der Formel haben wir in diesem Beispiel die Namen der Merk-

male einstufiger Tempomathebel“ und zweistufiger Tempomathebel“ durch einstufiger TH“ bzw. zweistu-
       ”                                   ”                                ”                    ”
figer TH“ ersetzt.


                                                         90
                   Abbildung 2: Ausschnitt aus einem Konfigurationsmodell


2.2   Das Konfigurationsmodell

Im Konfigurationsmodell ist der Zusammenhang zwischen Merkmalen und den variablen
Komponenten im Entwicklungsartefakt dokumentiert. Dies kann zum Beispiel ein optio-
nales Subsystem in Simulink oder eine variable Anforderung in einem Lastenheft sein.
Dabei sind für uns vor allem die aussagenlogischen Konfigurationsformeln relevant, die
formal beschreiben, welche Merkmalselektion zu welcher Systemvariante führt.
Definition: Sei M ein Merkmalmodell. Ein zugehöriges Konfigurationsmodell ist eine
endliche Menge von Variationspunkten KM = {V P1 , . . . , V PN }. Dabei besteht jeder
Variationspunkt V P = ((V1 , KF1 ), . . . , (Vp , KFp )) aus einer endlichen Menge von Va-
riationen V1 , . . . , Vp . Jeder Variation Vi ist eine Konfigurationsformel KFi ∈ F (M ) zu-
geordnet. Das Tupel V M = (M, KM ) aus Merkmalmodell und Konfigurationsmodell
nennen wir ein Variantenmodell.
In Abb. 2 sieht man einen beispielhaften Ausschnitt aus einem Konfigurationsmodell zu
dem Merkmalmodell in Abb. 1. Es enthält den Variationspunkt V P1 =VAR Tempomat mit
den Variationen
V1 = (Leermodul, ¬ (T empomat)),
V2 = (T M P H einstuf ig, einstuf iger T empomathebel) und
V3 = (T M P H zweistuf ig, zweistuf iger T empomathebel).
V P1 hat damit vergleichsweise einfache Konfigurationsformeln, da sie jeweils nur aus ei-
nem Literal bestehen. Grundsätzlich sind jedoch Konfigurationsformeln beliebiger Größe
möglich und auch realistisch, wodurch die Komplexität entsteht, die eine manuelle Analy-
se deutlich erschwert bzw. unmöglich macht. V P1 könnte beispielsweise die Modellierung
eines Subsystems in Simulink sein, welches, abhängig von einem Parameter, entweder die
eingehenden Signale ohne Verarbeitung weitergibt (V1 ) oder einen Tempomat mit ein-
bzw. zweistufigem Tempomathebel implementiert (V2 bzw. V3 ).


2.3   Der Konfigurationsprozess

Wie dieser Parameter ermittelt wird, beschreibt der Konfigurationsprozess. Soll dabei ei-
ne neue Systemvariante konfiguriert werden, wählt man dafür zunächst die gewünschten
Merkmale aus und definiert damit eine Selektion. Abhängig von dieser Selektion wird


                                             91
für jeden Variationspunkt einzeln entschieden, welche seiner Variationen in das System
integriert wird.
Definition: Sei dazu V P = ((V1 , KF1 ), . . . , (Vp , KFp )) ∈ KM ein Variationspunkt und
S ∈ F (M ) eine Selektion. Ist dann S ∧ KFi erfüllbar für ein 1 ≤ i ≤ p, so nennen wir
Vi die an dem Variationspunkt V P für die Selektion S gültige Variation. In diesem Fall
wird im weiteren davon die Rede sein, dass die Selektion S die Konfigurationsformel KFi
erfüllt.
Wären für eine Premium-Variante der Fahrerassistenzsysteme z.B. unter anderen die Merk-
male Tempomat und zweistufiger Tempomathebel ausgewählt, so würde der Konfigurati-
onsprozess am Variationspunkt V P1 die Variation 2 als gültig bestimmen. Auf diese Art
und Weise erhält man für jeden Variationspunkt genau eine Variation, welche mithilfe
des bereits erwähnten Parameters codiert wird. Diese Liste an Variationspunkt-Parameter-
Paaren wird anschließend in das Entwicklungsartefakt exportiert (z.B. per xml-Datei), um
die noch offene Variabilität zu binden. In unserem Beispiel würde dabei in das Simulink-
Subsystem die Implementierung des Tempomaten mit zweistufigem Tempomathebel ein-
gefügt werden.
Für den Konfigurationsprozess ist es dabei essentiell, dass für eine gegebene Selektion
S an jedem Variationspunkt genau eine Variation gültig wird. Ist an einem Variations-
punkt diese Eindeutigkeit nicht gegeben, so kann dessen Parameter gar nicht oder ggf. nur
falsch ermittelt werden. Die Folge davon ist ein inkonsistentes bzw. falsch konfiguriertes
Artefakt. Im nächsten Abschnitt werden Konsistenzbedingungen beschrieben, die solche
Fehlkonfigurationen verhindern können.


3     Definition der Konsistenzbedingungen

In diesem Abschnitt werden Konsistenzbedingungen für das Variantenmodell vorgestellt.
Diese beziehen sich vor allem auf die Konfigurationsformeln, da diese in der Regel händisch
eingegeben werden, wodurch es leicht zu Fehlern kommen kann. Außerdem wird auch die
Formalisierung des Merkmalmodells einbezogen, womit eine Analyse aller theoretisch
möglichen (also gültigen) Selektionen sichergestellt werden kann. Somit können nicht nur
die bestehenden, sondern auch zukünftige Varianten abgesichert werden. In den folgen-
den Unterabschnitten wird jeweils die Konsistenzbedingung zuerst formuliert (Bedingung)
und danach kurz erklärt (Beschreibung). Anschließend wird dargestellt, wie die Bedingung
mithilfe der Aussagenlogik geprüft wird (Prüfung) und schlussendlich ein Beispielmodell
angegeben, welches die Bedingung verletzt (Gegenbeispiel).


3.1   KB 1: Kontradiktionen in Konfigurationsformeln

Bedingung: Keine Konfigurationsformel steht im Widerspruch zu der Modellierung im
Merkmalmodell.


                                            92
                       Abbildung 3: inkonsistentes Konfigurationsmodell


Beschreibung: Jede Konfigurationsformel muss auch unter den Bedingungen des Merk-
malmodells erfüllbar sein. Andernfalls wird die betroffene Konfigurationsformel von kei-
ner gültigen Selektion erfüllt. Dadurch ist die zugehörige Variation nie Teil einer System-
variante und damit überflüssig.
Prüfung: Bei dieser Konsistenzbedingung wird für jede Konfigurationsformel KF im
Konfigurationsmodell einzeln geprüft, ob der folgende Ausdruck erfüllbar ist:

      φ(M) ∧ KF                                                                           (18)

Ist diese Formel nicht erfüllbar, gibt es also keine Belegung die φ(M) und KF erfüllt, so
existiert keine gültige Selektion, die die Konfigurationsformel KF erfüllt. Sie steht somit
im Widerspruch zum Merkmalmodell.
Gegenbeispiel: Betrachten wir das Variantenmodell, welches aus dem Merkmalmodell
der Fahrerassistenzsysteme von oben und dem Konfigurationsmodell in Abb. 3 besteht.
Hier verletzt der Variationspunkt VAR VP 1 die beschriebene Konsistenzbedingung. Die
Konfigurationsformel von Variation 2 wird bei einer gültigen Selektion immer zu false
evaluieren, da die Merkmale einstufiger Tempomathebel und zweistufiger Tempomathebel
im Merkmalmodell als Alternativen modelliert sind und somit nicht beide Merkmale in
einer Selektion ausgewählt werden dürfen.


3.2    KB 2: Tautologien in Konfigurationsformeln

Bedingung: Keine Konfigurationsformel wird von allen gültigen Selektionen erfüllt.
Beschreibung: Diese Konsistenzbedingung soll verhindern, dass man eine Konfigurati-
onsformeln formuliert, die von jeder gültigen Selektion S ∈ F (M ) erfüllt wird, die also
eine Tautologie bzgl. der Merkmalmodellierung ist.
Prüfung: Bei dieser Konsistenzbedingung wird für jede Konfigurationsformel KF im
Konfigurationsmodell einzeln geprüft, ob der folgende Ausdruck erfüllbar ist:

      φ(M) ∧ (¬KF )                                                                       (19)

Ist diese Formel nicht erfüllbar, so existiert für die Konfigurationsformel KF keine gültige


                                              93
Selektion, die ihre Negation erfüllt. Somit wird diese Formel von jeder gültigen Selektion
erfüllt, ist also eine Tautologie im Bezug auf die Merkmalmodellierung.
Gegenbeispiel: Betrachten wir wieder das Variantenmodell, welches aus dem Merkmalm-
odell der Fahrerassistenzsysteme von oben und dem Konfigurationsmodell in Abb. 3 be-
steht. Hier verletzt der Variationspunkt VAR VP 2 die beschriebene Konsistenzbedingung.
Die Konfigurationsformel von Variation 1 wird von jeder gültigen Selektion erfüllt, da das
Merkmal Limiter obligatorisch ist und daher in jeder gültigen Merkmalauswahl selektiert
werden muss. Damit ist diese Konfigurationsformel eine Tautologie bzgl. des Merkmalm-
odells.


3.3    KB 3: unterbestimmte Variationspunkte

Bedingung: An jedem Variationspunkt muss für jede gültige Selektion mindestens eine
Konfigurationsformel erfüllt sein.
Beschreibung: Wie bereits in Abschnitt 2 beschrieben, ist im Konfigurationsprozess wich-
tig, dass von einer gültigen Selektion genau eine Konfigurationsformel je Variationspunkt
erfüllt wird. Diese und die nächste Konsistenzbedingung stellen diese Eindeutigkeit sicher.
Prüfung: Jeder Variationspunkt wird bei dieser Bedingung einzeln geprüft. Die Bedin-
gung ist für den Variationspunkt V P = ((V1 , KF1 ), . . . , (Vp , KFp )) ∈ KM verletzt,
falls die folgende Formel aus F (M ) erfüllbar ist:
               p
               ^
      φ(M) ∧        (¬KFi )                                                               (20)
               i=1


Denn dann existiert eine Selektion S ∈ F (M ), die φ(M) und
      p
      ^
          (¬KFi )                                                                         (21)
      i=1


erfüllt. S ist somit gültig und erfüllt ¬KFi für alle 1 ≤ i ≤ p. Diese gültige Selektion S
erfüllt damit keine Konfigurationsformel an dem Variationspunkt V P ∈ KM .
Gegenbeispiel: Betrachten wir das Variantenmodell, welches aus dem Merkmalmodell
der Fahrerassistenzsysteme von oben und dem Konfigurationsmodell in Abb. 4 besteht.
Hier verletzt der Variationspunkt VAR VP 3 die beschriebene Konsistenzbedingung. Das
Merkmal Tempomat ist im Merkmalmodell optional, kann damit an- und abgewählt wer-
den. Beide Konfigurationsformeln werden jedoch nur von Selektionen erfüllt, in denen die-
ses Merkmal ausgewählt wurde. Dadurch kann für eine Fahrzeugvariante ohne Tempomat
für diesen Variationspunkt keine Variation ermittelt werden, wodurch die Konfiguration
fehlschlägt.


                                              94
                                Abbildung 4: inkonsistentes Konfigurationsmodell


3.4    KB 4: überbestimmte Variationspunkte

Bedingung: An jedem Variationspunkt darf für jede gültige Selektion höchstens eine Kon-
figurationsformel erfüllt sein.
Beschreibung: Ergänzend zur vorherigen Konsistenzbedingung werden hier Variations-
punkte gesucht, an denen für eine bestimmte Selektion mehr als eine Konfigurationsfor-
mel erfüllt werden. In diesem Fall könnte keine gültige Variation an dem Variationspunkt
ermittelt werden, wodurch im Konfigurationsprozess eine fehlerhafte Systemvariante ent-
steht.
Prüfung: Jeder Variationspunkt wird bei dieser Bedingung einzeln geprüft. Die Konsis-
tenzbedingung ist für den Variationspunkt V P = ((V1 , KF1 ), . . . , (Vp , KFp )) ∈ KM
verletzt, falls die folgende Formel erfüllbar ist:
                   _
      φ(M) ∧ (           (KFi ∧ KFj ))                                                  (22)
                   i<j


Begründung: Ist der obige Ausdruck erfüllbar, so existiert eine Selektion S ∈ F (M ),
sodass die Formel
                  _
    S ∧ φ(M) ∧ ( (KFi ∧ KFj ))                                                     (23)
                          i<j


erfüllbar ist. Damit ist insbesondere auch S ∧ φ(M) erfüllbar, woraus folgt, dass S eine
gültige Selektion ist. Darüber hinaus ist außerdem damit auch
            _
      S∧(         (KFi ∧ KFj ))                                                         (24)
            i<j


erfüllbar. Daraus folgt, dass mindestens ein Paar von Indizes 1 ≤ i, j ≤ p existiert, sodass
S∧KFi ∧KFj erfüllbar ist. Das bedeutet, dass die gültige Selektion S die beiden Konfigu-
rationsformeln KFi und KFj erfüllt. Die oben genannte Inkonsistenz liegt damit an dem
untersuchten Variationspunkt vor, da zwei verschiedene Konfigurationsformeln existieren,
die von einer gültigen Selektion erfüllt werden.


                                                      95
                             Tabelle 1: Laufzeiten des Prototyps
             Modell             KB1            KB2            KB3          KB4
        Variantenmodell 1    0,143 Sek.     0,143 Sek.     0,133 Sek.   0,145 Sek.
        Variantenmodell 2    0,146 Sek.     0,147 Sek.     0,143 Sek.   0,155 Sek.


Gegenbeispiel: Betrachten wir wieder das Variantenmodell, welches aus dem Merkmalm-
odell der Fahrerassistenzsysteme von oben und dem Konfigurationsmodell in Abb. 4 be-
steht. Hier verletzt der Variationspunkt VAR VP 4 die beschriebene Konsistenzbedingung.
Da es durchaus möglich ist, eine gültige Selektion mit den Merkmalen Tempomat und
einstufiger Tempomathebel zu definieren, würden in diesem Fall beide Konfigurationsfor-
meln von dieser Selektion erfüllt werden. Für diesen Variationspunkt könnte damit keine
eindeutige Variation ermittelt werden, wodurch die Konfiguration fehlschlägt.


4   Prototypische Implementierung und Evaluation

Um die beschriebenen Konsistenzbedingungen auch an bestehenden Variantenmodellen
prüfen zu können, ist eine prototypische Implementierung entstanden. Dadurch kann ein
beliebiges Modell analysiert und im Fehlerfall der betroffene Variationspunkt bzw. die
betroffene Konfigurationsformel angegeben werden. Die Analysen wurden an zwei Vari-
antenmodellen durchgeführt, welche in der industriellen Praxis entstanden sind. Varian-
tenmodell 1 besteht aus einem Merkmalmodell mit 298 Merkmalen und 367 Cross-Tree-
Constraints und einem Konfigurationsmodell mit 164 Variationspunkten und insgesamt
429 Variationen und demnach ebenso vielen Konfigurationsformeln. Die Größe des Mo-
dells liegt damit in einem Bereich, der für Domänen wie Motorsteuerung, Fahrerassistenz
oder e-Drive üblich ist. Das zweite Variantenmodell befindet sich noch in der Entwicklung
und ist daher etwas kleiner: 94 Merkmale, 43 Cross-Tree-Constraints, 14 Variationspunkte
mit 36 Variationen.
Tabelle 1 zeigt die Zeit, die der SAT-Solver im Durchschnitt benötigt, um eine Anfra-
ge zu bearbeiten. Da bei KB1 bzw. KB2 jede Konfigurationsformel einzeln analysiert
wird, müssen bei unserem ersten Beispielmodell 429 Analysen durchgeführt werden. Die
Prüfung des gesamten Modells benötigt daher 429 x 0,143 Sek. ≈ 61,3 Sekunden. Bei KB3
und KB4 wird dagegen nur für jeden Variationspunkt eine SAT-Analyse durchgeführt, wo-
durch sich die Laufzeit verringert. Mit durchschnittlich ca. 0.14 Sekunden sind die Lauf-
zeiten des Solvers für uns zufriedenstellend, zumal auch nach zahlreichen Durchläufen
keine Analyse länger als eine halbe Sekunde dauerte. Alle Laufzeiten wurden dabei auf
einem Windows 7-PC mit 2,53 GHz und 4 GB RAM gemessen.


                                             96
5   Verwandte Arbeiten

Auch andere Arbeiten beschäftigen sich mit dem Mapping zwischen Merkmalen und
Komponenten. Reiser et al. präsentieren einen Ansatz für das Variantenmanagement hier-
archischer komponentenbasierter Systeme [RKW09]. Dabei beschreiben Merkmalmodel-
le die Variabilität der jeweiligen Hierarchieebene, wobei mit sogenannten configuration
links Konfigurationsinformationen zwischen den Modellen ausgetauscht werden können.
Obwohl sich auch unsere Modellierung auf variable Komponenten bezieht, liegt der Un-
terschied darin, dass das gesamte System in einem Variantenmodell (und damit einem
Merkmalmodell) abgebildet wird, auf das sich die vorgestellten Konsistenzbedingungen
beziehen. In [MRM+ 12] wird ein mengentheoretischer Formalismus vorgestellt, um ein
Tracing zwischen Merkmalen (Spezifikation) und Komponenten (Implementierung) zu be-
schreiben. Während in deren Mapping ein Merkmal stets von einer oder mehreren Teil-
mengen von Komponenten implementiert werden kann, wird bei uns der Zusammenhang
mithilfe einer booleschen Formel ausgedrückt. Diese kann beliebig komplex sein, sodass
eine Komponente (in unserem Fall eine Variation) von mehreren Merkmalen abhängen
kann oder z.B. in das System integriert wird, sobald ein Merkmal oder eine Kombination
von Merkmalen nicht ausgewählt wird.
Ein ähnlicher Ansatz wird in [MHP+ 07] verfolgt. Hier wird zwischen Produktlinien- und
Softwarevariabilität unterschieden und eine separate Modellierung mit OVM- bzw. Merk-
malmodellen vorgeschlagen. Auf einer formalisierten Beschreibung dieser Modelle und
deren Beziehungen können anschließend Analysen automatisch ausgeführt werden. Teile
dieser Analysen (z.B. nicht realisierbare Merkmalselektionen) können auf unsere Art der
Modellierung übertragen werden. Der Großteil ist dagegen für uns in diesem Beitrag nicht
relevant (z.B. fehlende Eindeutigkeit zwischen Produktlinien- und Softwarevariabilität,
ungenutzte Merkmale), da sie keine direkte Gefährdung für den Konfigurationsprozess
darstellen. Insgesamt zielen die vorgestellten Analysen eher darauf ab, ob die Architektur
der Produktlinie flexibel genug ist, um die geplanten Produkte zu konfigurieren, wohinge-
gen wir uns in diesem Paper auf Fehler in der Aussagenlogik der Konfigurationsformeln
konzentrieren, um den Konfigurationsprozess an sich abzusichern.
Thaker et al. beschreiben einen Mechanismus für die safe composition of product lines“
                                                    ”
[TBKC07]. Auch dort werden SAT-Analysen vorgestellt, um zu prüfen, ob gültige Merk-
malselektionen zu inkonsistenten Systemvarianten führen können. Während wir auf In-
konsistenzen innerhalb des Variantenmodells eingehen, werden dort Constraints beschrie-
ben, die sich aus der Zusammensetzung von feature modules“, also aus der Produktlinie
                                           ”
selbst, ergeben.


6   Zusammenfassung

Die vorgestellten Analysen sollen sicherstellen, dass der Konfigurationsprozess fehlerfrei
abläuft, damit eine gültige Merkmalselektion stets zu einer validen Systemvariante führt.
Mit den Konfigurationsformeln stehen dabei gerade die Modellelemente im Fokus, die oft


                                            97
händisch erstellt werden und daher eine potentielle Fehlerquelle darstellen. Die manuelle
Prüfung der beschriebenen Bedingungen ist vor allem bei Modellen üblicher Größe nur mit
sehr viel Aufwand oder gar nicht möglich. Da unser Prototyp die Analysen in angemesse-
ner Zeit ausführen kann, stellt er eine große Unterstützung für den Entwicklungsprozess
des Variantenmodells dar.


Literatur

[Bat05]     Don Batory. Feature models, grammars, and propositional formulas. In Proceedings
            of the 9th international conference on Software Product Lines. Springer-Verlag, 2005.
[CE00]      Krzysztof Czarnecki und Ulrich Eisenecker. Generative Programming: Methods,
            Tools, and Applications. Addison-Wesley, Reading, MA, USA, 2000.
[CN01]      Paul C. Clements und Linda Northrop. Software Product Lines: Practices and Patterns.
            SEI Series in Software Engineering. Addison-Wesley, August 2001.
[CW07]      Krzysztof Czarnecki und Andrzej Wasowski. Feature diagrams and logics: There and
            back again. In Software Product Line Conference, 2007. SPLC 2007. 11th Internatio-
            nal, Seiten 23–34. IEEE, 2007.
[Hol12]     Hannes Holdschick. Challenges in the Evolution of Model-Based Software Product
            Lines in the Automotive Domain. In Proceedings of the 4th International Workshop on
            Feature-Oriented Software Development, FOSD ’12. ACM, 2012.
[KCH+ 90] K. C. Kang, S. G. Cohen, J. A. Hess, W. E. Novak und A. S. Peterson. Feature-Oriented
          Domain Analysis (FODA) Feasibility Study. Bericht, Carnegie-Mellon University
          Software Engineering Institute, November 1990.
[LSB+ ]     Rafael Lotufo, Steven She, Thorsten Berger, Krzysztof Czarnecki und Andrzej Wa-
            sowski. Evolution of the linux kernel variability model. In Proceedings of the 14th
            international conference on Software product lines: going beyond, SPLC 2010.
[MHP+ 07] Andreas Metzger, Patrick Heymans, Klaus Pohl, Pierre-Yves Schobbens und Germain
          Saval. Disambiguating the Documentation of Variability in Software Product Lines: A
          Separation of Concerns, Formalization and Automated Analysis. In RE. IEEE, 2007.
[MRM+ 12] Swarup Mohalik, S Ramesh, Jean-Vivien Millo, Shankara Narayanan Krishna und Ga-
          nesh Khandu Narwane. Tracing SPLs precisely and efficiently. In Proceedings of the
          16th International Software Product Line Conference-Volume 1. ACM, 2012.
[RKW09]     M-O Reiser, Ramin Tavakoli Kolagari und Matthias Weber. Compositional variability-
            concepts and patterns. In HICSS’09. 42nd Hawaii International Conference on System
            Sciences. IEEE, 2009.
[SLB+ 11]   Steven She, Rafael Lotufo, Thorsten Berger, Andrzej Wasowski und Krzysztof Czar-
            necki. Reverse engineering feature models. In Richard N. Taylor, Harald Gall und
            Nenad Medvidovic, Hrsg., Proceedings of the 33rd International Conference on Soft-
            ware Engineering, ICSE 2011, Waikiki, Honolulu, HI, USA, May 21-28, 2011, Seiten
            461–470. ACM, 2011.
[TBKC07]    Sahil Thaker, Don Batory, David Kitchin und William Cook. Safe composition of
            product lines. In Proceedings of the 6th international conference on Generative pro-
            gramming and component engineering, Seiten 95–104. ACM, 2007.


                                              98