Astrée: Nachweis der Abwesenheit von Laufzeitfehlern.
In Workshop ``Entwicklung zuverlässiger Software-Systeme'', Regensburg, Germany, June 18th, 2009.
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.
Abstract Interpretation, Static analysis, Runtime error, Embedded software, Aynchronous control/command software.
\bibitem{KastnerEtAl-09}
D.~K\"astner, C.~Ferdinand, S.~Wilhelm, S.~Nevona, O.~Honcharova,
P.~Cousot, R.~Cousot, J.~Feret, L.~Mauborgne, A.~Min\'e,
X.~Rival, and \'E.-J.~Sims.
\newblock \textsc{Astr\'ee}: Nachweis der Abwesenheit von Laufzeitfehlern.
\newblock In \emph{Workshop ``Entwicklung zuverl\"assiger Software-Systeme''}, Regensburg, German,
18 June 2009.
@InProceedings{KastnerEtAl-09,
author = {D.~K\"astner and C.~Ferdinand and S.~Wilhelm and S.~Nevona and O.~Honcharova and
P.~Cousot and R.~Cousot and J.~Feret and L.~Mauborgne and A.~Min\'e and
X.~Rival and \'E.-J.~Sims},
title = {\textsc{Astr\'ee}: Nachweis der Abwesenheit von Laufzeitfehlern},
booktitle = {Workshop ``Entwicklung zuverl\"assiger Software-Systeme''},
address = {Regensburg, Germany},
month = {18 June},
year = 2009,
}