Astrée: Nachweis der Abwesenheit von Laufzeitfehlern.

Résumé : Sicherheitskritische eingebettete Systeme müssen hohen Qualitätsanforderungen genügen. Laufzeitfehler, z.B. arithmetische Überläufe oder Rundungsfehler können zu fehlerhaftem Programmverhalten führen. Da in der Regel keine vollständige Testabdeckung möglich ist, bieten sich statische Analysatoren an. Diese bieten eine vollständige Coverage, können jedoch Fehlalarme erzeugen. Da jeder potentielle Laufzeitfehler manuell vom Benutzer überprüft werden muss, kann eine hohe Zahl von Fehlalarmen dazu führen, dass echte Fehler übersehen werden. Der statische Analysator Astrée kann durch Spezialisierung und Parametrisierung an die zu analysierende Software angepasst werden. Dies ermöglicht kurze Analysezeiten und eine niedrige Zahl von Fehlalarmen. Astrée wird z.B. bei der Zertifizierung von industrieller Flugzeugsteuerungssoftware eingesetzt. Safety-critical embedded software has to satisfy stringent quality.
Type de document :
Communication dans un congrès
Workshop "Entwicklung zuverlässiger Software-Systeme", Jun 2009, Regensburg, Germany. 2009
Liste complète des métadonnées

https://hal.inria.fr/hal-00753732
Contributeur : Jérôme Feret <>
Soumis le : lundi 19 novembre 2012 - 15:35:46
Dernière modification le : vendredi 25 mai 2018 - 12:02:05

Identifiants

  • HAL Id : hal-00753732, version 1

Collections

Citation

Daniel Kästner, Christian Ferdinand, Steplan Wilhelm, Stefana Nenova, Olha Honcharova, et al.. Astrée: Nachweis der Abwesenheit von Laufzeitfehlern.. Workshop "Entwicklung zuverlässiger Software-Systeme", Jun 2009, Regensburg, Germany. 2009. 〈hal-00753732〉

Partager

Métriques

Consultations de la notice

361