Reliable and Precise WCET and Stack Size Determination for a Real-life Embedded Application
Résumé
Failure of a safety-critical application on an embedded processor can
lead to severe damage or even loss of life. Here we are concerned with two kinds
of failure: stack overflow, which usually leads to run-time errors that are difficult
to diagnose, and failure to meet deadlines, which is catastrophic for systems
with hard real-time characteristics. Classical software validation methods like
simulation and testing with debugging require a lot of effort, are expensive, and
do not really help in proving the absence of such errors.
AbsInt's tools StackAnalyzer and aiT (timing analyzer) provide a solution to
these problems. They use abstract interpretation as a formal method that leads
to statements valid for all program runs. Both tools have been used successfully
at Hispano-Suiza to analyze applications running on a Motorola PowerPC
MPC555. They turned out to be well-suited for analyzing large safety-critical
applications developed at Hispano-Suiza. They can be used either during the
development phase providing information about stack usage and runtime behavior
well in advance of any run of the analyzed application, or during the
validation phase for acceptance tests prior to the certification review.