Static analysis methods play two vital roles in the design of embedded systems: validation and optimization. A static analysis technique deduces properties of a given system by analyzing its description. Its applicability to a particular system hinges upon its ability to deduce interesting properties while balancing the computational cost. This research studies a novel class of techniques for static analysis that has the potential to significantly increase the scope of static analysis.
The methodology, called constraint-based static analysis, diverges from previous work on static analysis. Whereas traditional propagation-based static analysis methods concentrate on iteratively constructing better approximations to the desired properties, the proposed approach directly solves for the properties. Given a class of assertions represented parametrically by a template property, a constraint-based method generates and solves constraints on the unknown parameters. This shift in strategy seeks the following advantages:
* It replaces heuristic guesses with a precise and predictable approach to approximation. Traditional approaches frequently require the use of heuristic guesses via widening and narrowing operators, which has limited their applicability. * In contrast to propagation-based methods, the new methods can be readily optimized to handle special cases effectively. * It enables a natural extension to the analysis of nonlinear discrete and hybrid systems. * The constraint-based methods for real-time and hybrid systems avoid explicitly solving differential equations, making them applicable to a larger class of systems.
The expected benefits of this research are many. Static analysis has not seen a major breakthrough in a decade. The project hopes to revive interest in static analysis and encourage the use of mathematical techniques such as Groebner bases. This research also links constraint solving technology to verification, thus opening opportunities for involvement of the constraint solving community in problems pertinent to the design of embedded systems. Finally, the results of this research bring closer the feasibility of using formal proof of safety properties in certifying software for safety-critical devices.
