Verifying non-functional real-time properties by static analysis

International audienceStatic analyzers based on abstract interpretation are tools aiming at the automatic detection of run-time properties by analyzing the source, assembly or binary code of a program. From Airbus' point of view, the first interesting properties covered by static analyzers available on the market, or as prototypes coming from research, are absence of run-time errors, maximum stack usage and Worst-Case Execution Time (WCET). This paper will focus on the two latter