EHS: Constraint-based Static Analysis of Embedded and Hybrid Systems

点击翻译按钮获取中文摘要

Manna - Abstract: Static analysis methods play two vital roles in the design of embeddedsystems: validation and optimization. A static analysis techniquededuces properties of a given system by analyzing its description.Its applicability to a particular system hinges upon its ability todeduce interesting properties while balancing the computational cost.This research studies a novel class of techniques forstatic analysis that has the potential to significantly increase thescope of static analysis. The methodology, called constraint-based static analysis, divergesfrom previous work on static analysis. Whereas traditionalpropagation-based static analysis methods concentrate on iterativelyconstructing better approximations to the desired properties, theproposed approach directly solves for the properties. Given a classof assertions represented parametrically by a template property, aconstraint-based method generates and solves constraints on theunknown parameters. This shift in strategy seeks the followingadvantages:* 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 openingopportunities for involvement of the constraint solving communityin problems pertinent to the design of embedded systems. Finally, theresults of this research bring closer the feasibility of using formal proof of safety properties in certifying software for safety-critical devices.