Wie funktioniert Astrée?

Die folgenden Beispiele zeigen typische Schwierigkeiten bei der statischen Analyse des C-Codes von eingebetteten Anwendungen auf.

In allen Fällen besteht die wichtigste Herausforderung darin, Analysemethoden zu ent­wickeln, die auf große industrielle Anwendungen skaliert werden können. Astrée nimmt Ihnen diese Arbeit ab.

Boolesche Variablen

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.

Rechnen mit Gleitkommazahlen

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.

Astrée behandelt Rechenoperationen auf Gleitkommazahlen mit abso­luter Präzision. Es berück­sichtigt alle möglichen Rundungsfehler. Es erkennt sogar 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;
    /* ...code to initialize x,y,z... */
    if ( (((*((unsigned*)&x) & 0x7f800000) >> 23) != 255 ) /* not NaN */
       && (x >= -1.0e38) && (x <= 1.0e38) ) {
        while (1) {
            y = x+1.0e21;
            z = x-1.0e21;
            x = y-z;
        }}
    else
        return;
}

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

Digitale Filter

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 mit höchster Präzision analysieren zu können.

Weiter