Certifying measurement unit safety policy
Certifying measurement unit safety policy
复制标题
认证计量单位安全政策
DOI：
10.1109/ase.2003.1240326
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
Feng Chen
中科院分区：
文献类型：
--
作者：
Grigore Roşu;Feng Chen
度量单元安全策略检查是软件分析中的一个主题，它关注于确保程序不违反度量单元的基本原则。这种违规可能隐藏了很难或不可能发现的重要的特定于域的错误。本文提出了用自动演绎法进行计量单位分析的方法。我们绘制测量单位认证工具的一般设计原则，并讨论我们的原型为C语言，其中包括动态和静态检查。我们的方法是基于假设/断言注释的代码，这是正确的解释我们的演绎为基础的工具和忽略标准编译器。我们不会为了支持单位而修改语言。该方法可以扩展到包含其他安全策略，而无需付出很大努力。
Measurement unit safety policy checking is a topic in software analysis concerned with ensuring that programs do not violate basic principles of units of measurement. Such violations can hide significant domain-specific errors which are hard or impossible to find otherwise. Measurement unit analysis by means of automatic deduction is addressed in this paper. We draw general design principles for measurement unit certification tools and discuss our prototype for the C language, which includes both dynamic and static checkers. Our approach is based on assume/assert annotations of code, which are properly interpreted by our deduction-based tools and ignored by standard compilers. We do not modify the language in order to support units. The approach can be extended to incorporate other safety policies without great efforts.