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

EHS：嵌入式和混合系统基于约束的静态分析

• 批准号: 0411363
• 负责人: Zohar Manna
• 金额: $ 30万
• 依托单位: Stanford University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2004
• 资助国家: 美国
• 起止时间: 2004-09-01 至 2007-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0411363&HistoricalAwards=false
• 关键词: EHS; Constraint; based; Static; Analysis

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.

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