Foundations of incremental aspect model-checking Export

@article{citeulike:1255311, abstract = {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.}, address = {New York, NY, USA}, author = {Krishnamurthi, Shriram and Fisler, Kathi}, citeulike-article-id = {1255311}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=1217295.1217296}, citeulike-linkout-1 = {http://dx.doi.org/10.1145/1217295.1217296}, doi = {10.1145/1217295.1217296}, journal = {ACM Trans. Softw. Eng. Methodol.}, keywords = {aspect-oriented, checking, feature-oriented, incremental, model, modular, programming, software, verification}, month = {April}, number = {2}, posted-at = {2008-11-15 19:48:32}, priority = {2}, publisher = {ACM Press}, title = {Foundations of incremental aspect model-checking}, url = {http://dx.doi.org/10.1145/1217295.1217296}, volume = {16}, year = {2007} }

TY - JOUR ID - citeulike:1255311 L3 - citeulike-article-id:1255311 N2 - 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. IS - 2 JF - ACM Trans. Softw. Eng. Methodol. AD - New York, NY, USA TI - Foundations of incremental aspect model-checking PB - ACM Press VL - 16 KW - aspect-oriented KW - checking KW - feature-oriented KW - incremental KW - model KW - modular KW - programming KW - software KW - verification AU - Krishnamurthi, Shriram AU - Fisler, Kathi PY - 2007/04// UR - http://dx.doi.org/10.1145/1217295.1217296 ER -