Validation of assembler programs for DSPs: a static analyzer

Digital Signal Processors are widely used in critical embedded systems to pilot low-level, often critical functionalities. We describe a static analyzer based on abstract interpretation and designed to validate industrial assembler programs for a DSP. The validation consists of guaranteeing the absence of runtime errors such as incorrect memory accesses and of tracking the sources of inaccuracies introduced by floating-point computations. Our first contribution is a new static analysis for relocatable assembler programs able to cope with dynamically computed branching addresses. Our second contribution is the analyzer itself and its graphical interface which helps the user to understand the numerical inaccuracies. Categories and Subject Descriptors D.2.4 [Software Engineering]: Program Verification—Formal methods, Validation; F.3.1 [Logics and meanings of Programs]: Specifying and Verifying and Reasoning about

• Type: Conference
• Year: 2004
• Where: PASTE
• Authors: Matthieu Martel
• Keywords: Assembler Programs, Critical Embedded Systems, Industrial Assembler Programs, PASTE 2004