Automatic and Precise Dimensional Analysis

From FSL
Jump to: navigation, search

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.

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.
PDF, Sources, TR@UIUC, BIB

Personal tools