Automatic and Precise Dimensional Analysis
From FSL
This paper is a follow-on to previous work within our group on unit safety, Rule-Based Analysis of Dimensional Safety and Certifying Measurement Unit Safety Policy.
[edit] Automatic and Precise Dimensional Analysis
- Marcelo d'Amorim, Mark Hills, Feng Chen and Grigore Rosu
- Technical report UIUCDCS-R-2005-2668, December 2005
- 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.
