Difference between revisions of "Certifying Measurement Unit Safety Policy"

From FSL
Jump to: navigation, search
Line 1: Line 1:
 +
This work has been published as a full paper in RTA'03 and as a tool paper in ASE'03.
 +
 +
== RTA'03 ==
 
<purge></purge>
 
<purge></purge>
<pub id='chen-rosu-2003-ase' template='PubDefaultWithAbstract'> </pub>
+
<pub id='chen-rosu-venkatesan-2003-rta' template='PubDefaultWithAbstractAndTitle'> </pub>
 +
 
 +
== ASE'03 ==
 +
<purge></purge>
 +
<pub id='chen-rosu-2003-ase' template='PubDefaultWithAbstractAndTitle'> </pub>

Revision as of 06:08, 3 August 2006

This work has been published as a full 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, LNCS 2706, pp197 - 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, LNCS, RTA'03, DBLP, BIB


ASE'03


Personal tools
Namespaces

Variants
Actions
Navigation