区间斜率作为浮点变量的数值抽象域
Interval Slopes as Numerical Abstract Domain for Floating-Point Variables
AI总结：
提出一种基于区间斜率的部分关系抽象域，用于浮点变量的静态分析，能够模拟浮点算术行为，验证嵌入式控制系统中的运行时错误和数值精度。
摘要：
嵌入式控制系统的设计主要使用基于模型的工具，如Matlab/Simulink。数值模拟是此类工具开发和验证的核心技术。众所周知，浮点运算仅提供近似结果，但在这一活动中无处不在。为了使用基于抽象解释的静态分析验证数值模拟的行为，我们从理论和实验上提出了一种新的部分关系抽象域，专门针对浮点变量。它源于使用斜率的非线性函数的区间展开，能够模拟浮点算术的所有行为。因此，它适用于证明运行时错误的缺失或分析嵌入式控制系统的数值精度。
英文摘要：
The design of embedded control systems is mainly done with model-based tools such as Matlab/Simulink. Numerical simulation is the central technique of development and verification of such tools. Floating-point arithmetic, that is well-known to only provide approximated results, is omnipresent in this activity. In order to validate the behaviors of numerical simulations using abstract interpretation-based static analysis, we present, theoretically and with experiments, a new partially relational abstract domain dedicated to floating-point variables. It comes from interval expansion of non-linear functions using slopes and it is able to mimic all the behaviors of the floating-point arithmetic. Hence it is adapted to prove the absence of run-time errors or to analyze the numerical precision of embedded control systems.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
