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

摘要：静态分析方法在嵌入式系统设计中起着验证和优化两大重要作用。静态分析技术通过分析给定系统的描述来推断其特性。它对特定系统的适用性取决于它在平衡计算成本的同时推断有趣属性的能力。这项研究研究了一类新的静态分析技术，它有可能显著增加静态分析的范围。这种方法被称为基于约束的静态分析，与以前的静态分析工作不同。传统的基于传播的静态分析方法侧重于迭代地构建对所需属性的更好的近似，而本文提出的方法直接解决了这些属性。给定一个由模板属性参数化表示的断言类，基于约束的方法生成并解决未知参数上的约束。这种策略的转变寻求以下优势：*它用一种精确和可预测的近似方法取代了启发式猜测。传统的方法通常需要通过扩大和缩小操作符来使用启发式猜测，这限制了它们的适用性。*与基于传播的方法相比，新方法可以很容易地优化以有效地处理特殊情况。*它可以自然扩展到非线性离散和混合系统的分析。*实时和混合系统的基于约束的方法避免了显式地求解微分方程，使它们适用于更大类型的系统。这项研究的预期好处有很多。静态分析在过去十年中没有取得重大突破。该项目希望恢复对静态分析的兴趣，并鼓励使用数学技术，如Groebner基。本研究还将约束求解技术与验证联系起来，从而为约束求解社区参与嵌入式系统设计相关问题提供了机会。最后，本研究的结果更接近于在安全关键设备的软件认证中使用安全属性的正式证明的可行性。

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.