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.

甘露 - 摘要：静态分析方法在嵌入式系统的设计中起两个至关重要的作用：验证和优化。 一种静态分析技术通过分析其描述来实现给定系统的特性。对特定系统的适用性取决于其能力，同时平衡了计算成本。这项研究研究了一类新型的技术外观分析，具有显着增加静态分析的阶段。该方法称为基于约束的静态分析，从先前的静态分析方面分歧。基于传统propagation的静态分析方法集中于迭代构建更好的所需属性的近似值，而所采用的方法直接求解了这些属性。 给定一个以模板属性为参数表示的classof断言，基于Aconstraint的方法生成并求解了Innknown参数的约束。 策略的这种转变寻求以下内容：*它以精确且可预测的近似方法代替了启发式猜测。传统方法经常需要通过扩大和狭窄的操作员来使用启发式猜测，这限制了其适用性。 *实时和混合系统的基于约束的方法避免明确求解微分方程，使其适用于较大类别的系统。这项研究的预期好处很多。十年来，静态分析并未实现重大突破。该项目希望恢复对静态分析的兴趣，并鼓励使用诸如格罗布纳基础等数学技术。这项研究还将解决技术的约束与验证联系起来，因此，与嵌入式系统的设计有关的约束解决社区问题的开放式运动。 最后，这项研究的内容更加接近使用正式的安全性证明在为安全至关重要的设备认证软件中的可行性。