Die folgenden Beispiele zeigen typische Schwierigkeiten bei der statischen Analyse des C-Codes von eingebetteten Anwendungen auf. Natürlich besteht die Herausforderung vor allem darin, Analysemethoden zu entwickeln, die auf große industrielle Anwendungen anwendbar sind.

Sicherheitskritische und insbesondere synchrone eingebettete Systeme arbeiten mit Tausenden von booleschen Variablen. Naive Analysemethoden führen daher schnell zu einer kombinatori­schen Explosion. Rechenzeit wie Speicherverbrauch können exponentiell steigen.

Dank hochentwickelter Spezialalgorithmen kann Astrée problemlos mit Tausenden von boole­schen Variablen so umgehen, daß sowohl kombinatorische Explosion als auch Fehlalarme ver­mieden werden können.

Ein einfaches Beispiel:

/* boolean.c */
typedef enum {FALSE = 0, TRUE = 1} BOOLEAN;
BOOLEAN B;
void main () {
  unsigned int X, Y;
  while (1) {
    /* ... */
    B = (X == 0);
    /* ... */
    if (!B) {
      Y = 1 / X;
    };
    /* ... */
  };
}

Eine Analyse dieses Programms mit Astrée liefert keine Warnungen, denn aufgrund der Be­ziehung zwischen B und X kann keine Division durch null bei der Ausführung des Programms auftreten. Astrée ist in der Lage, dies automatisch zu erkennen.

Programmen, die komplexe Systeme steuern, liegen mathematische Modelle zugrunde, die auf reellen Zahlen basieren. Computer rechnen allerdings mit Gleitkommazahlen, was zu recht über­raschenden Ergebnissen führen kann.

Betrachten wir die folgenden beiden Programme:

/* float-error.c */
int main () {
    float x, y, z, r;

    x = 1.000000019e+38;
    y = x + 1.0e21;
    z = x - 1.0e21;
    r = y - z;
    printf("%f\n", r);
}
% gcc float-error.c
% ./a.out
0.000000
/* double-error.c */
int main () {
  double x; float y, z, r;
  /* x = ldexp(1.,50)+ldexp(1.,26); */
  x = 1125899973951488.0; 
  y = x + 1;
  z = x - 1;
  r = y - z;
  printf("%f\n", r);
}
% gcc double-error.c
% ./a.out
134217728.000000

Da (x+a)-(x-a) = 2a, möchte man annehmen, daß diese Programme 2.0e21 bzw. 2.0 ausgeben sollten. Aufgrund von Rundungsfehlern ist das allerdings nicht der Fall. Astrée ist in der Lage, das zu erkennen. Es behandelt Rechenoperationen auf Gleitkommazahlen mit abso­luter Präzision und berücksichtigt alle möglichen Rundungsfehler sowie eventuelle kumulative Effekte, die in Programmen auftreten können, die stundenlang ohne Unterbrechung laufen.

Hier ist noch ein Beispiel:

/* float.c */
void main () {
  float x,y,z;
  if ((x < -1.0e38) || (x > 1.0e38)) return;
  while (1) {
    y = x+1.0e21;
    z = x-1.0e21;
    x = y-z;
  }
}

Astrée beweist, daß dieses Programm frei von Laufzeitfehlern ist, wenn es auf 32-Bit-Gleitkommazahlen rechnet.

Betrachten wir das folgende Beispiel:

/* filter.c */
typedef enum {FALSE = 0, TRUE = 1} BOOLEAN;
BOOLEAN INIT;
float P, X;

void filter () {
  static float E[2], S[2];
  if (INIT) {
    S[0] = X;
    P = X;
    E[0] = X;
  } else {
    P = (((((0.5*X)-(E[0]*0.7))+(E[1]*0.4))+(S[0]*1.5))-(S[1]*0.7));
  }
  E[1] = E[0];
  E[0] = X;
  S[1] = S[0];
  S[0] = P;
}

void main () {
  X = 0.2 * X + 5;
  INIT = TRUE;
  while (1) {
    X = 0.9 * X + 35;
    filter ();
    INIT = FALSE;
  }
}

Aufgrund von Gleitkommaberechnungen ist es nicht sofort ersichtlich, daß hier kein Überlauf passiert (genauer gesagt, daß P wie von Astrée berechnet in [-1327.05, 1327.05] liegt). Kommen noch boolesche Variablen oder weitere Filter hinzu, wird die Lage schnell noch unübersichtlicher. Nicht jedoch für Astrée. Es weiß genug über die Regelungstheorie, um Filter mir höchster Präzision analysieren zu können.

Hoch