Certifying Measurement Unit Safety Policy
Revision as of 22:23, 24 February 2016 by Yzhng173
This work has been published as a system paper in RTA'03 and as a tool paper in ASE'03.
- Rule-Based Analysis of Dimensional Safety
- Feng Chen and Grigore Rosu and Ram prasad Venkatesan
- RTA'03, Lecture Notes in Computer Science (LNCS) 2706, pp 197-207. 2003
- Abstract. Dimensional safety policy checking is an old topic in software analysis concerned with ensuring that programs do not violate basic principles of units of measurement. Scientific and/or navigation software is routinely dimensional and violations of measurement unit safety policies can hide significant domain-specific errors which are hard or impossible to find otherwise. Dimensional analysis of programs written in conventional programming languages is addressed in this paper. We draw general design principles for dimensional analysis tools and then discuss our prototypes, implemented by rewriting, which include both dynamic and static checkers. Our approach is based on assume/assert annotations of code which are properly interpreted by our tools and ignored by standard programming language compilers/interpreters. The output of our prototypes consists of warnings that list those expressions violating the unit safety policy. These prototypes are implemented in the rewriting system Maude, using more than 2,000 rewriting rules. This paper presents a non-trivial application of rewriting techniques to software analysis.
- Abstract. 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.