Validation of assembler programs for DSPs: a static analyzer

10 years 8 months ago
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
Matthieu Martel
Added 30 Jun 2010
Updated 30 Jun 2010
Type Conference
Year 2004
Authors Matthieu Martel
Comments (0)