Aspect Categories and Classes of Temporal Properties Export

@incollection{citeulike:715399, abstract = {Generic categories of aspects are described, and their potential value is explained. For some categories, broad classes of syntactically identifiable temporal properties, such as safety, liveness, or existence properties, are guaranteed to hold for a system with any aspect of the category woven into it, if the property was true in the system without the aspect. Thus classes of properties preserved by the aspect are defined. Moreover, relatively simple verification techniques are shown to hold for some classes of temporal properties over systems augmented with some other categories of aspects. Verification of new properties added by the aspects is also considered. Each category is defined in terms of the semantic transformation it makes to the state graphs of underlying systems. A generic procedure to identify syntactically when an aspect belongs to a category is described and related to existing code analysis systems that use static code analysis and dataflow techniques. The definitions of categories, identification procedures, and lemmas about property classes provide the needed foundations that justify and motivate automatic code analysis modules to identify aspect categories. The categories enable simpler proofs of correctness than would otherwise be possible, and exploiting their characteristics can aid in software development.}, author = {Katz, Shmuel}, citeulike-article-id = {715399}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/11687061_4}, citeulike-linkout-1 = {http://www.springerlink.com/content/t5604m0783472287}, doi = {10.1007/11687061_4}, journal = {Transactions on Aspect-Oriented Software Development I}, keywords = {aspect-oriented, categorization, programming}, month = {February}, pages = {106--134}, posted-at = {2009-10-20 01:02:53}, priority = {2}, title = {Aspect Categories and Classes of Temporal Properties}, url = {http://dx.doi.org/10.1007/11687061_4}, volume = {3880}, year = {2006} }

TY - CHAP ID - citeulike:715399 L3 - citeulike-article-id:715399 N2 - Generic categories of aspects are described, and their potential value is explained. For some categories, broad classes of syntactically identifiable temporal properties, such as safety, liveness, or existence properties, are guaranteed to hold for a system with any aspect of the category woven into it, if the property was true in the system without the aspect. Thus classes of properties preserved by the aspect are defined. Moreover, relatively simple verification techniques are shown to hold for some classes of temporal properties over systems augmented with some other categories of aspects. Verification of new properties added by the aspects is also considered. Each category is defined in terms of the semantic transformation it makes to the state graphs of underlying systems. A generic procedure to identify syntactically when an aspect belongs to a category is described and related to existing code analysis systems that use static code analysis and dataflow techniques. The definitions of categories, identification procedures, and lemmas about property classes provide the needed foundations that justify and motivate automatic code analysis modules to identify aspect categories. The categories enable simpler proofs of correctness than would otherwise be possible, and exploiting their characteristics can aid in software development. JF - Transactions on Aspect-Oriented Software Development I EP - 134 TI - Aspect Categories and Classes of Temporal Properties VL - 3880 SP - 106 KW - aspect-oriented KW - categorization KW - programming AU - Katz, Shmuel PY - 2006/02// UR - http://dx.doi.org/10.1007/11687061_4 ER -