COVER is a uni ed framework that supports the interplay between requirements analysts and software developers. It contracts a bridge between the requirements analyst's and the software developer's artifacts by enabling goal model analysis during software design. The goal model produced by the requirements analyst is kept alive and updated while the system is designed. Whenever the design of the system changes, COVER veri es the new design against the requirements of interest. The veri cation results are used to trigger a goal model analysis procedure. The results of this analysis can be used by the requirements analyst and the software developer to update the goal model or the design of the system. In this paper, we present the tool support developed for COVER.
Software development is a complex activity which relies on a sequence of development steps. It usually starts with the requirements analyst collecting the requirements of the system. The identi ed requirements are used by the software developer as guidelines in the system design, in which a model of the system is produced. The system design is not a straightforward activity. It usually includes a set of development rounds, in which a partial and incomplete model of the system is iteratively re ned. In order to satisfy the customer needs, the software developer must ensure that the nal, fully speci ed, version of the system satis es the requirements of interest.
Researchers' interest has been mainly focused on two separate aspects. On
the one hand, researchers have been working on developing techniques and
frameworks to help the requirements analyst in collecting and analyzing requirements.
KAOS [
One of the main problems of current software development techniques is the lack of integration between these two set of tools, and, consequently, the lack of a bridge between requirements analysts' and the software developers' work. This mismatch particularly a ects modern development life cycles which 1. are heavily based on iterative and incremental development processes and 2. require a strong interaction between the requirements analyst and the software developer.
COVER (Change-based gOal VEri er and Reasoner) [
This paper presents the tool support (hereafter called either COVERTool
or just COVER) used in a speci c instantiation of the framework, where the
variation of the TROPOS modeling language presented in [
The rest of the paper is organized as follows. Section 2 gives an overview of COVERTool. Section 3 describes the user experience in using COVERTool. Finally, Section 4 concludes the paper. 2
COVER3 is a framework that supports the interplay between requirements
analysis and design. It can be used to verify which goals of the goal models are
satis ed by the new design every time the developer changes the design of the
system, and to verify how the current design satis es the goals of the goal model,
when the requirements analyst modi es the goal model. The overall tool support
for COVER is a Java 8 application that uses the Goal Reasoning Tool (Gr-tool) [
The framework consists mainly of three main parts: the goal model design and requirements speci cation, the system design, and the design veri cation, which enables the goal model analysis. 3 The tool is available at https://github.com/claudiomenghi/COVER. Goal Model Design
G1
Goal model design and requirements speci cation. The requirements analyst develops a TROPOS goal model for the system using Gr-tool. Goals are re ned into requirements, which, in turn, are decomposed into tasks, i.e., the functionalities the system has to provide. The completion of a task is indicated by the developer with an event: the system generates the event if and only if the task of interest has been accomplished. The analyst uses these events to provide a formal description of some of the goals of the system. The analyst chooses the set of requirements to be formally speci ed in FLTL depending on the system under development. Note that events and FLTL formulae are not part of TROPOS; they are used to link the requirements analyst and developers models. System design. The software developer produces a high-level model of the system to be in MTSs. Then, she/he iteratively decomposes the system until the behaviors of all of its components are speci ed.
Design veri cation and goal model analysis. COVER veri es the new (incomplete/partial) design of the system. It relies on MTSA as a veri cation tool for MTSs. Since the model is incomplete, the veri cation procedure may return three di erent values: > if the property is satis ed by the current design, no matter how the unde ned parts of the system will be later re ned; ? if the property is not satis ed; ? whether its satisfaction depends on the parts which still have to be re ned.
The values obtained from the veri cation of the system design are used to
trigger the analysis of the goal model. Each goal of the goal model is associated
with an initial value, which speci es whether it is satis ed, possibly satis ed,
or not satis ed by the current design. The goals that have not been formalized
are considered as not satis ed. A label propagation algorithm is then used to
propagate the initial values. The label propagation algorithm in [
We describe how COVER can be used by requirements analysts and software developers.
Requirements analyst perspective. The analyst identi es the requirements of the system in TROPOS, using the Gr-Tool. We assume that the developer speci es each goal by means of an identi er followed by the goal name, i.e., the textual description of each goal matches the following pattern: IDENTIFIER: GOAL NAME. When the nal version of the goal model is produced, the requirements analyst formally speci es the requirements of interest. The analyst provides the speci cation of the requirements in a le with extension .lts. This le contains a set of FLTL formulae that formally specify the goals of the system. Each goal starts with an identi er followed by a semi column (e.g., G1 :) which is preceded by the keyword assert. When the formalization of the requirements ends, the requirements analyst forwards the produced le to the software developer. 1 java - jar COVER . jar initGoalModel . goal design . lts PROC finalGoalModel . goal
Listing 1.1. Running COVER
When the software developer produces a new (partial) model of the system, a modi ed version of the le .lts, containing also a behavioral model of the system, is delivered to the requirements analyst. The analyst runs COVERTool by executing the command in Listing 1.1, where: { initGoalModel.goal is the original goal model to be considered; { design.lts is the design to be veri ed; { PROC is the identi er of the process speci ed by the MTS contained in the le design.lts to be considered by the veri cation procedure; { finalGoalModel.goal is a le that will contain the goal model updated with the results of the label propagation.
An example of the tool's output is shown in Fig. 2a. COVERTool loads the goal model and iteratively analyzes its goals. When a goal is analyzed, COVERTool extracts the identi er of the goal and checks if the le design.lts contains an FLTL property associated with the goal. If a property is speci ed, it is veri ed w.r.t. the process PROC speci ed as parameter in the COVER Tool invocation. When all the properties are veri ed, the label propagation algorithm is executed. (a) An example of COVER output.
(b) Inspecting the output using the Gr-Tool.
The requirements analyst can graphically inspect the results obtained by
COVERTool and contained in the le finalGoalModel.goal using the Gr-Tool.
For example, Fig. 2b shows an example of results obtained using COVER. The
column Input SAT contains the results of the veri cation procedure, where the
values T and P specify that the property is satis ed and possibly satis ed,
respectively. When a goal is associated with no value, it is either violated or not
associated with an FLTL formula. The column Output SAT contains the results
obtained by running the label propagation algorithm. The requirements analyst
can use these results to improve its goal model. Additional details on how these
results are used to change the goal model can be found in [
The analyst executes the previously described procedure also when she/he already possesses a design of the system and she/he changes its goal model. This allows her/him to verify which goals of the new goal model are satis ed by design. Software developer perspective. The software developer receives from the requirements analyst the le containing the requirements that the system has to satisfy. The developer produces a behavioral model of the system basing his/her decision on the received requirements and then uses MTSA to verify if the produced model satis es/possibly satis es the requirements of interest. MTSA per se does not provide any feedback about the impact of the design decision over the goal satisfaction, but COVERTool in which MTSA is integrated provides this functionality and propagates the results obtained with MTSA back to the goal model. This allows the software developer to analyze the consequences of her/his design choices over the goal satisfaction.
COVERTool is executed using the command speci ed in Listing 1.1. The
obtained results are inspected using the Gr-Tool. The software developer can use
the results of the label propagation algorithm to improve its design. Additional
details can be found in [
This paper presented the tool support for COVER, a uni ed framework that enables goal model analysis during the software development. The goal model produced by the requirements analyst is kept alive during the design of the system. At each re nement round, i.e., whenever the developer produces a new increment or changes something in the model, the new (incomplete) design of the system is veri ed. The veri cation results are used to analyze the set of goals of the goal model that are currently satis ed, possibly satis ed and not satis ed.