Certifying Measurement Unit Safety Policy

From FSL
Jump to: navigation, search

This work has been published as a system paper in RTA'03 and as a tool paper in ASE'03.

RTA'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.
PDF, MOP, DOI, RTA'03, BIB


ASE'03

Certifying Measurement Unit Safety Policy
Grigore Rosu and Feng Chen
ASE'03, IEEE, pp 304-309. 2003
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.
PDF, MOP, DOI, ASE'03, BIB

Personal tools
Namespaces

Variants
Actions
Navigation