|
CMU-ISR-08-140
Institute for Software Research
School of Computer Science, Carnegie Mellon University
CMU-ISR-08-140
Checking Framework Interactions with Relationships
Ciera Jaspan, Jonathan Aldrich
December 2008
CMU-ISR-08-140.pdf
Keywords: Software frameworks, relationships, static analysis,
verification
Software frameworks impose constraints on how plugins may interact with them.
Many of hese constraints involve multiple objects, are temporal, and depend
on runtime values. Additionally, they are difficult to specify because they
are non-local and may break behavioral subtyping. This work presents
relationships as a means for specifying framework constraints,
and it presents a formal description and implementation of a static
analysis to find constraint violations in plugin code. We define three
variants of this analysis: one is sound, one is complete, and one provides
compromise of the two. We prove soundness and completeness for the appropriate
variants, and we show how the compromise variant works on examples from
real-world programs. This allows the user to select the option which is
the most cost-effective in practice with regard to the number of false
positives and false negatives.
110 pages
|