Abstract:
Formal methods are increasingly used to help ensuring the
correctness of complex, critical embedded software systems.
We show how sound semantic static analyses based on Abstract Interpretation
may be used to check properties at various levels of a software design: from
high level models to low level binary code. After a short introduction to the
Abstract Interpretation theory, we present a few current applications:
checking for run-time errors at the C level, translation validation from C to assembly, and analyzing SAO models of
communicating synchronous systems with imperfect clocks.
We conclude by briefly proposing some requirements to apply Abstract Interpretation to modeling languages such as UML.
\bibitem[BCC{\etalchar{+}}09a]{bccfmmr11}
Julien Bertrane, Patrick Cousot, Radhia Cousot, Laurent~Mauborgne
J{\'e}r{\^o}me~Feret, Antoine Min{\'e}, and X.~Rival.
\newblock Static analysis by abstract interpretation of embedded critical
software.
\newblock {\em Software Engineering Notes}, 36(1):1--8, January 2011.
@article{bccfmmr11,
author = "Julien Bertrane and Patrick Cousot and Radhia Cousot and
J{\'e}r{\^o}me Feret, Laurent Mauborgne and Antoine Min{\'e} and X. Rival",
title = "Static Analysis by Abstract Interpretation of Embedded Critical
Software",
journal = "Software Engineering Notes",
volume = 36,
number = 1,
year = 2011,
month = "January",
publisher = "ACM",
pages = "1--8"
}