Automatic and Precise Dimensional Analysis

d'Amorim, Marcelo; Hills, Mark; Chen, Feng; Rosu, Grigore

Permalink

https://hdl.handle.net/2142/11131 Copy

Description

Title

Automatic and Precise Dimensional Analysis

Author(s)

• d'Amorim, Marcelo
• Hills, Mark
• Chen, Feng
• Rosu, Grigore

Issue Date

2005-12

Keyword(s)

computer science

Abstract

The loss of NASA's Mars climate orbiter is evidence of the importance of units of measurement as a safety policy for software in general and for scientific applications in particular. In this paper we present a static analysis technique that detects violations of the unit policy. The technique relies on domain-specific unit annotations inserted in the code, either manually or automatically with the support of a tool, which are verified conservatively, i.e., all runtime unit errors are detected statically using an automatic theorem prover. This paper informally compares our approach with others, describes the technique in detail, and evaluates a benchmark built of standard programs for unit analysis and important fragments of NASA's SCRover project code.

Type of Resource

text

Permalink

http://hdl.handle.net/2142/11131

Copyright and License Information

You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).

Owning Collections