Modular Verification of Software Systems

Kathi Fisler

Worcester Polytechnic Institute

Abstract

Aspect-oriented programming (AOP) has become an increasingly important programming paradigm. AOP is one of a family of means for expressing abstractions that cut across the program's dominant modularity; these techniques enable the construction of software by composing features. Despite their importance, feature-based programming methods lack supporting computer-aided verification techniques, which are necessary for increasing reliability and developing confidence in systems.

This talk presents a technique for verifying feature-based programs (expressed as state machines). By analogy with modular compilation, we support modular verification, to both enable independent development and to reduce the computational cost of verification. We present the analysis and discuss subtleties that arose as we applied our prototype verifiers to real case studies.

Biography

Kathi Fisler is an Assistant Professor of Computer Science at WPI. Her research centers around formal approaches to understanding and predicting functional behavior of hardware and software systems. She has a particular interest in the role of diagrammatic representations in verification. Her current work explores modular analysis of feature-oriented software systems, the computational advantages of timing diagrams as a logic for temporal specifications, and change-impact analysis for access-control policies. Kathi earned her PhD in 1996 from Indiana University, did a postdoc at Rice University and internships at Bell Labs and Intel before starting at WPI in 2000.