Foundations of incremental aspect model-checking

Programs are increasingly organized around features, which are encapsulated using aspects and other linguistic mechanisms. Despite their growing popularity amongst developers, there is a dearth of techniques for computer-aided verification of programs that employ these mechanisms. We present the theoretical underpinnings for applying model checking to programs (expressed as state machines) written using these mechanisms. The analysis is incremental, examining only components that change rather than verifying the entire system every time one part of it changes. Our technique assumes that the set of pointcut designators is known statically, but the actual advice can vary. It handles both static and dynamic pointcut designators. We present the algorithm, prove it sound, and address several subtleties that arise, including cascading advice application and problems of circular reasoning.