MAVEN: Modular Aspect Verification Export

@incollection{citeulike:3033597, abstract = {Aspects are program modules that include descriptions of key events (called joinpoints) and code segments (called advice) to be executed at those key events when the aspect is bound (woven) to an underlying system. The MAVEN tool verifies the correctness of an aspect relative to its specification, independently of any specific underlying system to which it may be woven. The specification includes assumptions about properties of the underlying system, and guaranteed properties of any system after the aspect is woven into it. The approach is based on model checking of a single state machine constructed using the linear temporal logic (LTL) description of the assumptions, a description of the joinpoints, and the state machine of the aspect advice. The tableau of the LTL assumption is used in a unique way, as a representative of any underlying system satisfying the assumptions. This is the first technique for once-and-for-all verification of an aspect relative to its specification, thereby increasing the modularity of proofs for systems with aspects.}, author = {Goldman, Max and Katz, Shmuel}, citeulike-article-id = {3033597}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/978-3-540-71209-1_24}, doi = {10.1007/978-3-540-71209-1_24}, journal = {Tools and Algorithms for the Construction and Analysis of Systems}, keywords = {aspects, behavior, checking, enriched, model}, pages = {308--322}, posted-at = {2008-11-15 21:35:20}, priority = {3}, title = {MAVEN: Modular Aspect Verification}, url = {http://dx.doi.org/10.1007/978-3-540-71209-1_24}, year = {2007} }

TY - CHAP ID - citeulike:3033597 L3 - citeulike-article-id:3033597 N2 - Aspects are program modules that include descriptions of key events (called joinpoints) and code segments (called advice) to be executed at those key events when the aspect is bound (woven) to an underlying system. The MAVEN tool verifies the correctness of an aspect relative to its specification, independently of any specific underlying system to which it may be woven. The specification includes assumptions about properties of the underlying system, and guaranteed properties of any system after the aspect is woven into it. The approach is based on model checking of a single state machine constructed using the linear temporal logic (LTL) description of the assumptions, a description of the joinpoints, and the state machine of the aspect advice. The tableau of the LTL assumption is used in a unique way, as a representative of any underlying system satisfying the assumptions. This is the first technique for once-and-for-all verification of an aspect relative to its specification, thereby increasing the modularity of proofs for systems with aspects. JF - Tools and Algorithms for the Construction and Analysis of Systems EP - 322 TI - MAVEN: Modular Aspect Verification SP - 308 KW - aspects KW - behavior KW - checking KW - enriched KW - model AU - Goldman, Max AU - Katz, Shmuel PY - 2007/// UR - http://dx.doi.org/10.1007/978-3-540-71209-1_24 ER -