Detecting and proving the absence of run-time errors
Abstract interpretation is a formal methods technique that relies on a broad base of mathematical theorems that define rules for analyzing complex dynamic systems, such as software applications. Instead of analyzing each state of a program, abstract interpretation represents these states in a more general form and provides rules to manipulate them. It produces a mathematical abstraction and also interprets the abstraction.
To produce a mathematical abstraction of program states, abstract interpretation thoroughly analyzes all code variables. When combined with non-exponential algorithms and today's increased processing power, it helps to address complex embedded software verification and testing challenges.
You can use abstract interpretation with static code analysis to accomplish the following tasks:
- Perform code verification to identify and diagnose run-time errors
- Use metrics produced by this process to measure and improve software quality
- Verify completely and comprehensively all risky operations, getting a diagnostic of “proven,” “fail,” “unreachable,” or “unproven” for each operation
Combining abstract interpretation and static code analysis enables you to:
- Detect elusive run-time errors
- Prove the absence of certain run-time errors
- Produce code quality metrics
- Check source code for compliance to code standards such as MISRA C and JSF++
For details, see Polyspace® products.
Examples and How To
See also: static analysis with Polyspace products, verification, validation, and test, embedded systems, abstract interpretation, code review, cyclomatic complexity, formal methods, software metrics, software QA, software quality objectives, source code analysis, static code analysis