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