Astree: Nachweis der Abwesenheit von Laufzeitfehlern
D. Kästner, C. Ferdinand, S. Wilhelm, S. Nenova, O. Honcharova, A. Miné, X. Rival, L. Mauborgne, E. Sims, J. Feret, P. Cousot, R. Cousot
Niveau: Secondaire, Lycée, Terminale Astree: Nachweis der Abwesenheit von Laufzeitfehlern Daniel Kastner1, Christian Ferdinand1, Stephan Wilhelm1, Stefana Nenova1, Olha Honcharova1, Patrick Cousot2, Radhia Cousot2, Jerome Feret2, Laurent Mauborgne2, Antoine Mine2, Xavier Rival2, Elodie-Jane Sims2 1 AbsInt GmbH, Saarbrucken, Germany 2 Ecole Normale Superieure, Paris, France 05.06.2009 Kurzzusammenfassung Sicherheitskritische eingebettete Systeme mussen ho- hen Qualitatsanforderungen genugen. Laufzeitfehler, z.B. arithmetische Uberlaufe oder Rundungsfehler konnen zu fehlerhaftem Programmverhalten fuhren. Da in der Regel keine vollstandige Testabdeckung moglich ist, bieten sich statische Analysatoren an. Diese bieten eine vollstandige Coverage, konnen je- doch Fehlalarme erzeugen. Da jeder potentielle Lauf- zeitfehler manuell vom Benutzer uberpruft werden muss, kann eine hohe Zahl von Fehlalarmen dazu fuhren, dass echte Fehler ubersehen werden. Der sta- tische Analysator Astree kann durch Spezialisierung und Parametrisierung an die zu analysierende Softwa- re angepasst werden. Dies ermoglicht kurze Analyse- zeiten und eine niedrige Zahl von Fehlalarmen. Astree wird z.B. bei der Zertifizierung von industrieller Flug- zeugsteuerungssoftware eingesetzt. Schlusselworter Softwarevalidierung, Laufzeitfehler, statische Analyse. 1 Einfuhrung Die Test- und Validierungsphase stellt einen erheb- lichen Kostenfaktor bei der Entwicklung sicherheits- kritischer Systeme dar. Unentdeckte Fehler konnen schwere Schaden verursachen. Daher stellt sich die Frage, wie mit vertretbarem Aufwand das korrek- te Funktionieren der Software nachgewiesen werden kann.
- auf
- ein wichtiges
- nachweis der
- die jeweilige
- abwesenheit von
- laufzeitfeh- ler das
- compileroptmierungen zu
- und berucksichtigt
- astree