User Queries for Specification Refinement Treating Shared Aspect Join Points

We present an interactive semi-automatic procedure to help users refine their requirements formally and precisely, using knowledge the user possesses but does not notice as relevant and has difficulty formalizing. Questions in natural language are presented to the user, and augmentations to specifications, written in Linear Temporal Logic, are automatically created according to the answers. We apply our approach to a case study on specifying the desired aspect behavior in a delicate case when multiple aspects can share a join-point, i.e., be applied at the same state of base program computation. The questions used in the case study are derived from an in-depth analysis of semantics and mutual influence of aspects at a shared join-point. Aspects sharing a join-point might, but do not have to, semantically interfere. Our analysis and specification refinement enables programmers to distinguish between potential and actual interference among aspects at shared join-points, when aspects are modeled as state transition diagrams, and specifications are given as LTL assumptions and guarantees. The refined aspect specification, obtained from the procedure we describe, enables modular verification and interference detection among aspects even in the presence of shared join-points.