@incollection{Zhang2012ad, Abstract = {Crosscutting concerns are pervasive in embedded software and ambient systems due to the stringent non-functional requirements imposed on them. Maintaining families of these systems to address issues with the crosscutting concerns, such as security concerns, is recognised to be tedious and costly. To tackle the above problem, we adapt the aspect-oriented paradigm to feature-modeling. One of the most serious problems in aspect-oriented modeling is the potential of taking a valid model and spoiling its validity when weaving an aspect to it. We present a formal verification technique of aspectual composition in the context of feature-modeling that is based on product family algebra. We define a set of validity criteria for aspects with regard to their corresponding base specifications. The proposed approach enables the detection of dependency, reference, or definition invalid aspects. The verification is done prior to the weaving of the aspects to their base specifications.}, Address = {Thessaloniki, Greece}, Author = {Qinglei Zhang and Ridha Khedri and Jason Jaskolka}, Booktitle = {Proceedings of the 10th International Conference on Software Engineering and Formal Methods}, Editor = {George Eleftherakis and Mike Hinchey and Mike Holcombe}, Month = {October}, Pages = {109-125}, Publisher = {Springer Berlin/Heidelberg}, Series = {Lecture Notes in Computer Science}, Title = {Verification of Aspectual Composition in Feature-Modeling}, Volume = {7504}, Year = {2012} }