Identification of early aspects is the critical problem in aspect-oriented requirement engineering. But the representation of crosscutting concerns is various, which makes the identification difficult. To address the problem, this paper proposes the AspectQuery method based on goal model. We analyze four kinds of goal decomposition models, then summarize the main factors about identification of crosscutting concerns and conclude the identification rules based on a goal model. A goal is crosscutting concern when it satisfies one of the following conditions: i) the goal is contributed to realize one soft-goal; ii) parent goal of the goal is candidate crosscutting concern; iii) the goal has at least two parent goals. AspectQuery includes four steps: building the goal model, transforming the goal model, identifying the crosscutting concerns by identification rules, and composing the crosscutting concerns with the goals affected by them. We illustrate the AspectQuery method through a case study (a ticket booking management system). The results show the effectiveness of AspectQuery in identifying crosscutting concerns in the requirement phase.

The methodologies of product-line engineering emphasize proactive reuse to construct high-quality products more quickly that are less costly. Requirement engineering for software product families differs significantly from requirement engineering for single software products. The requirements for a product line are written for the group of systems as a whole, with requirements for individual systems specified by a delta or an increment to the generic set. Therefore, it is necessary to identify and explicitly denote the regions of commonality and points of variation at the requirement level. In this paper, we suggest a method of producing requirements that will be a core asset in the product line. Briefly, requirements for families of similar systems (i.e. domain) are collected and generalized which are then analyzed and modeled. The domain requirement as a core asset explicitly manages the commonality and variability. Through this method, the reuse of domain requirements can be enhanced. As a result, the cost and time of software development can be reduced and the productivity increased while significantly reducing error in the requirements.

Critical properties of real-time embedded systems must be verified before these systems are deployed as failing to meet these properties may cause considerable property damages and/or human casualties. Although Statechart is one of the most popular languages for modeling behavior of real-time systems, proof systems and analysis tools for Statechart so far are in research and do not fully support the semantics of the original Statechart, or have limited capabilities for proving real-time properties. This paper introduces a toolset ASADAL/PROVER for verifying temporal properties of Statechart extended with justice and compassion properties. ASADAL/PROVER is composed of two subsystems, RTTL-Prover and Model-Checker. The RTTL-Prover converts Statechart specifications into real-time temporal logic (RTTL) formulas of Ostroff, and then checks if the formulas satisfy a temporal property (also in RTTL) using theorem proving techniques. The Model-Checker supports verification of a predefined set of real-time properties using a model checking technique. The RTTL-Prover can support verification of any real-time properties as long as they can be specified in RTTL and, therefore, messages generated by the tool are general and may not be of much help in debugging Statechart specifications. The Model-Checker, however, can provide detailed information for debugging. ASADAL/PROVER has been applied successfully to some experimental systems. One of on-going researches in this project is to apply the symbolic model-checking technique by[3]to support Statecharts with a much larger global-state space. We are also extending the types of temporal properties supported by the Model-Checker.