Modular Static Checking of Software Design Intent Using Permissions

University Of Wisconsin-Milwaukee, Milwaukee WI

Investigators

Abstract

CCF-0702635 TITLE Modular Static Checking of Software Design Intent Using Permissions PI John Boyland Modularity is the key technique for controlling the complexity of large software projects. Modules often have requirements on how they communicate and collaborate with other modules. This work extends what can be expressed and checked in a modular way. Annotations of design intent about properties such as aliasing, effects and locking are given a strong semantic foundation using the concept of ``permissions.'' Annotations avoid both the need of a type system to have a single decidable semantics, and the excessive detail of full specification. Rather, a single (in principle undecidable) semantic system can be checked using a variety of different algorithms ranging from syntax-directed analysis to theorem proving. This work has the following objectives: (1) show soundness of a full system of permissions; (2) give a semantics for a wide-range of design-intent annotations; (3) implement permissions checkers; and (4) evaluate their usefulness on large commercial and open-source software. This research uses the techniques of logics, type systems and program analysis. The investigators use an existing infrastructure integrated with an open-source environment (``Eclipse''). It is the intent to make the resulting analyses available in open-source and/or commercial products.