Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

5-2006

Abstract

Misuse of measurement units is a common source of errors in scientific applications, but standard type systems do not prevent such errors. Dimensional analysis in physics can be used to manually detect such errors in physical equations. It is, however, not feasible to perform such manual analysis for programs computing physical equations because of code complexity. In this paper, we present a type system to automatically detect potential errors involving measurement units. It is constraint-based: we model units as types and flow of units as constraints. However, standard type checking algorithms are not powerful enough to handle units because of their abelian group nature (e.g., being commutative, multiplicative, and associative). Our system combines techniques such as type inference and Gaussian Elimination to overcome this problem. We have implemented Osprey, a prototype of the system for C programs, and evaluated it on various test programs, including computational physics and mechanical engineering applications. Osprey discovered unknown errors in mature code; it is precise with few false positives; it is also efficient and scales to large programs---we have successfully used it to analyze programs with hundreds of thousands of lines of code.

Keywords

Gaussian elimination, measurement units, dimensional analysis, constraint-based analysis, type systems

Discipline

Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

ICSE '06: Proceedings of the 28th International Conference on Software Engineering: 20-28 May 2006, Shanghai, China

First Page

262

Last Page

271

ISBN

9781595933751

Identifier

10.1145/1134285.1134323

Publisher

ACM

City or Country

New York

Copyright Owner and License

Authors

Additional URL

http://doi.org/10.1145/1134285.1134323

Download

Share

COinS