Christophe Negre

Efficient Binary Polynomial Multiplication Based on Optimized Karatsuba Reconstruction

Keywords: Binary polynomial multiplication, Karatsuba formula, optimized recursive reconstruction

, Bernstein proposed two optimized Karatsuba formulas for binary polynomial multiplication. Bernstein obtained these optimizations by re-expressing the reconstruction of one or two recursions of the Karatsuba formula. In this paper we present a generalization of these optimizations. Specifically, we optimize the reconstruction of s recursions of the Karatsuba formula for s ≥ 1. To reach this goal, we express the recursive reconstruction through a tree and re-organize this tree to derive an optimized recursive reconstruction of depth s. When we apply this approach to a recursion of depth s = log 2 (n) we obtain a parallel multiplier with a space complexity of 5.25n log 2 (3) + O(n) XOR gates and n log 2 (3) AND gates and with a delay of 2 log 2 (n)D ⊕ + D ⊗ .

INTRODUCTION

Finite fields are intensively used in cryptographic applications [START_REF] Miller | Use of elliptic curves in cryptography[END_REF], [START_REF] Koblitz | Elliptic curve cryptosystems[END_REF], [START_REF] Boneh | Identity-Based Encryption from the Weil Pairing[END_REF], [START_REF] Boneh | Short Signatures from the Weil Pairing[END_REF] and in error control coding [START_REF] Berlekamp | Bit-serial Reed-Solomon encoder[END_REF]. Specifically, a single cryptographic protocol based on elliptic curve requires several hundreds additions and multiplications in a finite field of size [2 160 , 2 600 ]. An addition in a finite field is generally simpler to implement than a multiplication which remains quite costly in time and resources.

Consequently, during the past two decades, an important amount of work have been done to improve the efficiency of the multiplication in finite field.

In this paper we focus on hardware design of parallel multiplier for extended binary fields F 2 n . A multiplication in such fields consists of a multiplication of binary polynomial followed by a reduction modulo an irreducible polynomial P of degree n. The most costly part of the finite field multiplication is the polynomial multiplication, since, when P is sparse (i.e., when P is a trinomial or a pentanomial), the reduction has a cost of O(n) bit additions. A binary polynomial multiplication can been done through August 22, 2012 DRAFT extension by first expressing the s recursions of the Karatsuba reconstruction in a tree structure. We then re-organize the operations in this tree leading to the optimization of the s recursions of the Karatsuba reconstruction. We also give an algorithmic form of the resulting reconstruction and evaluate thoroughly the complexity of this approach. We will show that if we apply this method to a recursion of depth s = log 2 (n), we obtain a parallel multiplier with a space complexity of 5.25n log 2 (3) + O(n) XOR gates and n log 2 (3) AND gates and a delay of 2 log 2 (n)D ⊕ + D ⊗ .

The paper is organized as follows: in Section 2, we review the original Karatsuba formula and the optimized versions proposed by Bernstein [START_REF] Bernstein | Batch Binary Edwards[END_REF]. In Section 3 we generalize the approach of Bernstein to s recursions of Karatsuba formula. Finally, we compare the complexities of the proposed method with best known approaches and give some concluding remarks in Section 4.

REVIEW OF KARATSUBA FORMULA

We review in this section the method of Karatsuba for the multiplication of binary polynomials. We also review the recent optimizations presented by Bernstein at Crypto 2009 [START_REF] Bernstein | Batch Binary Edwards[END_REF].

Karatsuba formula

We consider two degree n -

1 polynomials A(X) = n-1 i=0 a i X i and B(X) = n-1 i=0 b i X i in F 2 [X] with n = 2 k
′ 0 = A ′ 0 B ′ 0 = A L B L , C ′ 1 = A ′ 1 B ′ 1 = (A L + A H )(B L + B H ), C ′ 2 = A ′ 2 B ′ 2 = A H B H . (1)
• Reconstruction. We then reconstruct C = A × B as

C = C ′ 0 (1 + X n/2 ) + C ′ 1 X n/2 + C ′ 2 X n/2 (1 + X n/2 ), (2)
= C ′ 0 + (C ′ 0 + C ′ 1 + C ′ 2 )X n/2 + C ′ 2 X n . (3)
The three half size products C ′ 0 , C ′ 1 and C ′ 2 of (1) are computed by applying the same method recursively. If the recursive computations are performed in parallel we get a parallel multiplier with a subquadratic space complexity and a logarithmic delay. Specifically, the number of XOR gates (S ⊕ (n)), AND gates (S ⊗ (n)) and the delay are given in ( 4) is given in a recursive form (left) and a non-recursive form (right).

         S ⊕ (n) = 4n -4 + 3S ⊕ (n), S ⊗ (n) = 3S ⊗ (n), D(n) = 3D ⊕ + D(n/2).          S ⊕ (n) = 6n log 2 (3) -8n + 2, S ⊗ (n) = n log 2 (3) , D(n) = 3 log 2 (n)D ⊕ + D ⊗ . (4)
In the previous equation, D ⊕ represents the delay of an XOR gate and D ⊗ the delay of an AND gate.

Optimization of the reconstruction.

Recently an optimized version of the Karatsuba formula have been proposed: Bernstein in [START_REF] Bernstein | Batch Binary Edwards[END_REF] have reduced the complexity of the reconstruction step as follows

Step 1.

R 0 = P 0 + X n/2 P 1 , (Cost = n/2 -1 bit additions), Step 2. R 1 = R 0 (1 + X n/2 ), (Cost = n -1 bit additions), Step 3. C = R 1 + P 2 X n/2 , (Cost = n -1 bit additions).
(

) 5
This approach reduces the number of bit additions of one recursion of the Karatsuba formula

S ⊕ (n) = 7n/2 -3 + 3S ⊕ (n/2) which gives for a full recursion S ⊕ (n) = 5.5n log 2 (n) -7n + 3/2. But this approach conserves a delay of D(n) = 3 log 2 (n)D ⊕ + D ⊗ .
In the sequel we will call the reconstruction formula (5) as Bernstein's Reconstruction (BR 1 ) of one recursion of the Karatsuba formula.

Remark 1. The optimization of the reconstruction of the Karatsuba formula was also proposed by Zhou and Michalik in [START_REF] Zhou | Comments on "A New Architecture for a Parallel Finite Field Multiplier with Low Complexity Based on Composite Field[END_REF], independently from Bernstein. We have presented the approach of Bernstein since his approach is the base of our generalization.

August 22, 2012 DRAFT

Bernstein's optimization of two recursions of Karatsuba formula

In [START_REF] Bernstein | Batch Binary Edwards[END_REF] Bernstein has also extended his optimization to two recursions of Karatsuba formula. We here present this approach in a slightly different manner.

Component formation and recursive products. The component formation is recursively applied twice resulting in 9 terms of size n/4. One recursion consists of a splitting in two halves and an addition of these two halves. The corresponding circuit is depicted in Fig. 1. If we split A = A LL + A LH X n/4 + Fig. 1. Two recursions of the component polynomial formation A HL X 2n/4 + A HH X 3n/4 , the nine terms of size n/4 generated by the two recursions of the CPF are as follows A

A =A 0 (0) A 0 (1) A 1 (1) A 2 (1) A 4 (2) A 3 (2) A 2 (2) A 1 (2) A 0 (2) A 5 (2) A 6 (2) A 7 (2) A 8 (2)
(2)

0 = A LL , A (2)
1 = (A LL + A LH ), A (2)
1 = A LH , A (2) 3 = (A LL + A HL ), A (2) 4 = (A LL + A LH + A HL + A HH ), A (2) 5 = (A LH + A HH ), A (2) 6 = A HL , A (2) 7
= (A HL + A HH ), A (2)
8 = A HH .

The same formula is applied to B which results in nine terms B

i , i = 0, 1, . . . , 8 of size n/4. The nine recursive products are

C (2) i = A (2) i × B (2)
i , i = 0, 1 . . . , 8 and have degree 2n/4 -2.

Reconstruction. The first recursion in the reconstruction process produces

C (1) i , i = 0, 1, 2 in terms of C (2) i , i = 0, 1, . . . , 8. Specifically, C (1) 0 is expressed in terms of C (2) i , i = 0, 1, 2, and C (1) 1 is expressed in terms of C (2) i , i = 3, 4, 5, and C (1) 2 is expressed in terms of C (2)
i , i = 6, 7, 8, as follows:

C (1) 0 = (1 + X n/4 )C (2) 0 + X n/4 C (2) 1 + X n/4 (1 + X n/4 )C (2) 2 , C (1) 1 = (1 + X n/4 )C (2) 3 + X n/4 C (2) 4 + X n/4 (1 + X n/4 )C (2) 5 , C (1) 2 = (1 + X n/4 )C (2) 6 + X n/4 C (2) 7 + X n/4 (1 + X n/4 )C (2) 8 . (6)
We now apply a second recursion of the reconstruction process and we obtain C = C (0) in terms of

C (1) 0 , C (1) 1 , C (1) 2 as C = (1 + X n/2 )C (1) 0 + X n/2 C (1) 1 + X n/2 (1 + X n/2 )C (1) 2 . ( 7
)
August 22, 2012 DRAFT Note that the superscript (i) of A (i) , B (i) and C (i) indicates the depth of the data in the recursion.

The operations of ( 6) and ( 7) can be organized in a tree structure: starting from the root C = C (0) 0 which is linked to the three children C

(1) 0 , C

and C

(1)

2 . The links are labelled by the respective factors

(1 + X n/2 ), X n/2 and X n/2 (1 + X n/2 ) of C (1)
i , i = 0, 1, 2, appearing in [START_REF] Koblitz | Elliptic curve cryptosystems[END_REF]. We then repeat this process for each C [START_REF] Berlekamp | Bit-serial Reed-Solomon encoder[END_REF] i , i = 0, 1, 2. The resulting reconstruction tree is shown in Fig. 2 Fig. 2. Reconstruction tree of two recursions of Karatsuba

C 0 (0) ( 1 + X ) n 2 X ( 1 + X ) n 2 n 2 X n 2 X n 4 ( 1 + X ) n 4 X ( 1 + X ) n 4 n 4 X n 4 ( 1 + X ) n 4 X ( 1 + X ) n 4 n 4 X n 4 ( 1 + X ) n 4 X ( 1 + X ) n 4 n 4 C 0 (1) C 1 (1) C 2 (1) C 4 (2)
C 3

(2) C 2 (2) C 1 (2) C 0 (2) C 5 (2) C 6 (2) C 7 (2) C 8 (2)
We now modify this tree by performing the following changes:

• We first replace the sub-tree below C

(1) 1 by a block representing the reconstruction formula BR 1

given in [START_REF] Fan | Overlap-free Karatsuba-Ofman Polynomial Multiplication Algorithm[END_REF] in terms of C

(2)

3 , C (2)
4 , C

5 .

• We replace also the middle terms C

(2) 1

and C

(2) 7

by a block BR 0 representing a reconstruction of depth 0: by convention BR 0 (U ) = U for any U .

• We then move down the factor X n/2 , which appears in the label of the link between C (0) 0 and C

(1) 2 , to the three links below

C (1) 2 .
The resulting modified tree is shown in Fig. 3. This tree provides Bernstein's reconstruction for two

C 0 (0) ( 1 + X ) n 2 ( 1 + X ) n 2 X n 2 X n 4 ( 1 + X ) n 4 X ( 1 + X ) n 4 n 4 X ( 1 + X ) n 4 3 n 4 C 0 (1) C 1 (1) C 2 (1) C 4 (2) C 3 (2) C 2 (2) C 1 (2)
C 0

C 8

(2)

X 3n 4 C 7 (2) BR 1 BR 0 BR 0 X ( 1 + X ) n 4 2 n 4 August 22, 2012 DRAFT
recursions of the Karatsuba formula. We treat each operation labelled by the different link, starting from the bottom and climbing up to the root. We have three steps:

• Step 1. We add the leaf-coefficients C (2) 0 , C (2) 2 C
(2)

6 , C

(2) 8

of the tree in Fig. 3 multiplied by their respective factor 1, X n/4 , X 2n/4 and X 3n/4 :

C ← C (2) 0 + C (2) 2 X n/4 + C (2) 6 X 2n/4 + C (2)
8 X 3n/4 , Cost = 3n/4 -3.

• Step 2. We multiply by the common factor (1 + X n/4 ) and add the middle terms of depth two BR 0 (C

1 ) and BR 0 (C

7 ) multiplied by their respective monomial factor X n/4 and X 2n/4

C ← C(1 + X n/4 ), Cost = n -1, C ← C + X n/4 BR 0 (C (2) 1 ) + X 3n/4 BR 0 (C (2) 7
), Cost = 2(2n/4 -1).

• Step 3. We multiply by (1+X n/2 ) and add the middle term of depth one C

(1)

1 = BR 1 (C (2) 3 , C (2)
4 , C

5 ) multiplied by its label

X n/2        C ← C(1 + X n/2 ), Cost = n -1, C ← C + X n/2 BR 1 (C (2) 3 , C (2)
4 , C

5 ), Cost = (2n/2 -1) + 5n/4 -3

BR1

.

i , i = 0, 1, . . . , 8 9S ⊕ (n/4) 9S ⊗ (n/4)

Reconstruction

Step 1. 3n/4 -3 0

Step 2 2n -3 0

Step 3

13n/4 -5 0 Total 17n/2 -11 + 9S ⊕ (n/4) 9S ⊗ (n/4)
The non-recursive expression of this optimized approach, when n a power of 4, is as follows

   S ⊕ (n) = 217 40 n log 2 (3) -34n 5 + 11 8 , S ⊗ (n) = n log 2 (3) . ( 8
)
The recursive form of the delay of the optimized two recursions of Karatsuba formula is equal to

D(n) = 5D ⊕ + D(n/4
). The resulting non-recursive form of the delay is

D(n) = 5 2 log 2 (n)D ⊕ + D ⊗ when n is an even power of 2.
August 22, 2012 DRAFT

GENERALIZATION OF BERNSTEIN'S OPTIMIZATION OF KARATSUBA

In this section, we present an optimization of the Karatsuba multiplication which generalizes the approach of Bernstein. We will assume that the recursion in Karatsuba multiplication is performed with a depth s and we will optimize the reconstruction part of the recursions of the Karatsuba formula. For this, we will use a reconstruction tree to facilitate the generalization of Bernstein's optimization.

Karatsuba reconstruction tree of depth s

We split the Karatsuba recursion of depth s into two main steps: a first step which performs component polynomial formations and recursive products and a second step which performs the reconstruction of the product.

Component polynomial formations and recursive products. The component polynomial formation (CPF)

consists of recursively splitting in two halves and then generating three polynomials of half size: the two halves and their sum. If we perform the recursion up to a depth s we obtain the circuit shown in Fig. 4.

Note that the exponent (h) in the intermediate value

A (h) i represents the depth of A (h) i
in the recursion.

The application of the recursive CPF of depth s to the polynomial A of size n results in 3 s polynomials

A (s) i , i = 0, 1, . . . , 3 s -1 of size n/2 s .
Similarly, if we also apply the CPF of depth s to B we obtain

3 s terms B (s) i , i = 0, 1, . . . , 3 s -1. Then there are 3 s recursive products C (s) i = A (s) i × B (s) i , i = 0, . . . , 3 s -1 and the resulting polynomials C (s) i are of degree 2n/2 s -2.
A 1

A 0

(2) A 2 (s) A 1 (s) A 0 (s) A 3 -3 (s) s A (s) 3 -2 s A (s) 3 -1 s A 1 (1) A 5 (2)
A 4

(2)

A 3 (2) A 2 (1)
A 8

(2)

A 7

(2)

A 6

(

C (s-1) i = C (s) 3i (1 + X n/2 ) + C (s) 3i+1 X n/2 + C (s) 3i+2 X n/2 (1 + X n/2 ), (9)
where 0 ≤ i ≤ 3 s-1 -1. Then we repeat this process for s -2, s -1, . . . , 0 until we obtain C = C (0) 0 . These recursive reconstructions can be arranged through a reconstruction tree of depth s which has the following properties:

• The root node is labelled as C where 0 ≤ i < 3 h . We measure the depth h relatively to the root C (0) 0 of the reconstruction tree.

• Each node C (h) i of depth h is linked down to three children C (h+1) 3i , C (h+1) 3i+1 and C (h+1) 3i+2 of depth h + 1.
These three links are labelled by (1 + X n/2 h+1 ), X n/2 h+1 and X n/2 h+1 (1 + X n/2 h+1 ) respectively. This corresponds to one application of the reconstruction formula (2). In the sequel, the link joining C

X n/ 2 (1 + X n/ 2 ) C (1) 1 1 + X n/ 2 C (1) 2 C
(1) 0

X n/4 1 + X n / 4 1 + X n / 4 X n/4 X n / 4 ( 1 + X n / 4 ) X n/4 1 + X n / 4 C (s-1) 0 C (2) 0 C (2) 1 C (2) 2 C (2) 3 C (2) 4 C (2) 6 C (2) 7 C (2) 8 X n/2 X n / 4 ( 1 + X n / 4 ) X n / 4 ( 1 + X n / 4 ) C (s) 0 C (s) 1 C (s) 2 C (s) 3 s -2 C (s) 3 s -1 C (s) 3 s -3 C (s-1) 3 s-2 C (s-1) 3 s-1 -1 C (s-1) 2•3 s-2 C (s-1) 2•3 s-2 -1 C (s-1) 3 s-2 -1 1 + X n / 2 s X n / 2 s (1 + X n / 2 s ) 1 + X n / 2 s 1 + X n / 2 s X n / 2 s (1 + X n / 2 s ) 1 + X n / 2 s X n / 2 s (1 + X n / 2 s ) 1 + X n / 2 s X n / 2 s (1 + X n / 2 s ) X n/2 s X n/2 s X n/2 s X n/2 s X n/2 s 1 + X n / 2 s X n / 2 s (1 + X n / 2 s ) X n/2 s C (2) 5 X n / 2 s (1 + X n / 2 s )

The modified reconstruction tree and the generalization of Bernstein's reconstruction.

The first step to get a generalization of Bernstein's reconstruction is to modify reconstruction tree of depth s. But, before proceeding we need to set up some results. We will consider the specific nodes in and his father.

The following lemma specifies the subscripts j corresponding to the L/R nodes C

(h) j .

Lemma 1. Let h be an integer such that 0 ≤ h ≤ s. Let i = (i h-1 , . . . , i 0 ) 2 be the binary representation of an

integer i in [0, 2 h -1], we denote σ(i) the integer in [0, 3 s -1]
given by the following base 3 representation

σ(i) = (2i h-1 , . . . , 2i 0 ) 3 . ( 10
)
We consider a node C (h) j of depth h in the reconstruction tree of depth s. Then, the node

C (h) j is an L/R node of depth h if and only if there exists i in [0, 2 h -1] such that j = σ(i).
Proof: We prove it by induction on h. For h = 0 the unique L/R node is C . By induction hypothesis, there exists i ∈ [0, 2 h -1] such that k = σ(i). In other words we have i

= (i h-1 , . . . , i 1 , i 0 ) 2 and k = (2•i h-1 , . . . , 2•i 1 , 2•i 0 ) 3 . Now, since C (h+1) j
is an L/R node and since it is a child of C (h) k

we have j = 3k + j 0 where j 0 ∈ {0, 2}.

Then, we can deduce from the base 3 representation of k, that

j = (2 • i h-1 , . . . , 2 • i 1 , 2 • i 0 , j 0 ) 3 = (2 • i h-1 , . . . , 2 • i 1 , 2 • i 0 , 2(j 0 /2)) 3
This means that j = σ(i ′ ) where i ′ = (i h-1 , . . . , i 1 , i 0 , j 0 /2) 2 is in [0, 2 h+1 -1]. And this concludes the proof.

We now generalize the modifications done in Fig. 3 to the reconstruction tree of depth 2 . We perform the following modifications:

1) For each L/R-then-M node C (h) i
of depth h we replace its sub-tree by a block labelled GBR s-h . This block GBR s-h represents a recursive call to the generalized Bernstein's reconstruction method applied to a smaller tree. The inputs of this block are the leaves C (s)

3 s-h i , C (s) 3 s-h i+1 , . . . , C (s) 3 s-h i+3 s-h -1
which were the leaves of the replaced sub-tree.

2) We move down, as low as possible, all the factors of type X n/2 h appearing in the link labels. A factor X n/2 h on a link between C (h) j and his child C (h+1) 3j+2 is moved down to the three link relying C (h+1) 3j+2 to his children. We repeat this until we reach either L/R-then-M nodes or L/R leaves.

August 22, 2012 DRAFT

The modified reconstruction tree of depth s is depicted in Fig. 6.

Fig. 6. Modified reconstruction tree of depth s

C (0) 0 (1 + X n/ 2 ) 1 + X n/ 2 C (1) 2 C (1) 0 X n/4 C (2) 1 1 + X n / 4 ( 1 + X n / 4 ) ( 1 + X n / 4 ) 1 + X n / 4 C (2) 2 C (2) 0 C (2) 6 C (2) 8 X (2 s -1 )n /2 s (1 + X n/ 2 s ) 1 + X n/ 2 s X n/ 2 s (1 + X n/ 2 s ) X (2 s- 1 -1 )n /2 s (1 + X n/ 2 s ) C (s) 0 C (s) 1 C (s) 2 C (s) 3 s -3 C (s) 3 s -2 C (s) 3 s -1 X (2s -2) n/ 2 s (1 + X n/ 2 s ) X (2 s-1 +1)n/2 s C (1) 1 C
(2) 7

X 3n/4 X n/2 X n/2 s X (2 s-1 -1)n/2 s X (2 s -1)n/2 s X (2 s-1 -2 )n /2s (1 + X n/ 2 s ) X (2 s-1 +1 )n /2 s (1 + X n/ 2 s ) X 2 s-1 n/ 2 s (1 + X n/ 2 s ) GBR s-2 GBR s-1 GBR0 GBR0 GBR0 GBR0 GBR s-2
Remark 2. We could prove that the link label of the modified tree are as follows (i) If the link joins up an L/R leave C (s) j to his parent then there exists i ∈ [0, 2 s [ such that j = σ(i)

and the link label is X in/2 s (1 + X n/2 s ).

(ii) If the link joins up an L/R-then-M node C (h) j to this parent, then there exists i ∈ [0, 2 h-1 [ such that j = 3σ(i) + 1 and the link label is X n/2 h X in/2 h-1 .

(iii) Let C (h) j be a node which is not an L/R leave neither an L/R-then-M node. Then the link which joins up C (h) j

to his parent has (1 + X n/2 h ) as label.

Since we do not need these three points to be proven in the sequel, we skip this proof here.

The GBR algorithm

We now use the modified reconstruction tree to derive a generalized Bernstein's reconstruction (GBR).

We generalize the scheme used for the modified reconstruction tree of depth 2 given in Subsection 2.2.

We accumulate the values of the modified reconstruction tree, depth by depth, starting from the bottom of the tree. These steps are as follows:

• Step 1: Initialization. We accumulate, in an intermediate value U, the values in the L/R leaves C (s) σ(i) , i = 0, . . . , 2 s -1, multiplied by their respective factors X in 2 s .

August 22, 2012 DRAFT

• A loop on the depth h starting from s and going down to 1, where we perform the three following operations:

-Step 2: Multiplication by the depth factor: we multiply U by (1 + X 2 h ).

-Step 3: Reconstruction of the L/R-then-M terms of depth h. We reconstruct the L/R-then-M terms

C (h)
3σ(i)+1 , i = 0, . . . , 2 h-1 -1, of depth h by applying GBR s-h to the leaves of each sub-tree with root C

n 2 h • X in 2 h-1 .
The above method is specified in Algorithm 1. Proof: We prove the theorem by induction on s. First, since for s = 1 and s = 2 Algorithm 1 corresponds to Bernstein's reconstruction formulas reviewed in Section 2, the induction hypothesis is satisfied for these two cases.

Algorithm 1 GBR s Require: C (s) 0 , . . . , C (s) 3 s -1 Ensure: U = GBR2s (C0, . . . , C3s-1) U ← ( 2 s -1 i=0 C (s) σ(i) X in 2 s ) //Step 1: Initialization for h = s to 1 U ← U × (1 + X n 2 h ) //Step 2: Multiplication of depth h for i = 0 to 2 h-1 -1              //Step 3 : Reconstruction of the L/R-then-M terms j ← 3σ(i) + 1 Vi ← GBR s-h (C (s) 3 s-h j , . . . , C (s) 3 s-h j+3 s-h -1 ) end for U ← U + X n 2 h 2 h-1 -1 i=0
We now assume that Algorithm 1 is valid up to s and we prove its validity for s + 1. Specifically, we have to show that when Algorithm 1 is run with inputs C and C

(1) 2 :

C (0) = (1 + X n/2 )C (1) 0 + X n/2 C (1) 1 + X n/2 (1 + X n/2 )C (1) 2 = (1 + X n/2 ) C (1) 0 + X n/2 C (1) 2 ( * ) +X n/2 C (1) 1 . (11)
Now, by induction hypothesis, if we apply the code in Algorithm 1 for a depth s, it correctly reconstructs

• C

(1)

0 = A (1) 0 × B (1) 0 for n ′ = n/2 and inputs C (s+1) 0 , . . . , C (s+1)
3 s -1 .

• C

(1)

1 = A (1)
1 × B

(1) 1

for n ′ = n ′ /2 and inputs C

(s+1) 3 s , . . . , C (s+1)
2•3 s+1 -1 .

• C

(1)

2 = A (1)
2 × B

(1) 2

for n ′ = n ′ /2 and inputs

C (s+1) 2•3 s , . . . , C (s+1)
3 s+1 -1 . Our strategy is to merge this valid code which computes C

(1) 0 + X n/2 C (1) 2 is given in Algorithm 2.
We have merged the code by performing one simple change: when an accumulation is performed, we accumulate in the same variable U the values corresponding to C

(1) 0 and the values corresponding to

C (1) 2 multiplied by X n/2 . Algorithm 2 Two-Merged GBR s Require: C (s+1) 0 , . . . , C (s+1) 3 s -1 and C (s+1) 2•3 s , . . . , C (s+1) 3 s+1 -1 . Ensure:U = GBRs(C (s+1) 0 , . . . , C (s+1) 3 s -1 ) + X n ′ GBR2,s( (s+1) 2•3 s , . . . , C (s+1) 3 s+1 -1 ) U ← 2 s -1 i=0 C (s+1) σ(i) X in ′ 2 s + X n ′ 2 s -1 i=0 C (s+1) 2•3 s +σ(i) X in ′ 2 s //Merged initializations for h = s to 1 U ← U × (1 + X n ′ 2 h+1 )
//Merged multiplications of depth h

for i = 0 to 2 h-1 -1                  // reconstruction // of the L/R-then-M terms j ← 3σ(i) + 1 Vi ← GBR s-h (C (s+1) 3 s-h j , . . . , C (s+1)
3 s-h j+3 s-h -1 ) V ′ i ← GBR s-h (C (s+1) 2•3 s +3 s-h j , . . . , C (s+1) 2
•3 s +3 s-h j+3 s-h -1 ) end for U ← U + X n ′ 2 h 2 h-1 -1 i=0 ViX in ′ 2 h-1 + X n ′ X n ′ 2 h 2 h-1 -1 i=0 V ′ i X in ′ 2 h-1 //Merged accumulation of //the L/R-then-M terms end for
We now arrange each step of Algorithm 2:

• Modification of the merged initializations. Using the definition of σ in Lemma 1, for each i ∈ {0, 1, . . . , 2 s -1}, we have 2

• 3 s + σ(i) = σ(2 s + i).
We can then arrange the merged initializations step as follows

2 s -1 i=0 C (s+1) σ(i) X in ′ 2 s + X n ′ 2 s -1 i=0 C (s+1) 2•3 s +σ(i) X in ′ 2 s = 2 s -1 i=0 C (s+1) σ(i) X in ′ 2 s + 2 s -1 i=0 C (s+1) σ(2 s +i) X (2 s +i)n ′ 2 s = 2 s -1 i=0 C (s+1) σ(i) X in ′ 2 s + 2 s+1 -1 i=2 s C (s+1) σ(i) X in ′ 2 s = 2 s+1 -1 i=0 C (s+1) σ(i) X in ′ 2 s
August 22, 2012 DRAFT

• Modification of the merged reconstruction of the L/R-then-M terms. We arrange the loop "for i = 0 to 2 h-1 -1" by splitting this loop into two loops: a loop on V i and a loop on V ′ i . For the loop on V i we only change the names of the variables: i becomes i ′ and j becomes j ′ . For the second loop on V ′ i we perform changes in the variables j and i. Specifically, for i we perform the change of variable i ′ = i + 2 h-1 . For the variable j we remark that 2 • 3 s + 3 s-h j = 3 s-h (2 • 3 h + j) which implies that

j ′ = 2 • 3 h + j satisfies j ′ = 2 • 3 h + 3σ(i) + 1 = 3(2 • 3 h-1 + σ(i)) + 1 = 3σ(2 h-1 + i) + 1 = 3σ(i ′ ) + 1.
We obtain the following modified pseudo-code:

for i ′ = 0 to 2 h-1 -1 do j ′ ← 3σ(i ′ ) + 1 V i ′ ← GBR s-h (C (s+1) 3 s-h j ′ , . . . , C (s+1)
3 s-h j ′ +3 s-h -1 ) end for for i ′ = 2 h-1 to 2 h -1 do j ′ ← 3σ(i ′ ) + 1 V ′ i ′ -2 h ← GBR s-h (C (s+1) 3 s-h j ′ , . . . , C (s+1) 3 s
-h j ′ +3 s-h -1 ) end for
The two for loops in the above pseudo-code can then be merged into a single for loop. We just have to rename

V ′ i ′ -2 h-1 by V i ′ , i ′ = 2 h-1 , . . . , 2 h -1.
We obtain the following loop:

for i ′ = 0 to 2 h -1 do j ′ ← 3σ(i ′ ) + 1 V i ′ ← GBR s-h (C (s+1) 3 s-h j ′ , . . . , C (s+1) 3 s-h j ′ +3 s-h -1 ) end for
• Modification of the accumulation of L/R-then-M terms. Here we first need to replace

V ′ i = V ′ i ′ -2 h-1 by V i ′ due
to the former changes and then perform the following simplifications

U + X n ′ 2 h 2 h-1 -1 i ′ =0 V i ′ X i ′ n ′ 2 h-1 + X n ′ X n ′ 2 h 2 h -1 i ′ =2 h-1 V i ′ X (i ′ -2 h-1 )n ′ 2 h-1 = U + X n ′ 2 h 2 h-1 -1 i ′ =0 V i ′ X i ′ n ′ 2 h-1 + X n ′ 2 h 2 h -1 i ′ =2 h-1 V i ′ X i ′ n ′ 2 h-1 = U + X n ′ 2 h 2 h -1 i ′ =0 V i ′ X i ′ n ′ 2 h-1
.

These modifications, along with the change h ′ = h+1 and n ′ = n/2 and the trivial change i = i ′ and j = j ′ results in the following pseudo-code which correctly computes C

(1)

0 +X n/2 C (1) 2 .
U ←

2 s+1 -1 i=0 C (s+1) σ(i) X in 2 s+1 for h ′ = s + 1 to 2 do U ← U × (1 + X n 2 h ′ ) August 22, 2012 DRAFT for i = 0 to 2 h ′ -1 -1 do j ← 3σ(i) + 1 V i ← GBR s+1-h ′ (C (s+1) 3 s+1-h ′ j , . . . , C (s+1) 3 s+1-h ′ j+3 s+1-h ′ -1 ) end for U ← U + X n 2 h ′ 2 h ′ -1 -1 i=0 V i X in 2 h ′ -1

end for

We finally obtain the code of Algorithm 1 for s + 1 by adding the computation U ← (1 + X n/2 )U and U ← U + GBR s (C

(s+1) 3 s , . . . , C (s+1) 2•3 s -1
). But these two operations correspond to h ′ = 1 in the previous pseudo code and the resulting pseudo-code correctly computes C = C (0) 0 as in [START_REF] Zhou | Comments on "A New Architecture for a Parallel Finite Field Multiplier with Low Complexity Based on Composite Field[END_REF]. This concludes the proof on the validity of Algorithm 1.

Complexity evaluation

We evaluate in this subsection the complexity of Algorithm 1 and of the resulting optimized Karatsuba multiplier. We first evaluate the arithmetic complexity of Algorithm 1, i.e., the number of bit additions required in the reconstruction.

Arithmetic complexity of the GBR s algorithm

The number of bit additions performed in Algorithm 1 is denoted as S(n, s). We evaluate this complexity in two steps: we first provide in Lemma 2 a recursive form of the arithmetic complexity of Algorithm 1.

We will then derive a regular non-recursive form of this complexity in a second lemma.

Lemma 2 (Recursive complexity of the GBR 2,s algorithm). The number of bit additions S(s, n) performed in the generalized Bernstein's reconstruction of depth s (Algorithm 1) is as follows

S(s, n) = n + s(2n -1) - n 2 s -2 s+1 + 2 + s i=1 2 i-1 S(s -i, n/2 i ) (12)
Proof: We separately evaluate the cost of the four steps of Algorithm 1.

• Cost of Step 1, the initialization step. We evaluate here the cost of the initialization step U ← (

2 s -1 i=0 C (s) σ(i) X in 2 s ).
We arrange the sum as follows

2 s -1 i=0 C (s) σ(i) X in 2 s =   2 s-1 -1 i=0 C (s) σ(2i) X 2in 2 s   S1 +   2 s-1 -1 i=0 C (s) σ(2i+1) X (2i+1)n 2 s   S2 .
As we can see in

(2 s-1 -1)( 2n 2 s -2) + n 2 s -1 = n -n/2 s -2 s + 1.
August 22, 2012 DRAFT Fig. 7. Evaluation of the cost of the initialization step

C (s) σ(0) C (s) σ(1) C (s) σ(2) C (s) σ(3) C (s) σ(2 s -3) C (s) σ(2 s -1) 0 n 2 s 4n 2 s 3n 2 s C (s) σ(2 s -2) S 1 → S 2 → (2 s-1 -2)n 2 s 2 s-1 n 2 s (2 s-1 -1)n 2 s n 2 s (2 s-1 +1)n 2 s
We can also remark in Fig. 7 that the degree of U after this first step is d I = (2 s + 1) n 2 s -2.

• Cost of Step 2. In this step we sequentially multiply U by 1 + X n/2 h for h = s, s -1, . . . We can then obtain the costs of each multiplication by 1 + X n/2 h for h = s, s -1, . . . , 1 and also the degree of the variable U after each multiplication. These costs and degrees are given in Table 2.

We obtain the total cost of Step 2 after noticing that each multiplication in Table 2 has a cost of

s d I + 1 -n/2 s d I + n/2 s s -1 (d I + 1 + n/2 s ) -n/2 s-1 d I + n/2 s + n/2 s-1 s -2 (d I + 1 + n/2 s + n/2 s-1 ) -n/2 s-2 d I + n/2 s + n/2 s-1 + n/2 s-2 . . . . . . . . . 1 (d I + 1 + n/2 s + n/2 s-1 + • • • + n/4) -n/2 d I + n/2 s + n/2 s-1 + • • • + n/4 + n/2 = 2d I (1 -1 2 s ) Total s(d I + 1 -n/2) August 22, 2012 DRAFT d I + 1 -n/2 s . This implies that the cost of Step 2 is s(d I + 1 -n/2) = s((2 s + 1) n 2 s -1 -n/2 s ) = s(n + n/2 s -1 -n/2 s ) = s(n -1).
/2 h + (2 h-1 -1)n/2 h-1 + 2n/2 h -2 = n + n/2 h -2 which is lower than the degree of U since deg U = d I + n/2 s + n/2 s-1 + n/2 s-2 + • • • + n/2 h = (2 s + 1) n 2 s + n/2 s + n/2 s-1 + n/2 s-2 + • • • + n/2 h = n -2 + n/2 s + n/2 s + n/2 s-1 + n/2 s-2 + • • • + n/2 h = n -2 + n/2 h-1
• Cost of Step 3. For a fixed h we have to reconstruct the 2 h-1 middle terms C (h) 3σ(i)+1 , i = 1, . . . , 2 h-1 -1 using a recursive call to the GBR s-h algorithm. Since, by induction, the GBR s-h algorithm requires S(s -h, n/2 h ), this results in 2 h-1 S(s -h, n/2 h ) bit additions for a given h. Now since h takes all the values among {s, s -1, . . . , 2, 1} and since a reconstruction of depth 0 is free of computation, we conclude that the cost of the recursive reconstructions in the whole algorithm is as follows

s-1 h=1 2 h-1 S(s -h, n/2 h ) = s-1 h ′ =1 2 s-h ′ -1 S(h ′ , n/2 s-h ′ ).
after performing the change h ′ = s -h in the summation variable.

• Cost of Step 4. For each h ∈ {s, s -1, . . . , 2, 1} we add to U the 2 h-1 middle terms C Consequently, there are two types of critical path:

• The blue path goes through one split block and an addition, followed by one CPF of depth s-1, then one multiplier M ult(n/2 s ) and then a reconstruction block of depth s -1 and a final addition. By induction hypothesis, the path which goes through the CPF block of depth s -1 and one multiplier M ult(n/2 s ) and then a reconstruction block of depth s -1 has a delay of (2(s -1) + 1)D ⊕ + D(n/2 s ).

With the initial and final addition, we obtain the following delay for the entire path D = (2s + 1)D ⊕ + D(n/2 s ).

• The red path goes through one CPF of depth s -1 then one multiplier M ult(n/2 s ) and then the merged reconstruction plus the final operations (the multiplication by 1+X n/2 and the last addition).

August 22, 2012 DRAFT

f n = 3 s f n/2 s + cn + d, f 0 = 0 for a fixed s is as follows

f n = 2 s c 3 s -2 s + d 3 s -1 n log 2 (3) - 2 s cn 3 s -2 s - d 3 s -1 .
The results presented in Table 3 show that the generalization of Bernstein's approach provides multipliers with better space complexities. This was the initial goal of Bernstein. But surprisingly this also improves the delay of the multiplier. The results in Table 3 even show that the leading term of the complexities (space and time) slowly approach the leading term of the complexity of the multiplier of Corollary 1. This multiplier achieves the best complexity regarding the leading terms of the space and time complexities.

  . The method of Karatsuba for polynomial multiplication consists of expressing the product C = A × B in terms of three multiplications of polynomial of half size. The detailed computations are given below: August 22, 2012 DRAFT • Component polynomial formation (CPF). The component polynomial formation consists of splitting A in two halves A(X) = three polynomials of half sizeA ′ 0 = A L , A ′ 1 = A L + A H and A ′ 2 = A H . The same is done for B = B L + B H X n/2 : we generate B ′ 0 = B L , B ′ 1 = B L + B H and B ′ 2 = B H .• Recursive products. We perform the pairwise products of the CPF of A and B C

Fig. 3 .

 3 Fig. 3. Modified reconstruction tree of two recursions of the Karatsuba formula

Fig. 4 .

 4 Fig. 4. Component polynomial formation of depth s A =A 0 (0)

  corresponds to the reconstructed product C = A × B. • The intermediate nodes of depth h are labelled as C (h) i

  will be called the left (L) link starting inC (h) i , the link joining C (h) i to C (h+1)3i+2 will be called the right (R) link and the link C

  3i+1 will be called the middle link (M). The reconstruction tree of depth s is shown in Fig.5

Fig. 5 .

 5 Fig. 5. Reconstruction tree of depth s

  the lemma. We now assume that the statement is true for h and we prove it for h + 1. Let C (h+1) j be an L/R node of the reconstruction tree. By definition of an L/R node, all the ancestors of C (h+1) j are also L/R nodes and in particular C

4 :

 4 Accumulation of the reconstructed L/R-then-M terms. We accumulate into U the values of the reconstructed L/R-then-M nodes C (h) 3σ(i)+1 multiplied by their respective factors X

ViX in 2 h- 1 //Step 4 :Theorem 1 ( 3 si 3 s

 14133 Accumulation in U of the L/R-then-M terms end for return(U )The following theorem establishes the validity of Algorithm 1, i.e., that it correctly reconstructs the polynomial C. Validity of Algorithm 1). Let us consider two degree n polynomials A and B where n = 2 s n ′ -1 be their respective component polynomial formation of depth s. Then if C , i = 0, . . . , 3 s -1 are their pairwise products and if Algorithm 1 is run with inputs C -1 , it outputs a polynomial U which satisfies U = A × B.

1 ,

 1 . . . , C (s+1) 3 s+1 -1 it correctly computes August 22, 2012 DRAFT C = A × B. We use for this the following expression of C = C

  in[START_REF] Zhou | Comments on "A New Architecture for a Parallel Finite Field Multiplier with Low Complexity Based on Composite Field[END_REF] and afterwards to derive the code which computes C = C (0) 0 . The merged code computing C

Fig 7 , 1 - 1 )

 711 there are no overlaps in the sums S 1 and S 2 . The computations consists of adding the 2 s-1 terms C of S 2 to S 1 . Since each C (s) σ(j) has size 2n/2 s -1, the addition of the 2 s-1 -1 terms C (s) σ(1) , . . . , C (s) σ(2 s-1 -3) requires 2n 2 s -2 bit additions, and the last term C (s) σ(2 s-1 -1) requires n 2 s -1 bit additions. This leads to the following cost of this step:

, 1 .

 1 Let us denote d I as the initial degree of U . The following diagram shows that the cost of a multiplication of a polynomial U of degree d by 1 + X r requires d + 1 -r bit additions and results in a polynomial of degree d + r.

Remark 3 .

 3 The cost of Step 2 can be independently evaluated from Step 3 and Step 4. Indeed, Step 3 and Step 4 do not change the degree of U : the added polynomial in Step 4 for a depth h has a degree of n

1 n 4 sn -2 s + 1 = 1 i=1 2 Lemma 3 . 1 . 2 )Fig. 8 .Merged

 141123128 Fig. 8. Block decomposition of the multiplier based on merged reconstruction

TABLE 1 Complexity

 1

	Operation			Computations	# XOR	# AND
	CPF			CPF of A CPF of B	n/2 + 3n/4 n/2 + 3n/4	0 0
	Rec. Products.	A	(2) i	• B

evaluation of Bernstein's optimization of two recursions of Karatsuba

  is an L/R node of depth h if the path which starts at the root node and goes to C

	the reconstruction tree of depth s defined as follows.
	Definition 1. Let C	(h) i	be a node of depth h of the reconstruction tree of depth s, then
	(i) We say that C	(h) i	(h) i	uses
	only left (L) or right (R) link at each depth.
	(ii) We call an L/R-then-M node of depth h a node C	(h) i	such that the path which starts from the root node and
	goes down to C	(h) i	uses only left or right link at each depth unless the last link between the middle term C	(h) i
	August 22, 2012				DRAFT

TABLE 2

 2 Cost evaluation of Step 2

	Level	Cost	Resulting degree

Proof: We proceed to the proof of (14) using an induction proof. Specifically, we denote the term γ(s, n) = n + s(2n -1) -n 2 s -2 s+1 + 2 which appears in (13) and

the expression in the right side of (14). Proving that the two expressions of S(n, s) of ( 14) and (13) are equals is equivalent to prove that

We prove that this latter equality is true it by induction on s. For s = 1 this can be checked directly using the material of Section 2. We assume that ( 14) and ( 16) are true up to s -1 and we show that they are also true for s. We begin by rewriting the sum in the left side of (16) as follows

This latter identity is obtained by setting s ′ = s -1 and n ′ = n/2. We apply the induction hypothesis (16) to the sum

Now, we separately arrange the terms 3ρ(s -1, n/2) and 2γ(s -1, n/2). We replace ρ(s -1, n/2) by the corresponding expression in terms of n and s given in (15):

Similarly we treat the term 2γ(s -1, n/2) in the same way

We finally replace in (17) the new expression of 3ρ(s -1, n/2) and 2γ(s -1, n/2). We obtain, after some simplifications, that s,n) and this ends the proof.

August 22, 2012 DRAFT

Complexities of the parallel multiplier based on GBR s

We consider a parallel multiplier which consists of:

• Two parallel circuits preforming the recursive CP F of depth s for the two inputs A and B.

• 3 s parallel multipliers of polynomial of degree n/2 s which compute

• A reconstruction based on Algorithm 1: the bit additions performed in Step 1, 2 and 4 are performed with parallel XOR gates and the recursive reconstructions in Step 3 are all performed in parallel.

The space and time complexities of this multiplier is established in Lemma 4.

Lemma 4. The space complexity consists of the number of XOR gates, denoted as S ⊕ (n), and the number of AND gates, denoted as S ⊗ (n). The space complexity and the delay of the considered parallel multiplier are as follows

Proof: Evaluation of the space complexity.The number of XOR gates is the sum of the number of XOR gates of the two parallel recursive CPFs of depth s and the 3 s multipliers of degree n/2 s polynomials and the reconstruction of depth s. The number of AND gates is simply equal to 3 s S ⊗ (n/2 s ). Based on Fig. 4, we note that the number of XOR gates S CP F,⊕ (n) of a CPF of depth s satisfies

We then use the number of XOR gates of the reconstruction of depth s given in (14) to derive the following recursive expression of the space complexity of the proposed multiplier

After some simplifications we obtain the required expression (18) of the space complexity.

Evaluation of the delay. We show by induction on s that the expression in (18) is true. We assume that the delay in (18) is true up to s -1 and we show it for s. For this we decompose the multiplier in the following blocks:

• Decomposition of the recursive CPF block of depth s. We re-express the CPF of depth s by applying one recursion of Karatsuba formula and then three blocks of CPF of depth s -1. We do this for the two CPF blocks of A and B.

• Decomposition of the GBR of depth s. We decompose the reconstruction block of depth s based on the method used in the proof of Theorem 1. We split the reconstruction block in one merged

COMPLEXITY COMPARISON AND CONCLUSION

We have presented in the previous section a generalization of Bernstein's optimization of the Karatsuba reconstruction. This optimization can be used to any depth s in the reconstruction. One interesting case is when we apply this approach to the full recursive reconstruction. In the following corollary we give the complexity of the multiplier based on this approach.

Corollary 1. If we design a parallel Karatsuba multiplier with a generalized Bernstein's reconstruction of depth s = log 2 (n), i.e., the GBR is applied to the full recursive reconstruction, we obtain a multiplier with the following complexity:

The complexity stated in the above corollary is a direct consequence of Lemma 4. In


Isabelle Mirbel
email: isabelle.mirbel@unice.fr

Serena Villata
email: serena.villata@inria.fr

Enhancing Goal-based Requirements Consistency: an Argumentation-based Approach

Requirements engineering research has for long recognized the leading role of goals as requirement artifacts during the requirements engineering specification processes. Given the large number of artifacts created during the requirements specification and the continuous evolution of these artifacts, reasoning about them remains a challenging task. Moreover, the rising complexity of the target domain under consideration during the requirements engineering process as well as the growth of geographically distributed projects explain why the number of collected requirements as well as their complexity also increase. In this context, providing support to stakeholders in achieving a common understanding of a set of goal-based requirements, in consolidating them and keeping them consistent over time is another challenging task. In this paper, we propose an approach to detect consistent sets of goal-based requirements and maintain their consistency over time. Our approach relies on argumentation theory which allows to detect the conflicts among elements called arguments. In particular, we rely on meta-argumentation, which instantiates abstract argumentation frameworks, where requirements are represented as arguments and the standard Dung-like argumentation framework is extended with additional relations between goal-based requirements.

Introduction

Requirements engineering (RE) research has for long recognized the leading role of goals during the requirements engineering processes. Several goal-oriented requirements engineering approaches have been proposed in the literature [START_REF] Yu | Towards Modelling and Reasoning Support for Early-Phase Requirements Engineering[END_REF][START_REF] Bresciani | Modeling early requirements in Tropos: a transformation based approach[END_REF][START_REF] Amyot | User Requirements Notation: The First Ten Years, The Next Ten Years[END_REF][START_REF] Rolland | A Multi-Model View of Process Modelling[END_REF]. Goals have shown to be useful for achieving requirements completeness, avoiding irrelevant requirements, explaining requirements to stakeholders, structuring complex requirements documents through goal refinement, supporting decision making through alternative goal refinements, managing conflicts among multiple viewpoints, separating stable from more volatile information and driving requirements identification [START_REF] Van Lamsweerde | Goal-Oriented Requirements Engineering: A Guided Tour[END_REF].

As it has been highlighted in Pohl [START_REF] Pohl | Requirements Engineering. Fundamentals, Principles, and Techniques[END_REF], given the large number of artifacts created during the requirements engineering process and the continuous evolution of these artifacts, managing and organizing requirements artifacts is a challenging task. The rising complexity of the target domain under consideration during the requirements engineering process also increases the number of collected requirements as well as their inter-dependencies and it makes this task much more challenging. Dedicated tools are required to support stakeholders in achieving a common understanding of a set of requirements, in consolidating it and in keeping it consistent over the whole project life cycle. As it has been highlighted in the literature [START_REF] Van Lamsweerde | Goal-Oriented Requirements Engineering: A Guided Tour[END_REF], even if inconsistencies may be desirable, for instance to allow further elicitation of requirements that would have been missed otherwise, their resolution is necessary at some point. Tools are required to highlight inconsistencies and to support stakeholders who will handle the resolution process. Requirements are usually provided by different groups of stakeholders. This means that we cannot just consider a set of requirements as correct or not. When a requirement is suitable for a group of stakeholders, this leads to the removal of other requirements in order to keep the full requirements set consistent. If this requirement is discovered as not so important for another group of stakeholders, it is therefore removed from the full requirements set to insure consistency from their point of view.

Different kinds of relationships hold between goals [START_REF] Pohl | Requirements Engineering. Fundamentals, Principles, and Techniques[END_REF]. For instance, goal decomposition relationships are distinguished from goal dependencies, i.e., two kinds of decomposition are possible depending on the fact that all subgoals are required to satisfy a super-goal (AND-decomposition) or at least one subgoal (OR-decomposition). The following dependencies have been identified [START_REF] Pohl | Requirements Engineering. Fundamentals, Principles, and Techniques[END_REF]: equivalence, conflict, and require. This paper focuses on the modeling of goal-based requirements with the aim to support the stakeholders, i.e., the agents, in detecting inconsistent sets of requirements and solving these inconsistencies. We propose to use well-known Dung-like abstract argumentation [START_REF] Dung | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF] to reason about the consistency of a set of goal-oriented requirements. Dung-like abstract argumentation models the information as abstract elements called arguments. The arguments are linked to each others by an attack relation. Therefore, we present a way to model additional goal-based relations, to detect the inconsistencies among goals, and provide a decision support system for their resolution.

Following the idea proposed by Bagheri and Ensan [START_REF] Bagheri | Consolidating multiple requirement specifications through argumentation[END_REF], we propose an approach in which consistent subsets of requirements are provided to the stakeholders to allow them to understand the different units of consistent requirements. As it has been highlighted in Bagheri and Ensan [START_REF] Bagheri | Consolidating multiple requirement specifications through argumentation[END_REF], the use of abstract argumentation is reasonable because it does not need the requirements to be formally defined and only needs the relationships between the requirements to be defined. With respect to the work of Bagheri and Ensan [START_REF] Bagheri | Consolidating multiple requirement specifications through argumentation[END_REF], which concentrates on the conflict relation, in our approach we take into consideration all the relations required to organize goals, i.e., AND/OR-decomposition, conflict, require and equivalence dependencies. Therefore, we rely on meta-argumentation [START_REF] Boella | On the Acceptability of Meta-arguments[END_REF][START_REF] Boella | Meta-Argumentation Modelling I: Methodology and Techniques[END_REF] which has been proposed as a general methodology to handle the introduction of new relations among the arguments by reusing Dung's theory and results.

Alternative approaches to argumentation theory are for instance Answer Set Programming, and first-order logic [START_REF] Goknil | Semantics of trace relations in requirements models for consistency checking and inferencing[END_REF]. As underlined by Bagheri and Ensan [START_REF] Bagheri | Consolidating multiple requirement specifications through argumentation[END_REF], a drawback of pure logical formalisms for dealing with inconsistency in requirement specifications is that they identify and solve the inconsistency in pure syntactic form without taking into account the semantical information required to solve inconsistency. The advantage of using argumentation theory is twofold: first, argumentation theory provides a formal but intuitive technique to reason over inconsistency allowing the detection of the implicit relationships among the arguments and their inconsistencies, and second it allows the stakeholders to choose among different sets of consistent requirements using acceptability semantics [START_REF] Dung | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF] with the possibility of specifying whether the choice of the consistent set of requirements has to be guided by skeptical or credulous semantics.

The paper is organized as follows. In Section 2, we discuss why and how argumentation is helpful to check the consistency in requirements engineering. In Section 3, we detail how the different goals decomposition relationships and goals dependencies are modeled in our framework. In Section 4, we illustrate our proposal with an example. Section 5 compares the proposed approach to the related work. Finally, we conclude and give some perspectives.

Meta-argumentation: overview

We provide the basic concepts of Dung's abstract argumentation [START_REF] Dung | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF]. A Dungstyle argumentation framework [START_REF] Dung | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF] aims at representing conflicts among elements called arguments. It allows to reason about these conflicts in order to detect, starting by a set of arguments and the conflicts among them, which are the accepted arguments. The accepted arguments are those arguments which are considered as believable by an external evaluator, who has a full knowledge of the argumentation framework. A Dung-style framework is based on a binary attack relation among arguments, whose role is determined only by their relation to other arguments. Dung [START_REF] Dung | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF] presents several acceptability semantics that produce zero, one, or several sets of accepted arguments. The set of accepted arguments of an argumentation framework consists of a set of arguments that does not contain an argument attacking another argument in the set. Roughly, an argument is accepted if all the arguments attacking it are rejected and it is rejected if it has at least an argument attacking it which is accepted. The (possibly multiple) set of accepted arguments computed using one of the acceptability semantics are called extensions.

Definition 1 (Argumentation framework AF

). An argumentation framework is a tuple A, → where A is a finite set of elements called arguments and → is a binary relation called attack defined on A.

A semantics of an argumentation theory consists of a conflict free set of arguments cf (S), i.e., a set of arguments that does not contain an argument attacking another argument in the set. Like Baroni and Giacomin [START_REF] Baroni | On principle-based evaluation of extension-based argumentation semantics[END_REF], we use a function E called acceptance function mapping an argumentation framework A, → to its set of extensions, i.e., to a set of sets of arguments.

Definition 2 (Acceptance function). Let U be the universe of arguments. An acceptance function E : 2 U × 2 U ×U → 2 2 U is a partial function which is defined for each argumentation framework A, → with finite A ⊆ U and →⊆ A × A, and maps an argumentation framework A, → to sets of subsets of A:

E( A, → ) ⊆ 2 A .
The following definition summarizes the most widely used acceptability semantics of arguments [START_REF] Dung | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF]. -S ∈ E admiss (AF ) iff cf(S) and S ⊆ D(S).

-S ∈ E compl (AF ) iff cf(S) and S = D(S).

-S ∈ E ground (AF ) iff S is smallest in E compl (AF ). -S ∈ E pref (AF ) iff S is maximal in E admiss (AF ). -S ∈ E stable (AF ) iff cf(S) and ∀b ∈ A\S ∃a ∈ S : a → b.

Meta-argumentation

Meta-level argumentation has been proposed in several works [START_REF] Jakobovits | Robust semantics for argumentation frameworks[END_REF][START_REF] Baroni | Argumentation framework with recursive attacks[END_REF][START_REF] Cayrol | Coalitions of arguments: A tool for handling bipolar argumentation frameworks[END_REF][START_REF] Modgil | Metalevel argumentation[END_REF] and further developed with different goals. Boella and colleagues [START_REF] Boella | On the Acceptability of Meta-arguments[END_REF][START_REF] Boella | Meta-Argumentation Modelling I: Methodology and Techniques[END_REF], in particular, proposed the meta-argumentation methodology where extended argumentation frameworks are instantiated with meta-arguments, and reasoning in the meta-level is allowed without the need to extend Dung-like abstract framework. Meta-argumentation instantiates Dung's theory with meta-arguments, such that Dung's theory is used to reason about itself [START_REF] Boella | Meta-Argumentation Modelling I: Methodology and Techniques[END_REF][START_REF] Modgil | Metalevel argumentation[END_REF]. Meta-argumentation is a particular way to define mappings from argumentation frameworks to extended argumentation frameworks: arguments are interpreted as meta-arguments, of which some are mapped to "argument a is accepted", acc(a), where a is an abstract argument from the extended argumentation framework EAF . Moreover, auxiliary arguments are introduced to represent, for example, attacks, so that, by being arguments themselves, they can be attacked or attack other arguments.

The function f assigns to each argument a in the EAF , a meta-argument "argument a is accepted" in the basic argumentation framework. The function f -1 instantiates an AF with an EAF . We use Dung's acceptance functions E to find functions E between EAF s and the acceptable arguments AA they return. The accepted arguments of the meta-argumentation framework are a function of the EAF AA = E (EAF ). The transformation function consists of two parts: the function f -1 , transforming an AF to an EAF , and a function g which transforms the acceptable arguments of the AF into acceptable arguments of the EAF . Summarizing

E = {(f -1 (a), g(b)) | (a, b) ∈ E} and AA = E (EAF ) = g(AA) = g(E(AF )) = g(E(f (EAF ))).
The first step of the meta-argumentation approach is to define the set of EAF s. The second step consists of defining flattening algorithms as a function from this set of EAF s to the set of all basic AF : f : EAF → AF . The inverse of the flattening is the instantiation of the AF . See [START_REF] Boella | Meta-Argumentation Modelling I: Methodology and Techniques[END_REF] for further details. Given an acceptance function E for an AF , the extensions of accepted arguments of an EAF are given by

E (EAF ) = g(E(f (EAF ))). The derived accep- tance function E of the EAF is thus E = {(f -1 (a), g(b)) | (a, b) ∈ E}.
Definition 5 presents the instantiation of a basic AF using meta-argumentation.

Definition 5. Given an EAF

= A, → where A ⊆ U is a set of arguments, and →⊆ A × A. M A ⊆ M U is {acc(a) | a ∈ U } ∪ {X a,b , Y a,b | a, b ∈ U}, and -→⊆ M A×M A is a binary relation on M A such that: acc(a) -→ X a,b , X a,b -→ Y a,b , Y a,b -→ acc(b) if and only if a, b ∈ A and a → b ∈→.
Intuitively, the X a,b auxiliary argument means that the attack a → b is "inactive", and the Y a,b auxiliary argument means that the attack is "active". An argument of an EAF is accepted iff it is accepted in the flattened AF .

In our approach, we propose to model decomposition relationships and dependencies as a meta-argumentation framework dedicated to goal-based requirements engineering. Goals are modeled as meta-arguments and decomposition relationships and dependencies as relations among them. Thanks to the semantics assigned to each of the decomposition relationships and dependencies introduced, mappings to the argumentation framework are possible as well as reasoning to find consistent subsets of goals, i.e., extensions of the argumentation framework. In the next sections, we illustrate our proposal with the help of an example extracted from Pohl [START_REF] Pohl | Requirements Engineering. Fundamentals, Principles, and Techniques[END_REF].

Goal decomposition and dependencies

Requirements engineering is generally viewed as a process consisting of four core activities: elicitation, analysis, negotiation and validation. Each activity produces information which must be made persistent by documenting it in the right way. In order to facilitate communication, to support negotiation or to provide basis for a contract, for deriving manuals or for project planning for instance, requirements are traditionally defined in a requirement document or database. Requirements artifacts can be documented using natural language or a conceptual modeling language. Goals [START_REF] Van Lamsweerde | Goal-Oriented Requirements Engineering: A Guided Tour[END_REF] are proposed for this purpose. Goals aim at capturing the rationale of the software systems and document agents' intentions. Regardless of the chosen means to document requirements, they appear closely related to each other.

According to the literature review presented in Pohl [START_REF] Pohl | Requirements Engineering. Fundamentals, Principles, and Techniques[END_REF], different kinds of relationships hold between goals. Goal decomposition relationships are distinguished from goal dependencies. Two kinds of decomposition are possible depending on the fact that all subgoals are required to satisfy a super-goal (ANDdecomposition) or at least one sub-goal (OR-decomposition). With regards to dependencies, equivalence, conflict, obstruction, support and require relationships have been identified. Obstruction and support aim at eliciting partial dependencies between goals. Therefore we do not take them into account in our current framework in which we only reason on crisp acceptance, and not on partial acceptance. This is left as future work.

In our approach, we rely on the meta-argumentation methodology to formally model the requirements and these main relationships among them. We choose the meta-argumentation methodology because it allows to model extended argumentation frameworks, i.e., argumentation frameworks where additional relations among the arguments are introduced, as Dung-like abstract frameworks in order to reuse Dung's properties and theorems. We define an extended argumentation framework for reasoning about requirements as follows:

Definition 6 (Requirement-based EAF ). A requirement-based extended argumentation framework REAF is a tuple A, →, CF, RQ, AND-dec, OR-dec, EQ where A ⊆ U is a set of requirements, →⊆ A × A, CF is a binary conflict relation on A (CF ⊆ A × A), RQ is a binary requires relation on A (RQ ⊆ A × A), AN D -dec is a AND-decomposable relation on

2 A × A (AN D -dec ⊆ 2 A × A), OR -dec is a OR-decomposable relation on 2 A × A (OR -dec ⊆ 2 A × A),
and EQ is a binary equivalence relation on A (EQ ⊆ A × A). The universe of meta-requirements is Roughly, the extensions of the REAF contain the set of requirements that do not conflict with each other and that satisfy the constraints posed by the other relations.

M U = {acc(a) | a ∈ U} ∪ {X a,b , Y a,b | a, b ∈ U} ∪ {Z a,b | a, b ∈ U } ∪ {R a,b | a, b ∈ U } ∪ {T a,b | a, b ∈ U },

Goal decomposition

Two kinds of goal decomposition have been identified in the literature [START_REF] Pohl | Requirements Engineering. Fundamentals, Principles, and Techniques[END_REF]. In the following we explain how we model them in our meta-argumentation framework.

AND-decomposition. Pohl [START_REF] Pohl | Requirements Engineering. Fundamentals, Principles, and Techniques[END_REF] defines the AND-decomposition in the following way: The decomposition of a super-goal into a set of sub-goals is an AND-decomposition if and only if all sub-goals must be satisfied in order to satisfy the super-goal.

We model the AND-decomposition relationship in meta-argumentation as follows: a super-goal to be accepted has to have all its sub-goals accepted. The idea is that all the sub-goals are represented as meta-requirements in the meta-level. They attack meta-requirement T which attacks the meta-requirement representing the super-goal. Meta-requirement T is not connected to a real requirement in the object level, but as previously noticed for X and Y , it is just used to reason in the meta-level. The formalization of the AND-decomposition relation is presented in Definition 7. This is similar to the representation of a conjunctive pattern of arguments, as discussed by Villata et al. [START_REF] Villata | Argumentation Patterns. 8th International Workshop on Argumentation in Multi-Agent Systems[END_REF]. In this way, we have that the goal G is accepted only if all the sub-goals are accepted too. If one (or more) sub-goal is not accepted, then the respective meta-requirement T i is accepted, and given the attack of this meta-requirement against the super-goal, the super-goal is made unacceptable. An example of AND-decomposition is shown in Figure 1, where both goals G1 and G2 need to be accepted to have goal G3 accepted.

Definition 7. Given a REAF = A, →, CF, RQ, AN D -dec, OR -dec, EQ , the set of meta-arguments M A ⊆ M U is {acc(a) | a ∈ U } ∪ {X a,b , Y a,b | a, b ∈ U} ∪ {Z a,b | a, b ∈ U} ∪ {R a,b | a, b ∈ U} ∪ {T a,b | a, b ∈ U} and -→⊆ M A × M A is a binary relation on M A such that: -acc(r 1 ) -→ T r1,a iff a AN D -dec r 1 , . . . ,
Proposition 1 (Semantics of AND-dec). Given a REAF , if it holds that a 1 , . . . , a n AN D-dec b and all goals a 1 , . . . , a n are accepted then goal b is accepted too.

Proof. We prove the contrapositive. If it holds that a 1 , . . . , a n AN D -dec b and goal b is rejected, then goals a 1 , . . . , a n are rejected too. Assume a 1 , . . . , a n AN Ddec b and assume that meta-requirement acc(b) is rejected, then there exists at least one meta-requirement T a1 , . . . , T an that is accepted. Consequently, at least one meta-requirement acc(a 1 ), . . . , acc(a n ) is rejected. OR-decomposition. Pohl [START_REF] Pohl | Requirements Engineering. Fundamentals, Principles, and Techniques[END_REF] defines the OR-decomposition in the following way: The decomposition of a super-goal into a set of sub-goals is an ORdecomposition if and only if satisfying one of the sub-goals is sufficient for satisfying the super-goal. We model the OR-decomposition relationship in meta-argumentation as follows: a super-goal to be accepted needs to have at least one of its sub-goals accepted. The idea is that all the sub-goals in the meta-level attack the same meta-requirement R which attacks the meta-requirement representing the supergoal. In this way, we have that the goal G is accepted when at least one of its subgoals is accepted too. If no sub-goal is accepted, then the meta-requirement R is accepted, and given the attack of this meta-requirement against the super-goal, the super-goal is made unacceptable. The formalization of the OR-decomposition relation is presented in Definition 8. Definition 8. Given a REAF = A, →, CF, RQ, AN D -dec, OR -dec, EQ , the set of meta-arguments

M A ⊆ M U is {acc(a) | a ∈ U } ∪ {X a,b , Y a,b | a, b ∈ U} ∪ {Z a,b | a, b ∈ U} ∪ {R a,b | a, b ∈ U} ∪ {T a,b | a, b ∈ U} and -→⊆ M A × M A is a binary relation on M A such that:
acc(r 1 ) -→ R r,a iff a OR -dec r 1 , . . . , r n , and -. . . acc(r n ) -→ R r,a iff a OR -dec r 1 , . . . , r n , and -R r,a -→ acc(a) iff a OR -dec r 1 , . . . , r n .

An example of OR-decomposition is shown in Figure 2, where either goal G1 or goal G2 need to be accepted to have goal G3 accepted.

Goal dependencies

Different kinds of dependencies between goals have been identified in the literature [START_REF] Pohl | Requirements Engineering. Fundamentals, Principles, and Techniques[END_REF]. In the following, we explain how we model the conflict, requires and equivalence dependencies in our extended argumentation framework.

Conflict dependency. Pohl [START_REF] Pohl | Requirements Engineering. Fundamentals, Principles, and Techniques[END_REF] defines the conflict dependency in the following way: a conflict dependency exists between two goals if the satisfaction of one goal entirely excludes the satisfaction of the other goal, and vice versa.

In Definition 9, we present how to model the conflicts among requirements. The two meta-requirements X and Y are used to model the conflict relation in the meta-level as well as the attack relation. The semantics of the conflict dependency is similar to the semantics of the attack relation in Dung-style abstract argumentation. The difference is that the attack relation is directed from an argument to another argument while the conflict dependency leads to a cycle of attacks, i.e., the two arguments attack each other. An example of conflict dependency is shown in Figure 3, where goal G1 cannot be accepted if goal G2 is accepted and vice versa. In particular, the three extensions using complete semantics are {G1}, {G2}, and ∅. Require dependency. Pohl [START_REF] Pohl | Requirements Engineering. Fundamentals, Principles, and Techniques[END_REF] defines the require dependency in the following way: a goal G 1 is related to a goal G 2 by a requires dependency if the satisfaction of the goal G 2 is a prerequisite for satisfying goal G 1 .

We model the requires relation as a relation such that, given that G 1 requires G 2 , G 1 is accepted only if G 2 is accepted too. This means that if G 2 is not accepted, then G 1 is not accepted either. We formalize the requires relation using meta-argumentation in Definition 10. Definition 10 highlights that goals cannot only conflict with each other but can also require the acceptability of other goals to be themselves accepted. The requires relation is defined following the example of the modeling in metaargumentation of the support relation [START_REF] Boella | Support in abstract argumentation[END_REF]. An example of requires dependency is shown in Figure 4, where the goal G1 needs goal G2 accepted to be accepted too. Proposition 2 (Semantics of requires). Given a REAF , if it holds that a RQ b and goal a is accepted, then goal b is accepted too.

Definition 10. Given a

REAF = A, →, CF, RQ, AN D -dec, OR -dec, EQ , the set of meta-arguments M A ⊆ M U is {acc(a) | a ∈ U } ∪ {X a,b , Y a,b | a, b ∈ U} ∪ {Z a,b | a, b ∈ U} ∪ {R a,b | a, b ∈ U} ∪ {T a,b | a, b ∈ U} and -→⊆ M A × M A is a
Proof. We prove the contrapositive. If it holds that a RQ b and goal b is not accepted, then goal a is not accepted. Assume that a RQ b and assume that meta-requirement acc(b) is not accepted, then meta-requirement Z a,b is accepted. Consequently, meta-requirement acc(a) is not accepted. Proof. We use reasoning by cases. Case 1: acc(c) is accepted, then acc(a) is not accepted, follows from Proposition 2, and given c → b, c → a can be deleted without changing the extension. Case 2: acc(c) is not accepted, then acc(a) is accepted, and the attack relation c → a can be avoided.

Goal equivalence. Pohl [START_REF] Pohl | Requirements Engineering. Fundamentals, Principles, and Techniques[END_REF] defines the goal equivalence in the following way: An equivalence dependency exists between two goals if the satisfaction of one goal implies the satisfaction of the other goal. We model the equivalence dependency in the following way: given that G1 is equivalent to G2 then if G 1 is in conflict with other goals, then G 2 is in conflict with these other goals too, and if goal G 2 is in conflict with other goals, then goal G 1 conflicts with these goals too. In order to maintain the semantics of the equivalence dependency, we have to consider how to manage the conflicts addressed against goal B when goal A is equivalent to B. In this case, we want to model the situation such that every time goal B is in conflict with another goal, then this new goal is in conflict also with A and vice-versa. We achieve it by introducing an additional kind of conflict among the goals called equivalence attacks.

An example of equivalence dependency is shown in Figure 5. In this example, G 1 is conflicting with G 3 then G 3 is also conflicting with G 2 as it is shown by the dashed lines. And if a conflict involving G 2 would exist, then G 1 would also be in conflict with this goal. We do not include this case in the figure for clarity purpose. In the following section, we introduce an example including the different kinds of decomposition and dependency relationships previously discussed to show the effectiveness of our approach.

Example

To show how the translations of the different relationships existing between goals are combined into our extended argumentation framework, an example of goaloriented requirements modeling is presented in Figure 6. In this example, there is a conflict between G 6 and G 11 . Therefore the mapping to our meta-argumentation framework leads to 2 extensions in complete semantics: the former in which G 6 is accepted and G 11 not accepted; and the latter in which G 11 is accepted and G 6 is not accepted 3 .

Figure 7 shows the representation in the meta-level of the example from Figure 6. In this framework, we show the first extension, where G 6 is accepted and G 11 is rejected. For clarity of the figure, we duplicated the meta-requirement acc[G11]. The set of goals in grey corresponds to a coherent set of goals. No goal represented in white can be added to this set without making it inconsistent. Note that only meta-requirements representing the goals are requirements in the object level. Figure 8 shows the set of accepted goals on the goal hierarchy corresponding to this first extension. 7. The meta-argumentation framework and the extension where goal G6 is accepted.

acc[G17] acc[G3] acc[G5] acc[G6] acc[G7] acc[G9] acc[G10] acc[G12] acc[G13] acc[G14] acc[G15] acc[G16] acc[G18] T T T T Y X Fig.
The second extension starting from the goal-oriented requirement modeling of Figure 6 is shown in Figure 9. In this extension, G 11 is accepted and G 6 is not accepted. Again, meta-requirement acc[G11] is duplicated for clarity reasons. No goal represented in white can be added to the set without making it inconsistent. Figure 10 shows the set of accepted goals on the goal hierarchy corresponding to the second extension.

As it is shown by this running example, we propose an approach in which consistent subsets of an initial goals set are provided to the stakeholders to allow them to understand the different units of consistent goals. This is particularly useful when the number of collected requirements as well as the number of inter-dependencies are big. In this context, our approach aims at supporting stakeholders in achieving a common understanding of a set of goal-based re-and on its notion of acceptability semantics to assess which are the acceptable requirements, instead of introducing a new framework; second, we reason at the pure abstract level as done by Bagheri and Ensan [START_REF] Bagheri | Consolidating multiple requirement specifications through argumentation[END_REF] starting from the set of goalbased requirements and their relationships, we are not interested in modeling the discussions of the stakeholders to verify the validity of an artifact using a propositional language; third, we do not consider only the conflict and the preference relationships among the requirements, but we consider goal-based requirements and their additional relationships (AND/OR-decomposition, and require, conflict and equivalence goal dependencies) provided by the stakeholders to detect the (possibly multiple) consistent sets of requirements, showing in addition how the inconsistencies may be resolved. Ingolfo et al. [START_REF] Ingolfo | Establishing Regulatory Compliance for Software Requirements[END_REF] use the ACE framework to deal with the compliance of software requirements. In Goknil et al. [START_REF] Goknil | Semantics of trace relations in requirements models for consistency checking and inferencing[END_REF], a meta model is proposed to reason about requirements consistency. In their approach, some well-known relationships between requirements are formalized by relying on first-order logic. Thanks to this meta model, implicit relations and inconsistencies are detected. We propose to address this issue by using abstract argumentation theory in order to put in evidence consistent sets of requirements.

Conclusion

In this paper we present an approach to support consistency checking in goalbased requirements engineering. Our approach aims at detecting implicit relationships between the requirements and checking the possible inconsistencies among them.

Our proposal uses argumentation theory to formalize the requirement and their relationships, and to detect the inconsistencies. We represent requirements as abstract arguments and the conflicts among the requirements are the conflicts among the arguments. In particular, we rely on the meta-argumentation methodology to formally model the decomposition and dependencies which may exist between goals. We choose the meta-argumentation methodology because it allows to model argumentation frameworks with additional relations among the arguments as Dung-like abstract frameworks thus reusing Dung's properties and algorithms.

Several open challenges will be addressed as future works. First, we are developing a tool which asks the stakeholders to enter the set of requirements and the relationships among them, and it returns a graphical visualization of the requirements, as shown in Figure 6 and7. The tool highlights the set of consistent requirements, and provides the stakeholder with the possible alternatives. These alternatives depend on the chosen acceptability semantics. Second, we plan to introduce into the framework also the relationships between agents and the requirements they propose. This has to be done to be able to reason about trust, allowing the expression of different evaluations of the acceptability of the arguments depending on the stakeholder who is proposing them [START_REF] Villata | Arguing about the Trustworthiness of the Information Sources[END_REF]. Third, we plan to use fuzzy values expressing the degree of acceptability of the arguments to take into account partially satisfied goals [START_REF] Da Costa Pereira | Changing ones mind: Erase or rewind?[END_REF], as it is necessary to model the obstruction and support relationships. Moreover, we plan to address dynamical issues such as changes in the set of requirements and goals, which are common in most engineering projects. Finally, we will investigate the cost associated with argumentation-based approaches to software engineering.

Definition 3 (

 3 Acceptability semantics). Let AF = A, → be an argumentation framework. Let S ⊆ A. S defends a if ∀b ∈ A such that b → a, ∃c ∈ S such that c → b. Let D(S) = {a | S defends a}.

Definition 4 .

 4 An extended argumentation framework EAF is a tuple A, → where A ⊆ U is a set of arguments, and → is a binary attack relation on A. The universe of meta-arguments is M U = {acc(a) | a ∈ U} ∪ {X a,b , Y a,b | a, b ∈ U}, where X a,b , Y a,b are the meta-arguments corresponding to the attack a → b. The flattening function f is given by f (EAF ) = M A, -→ , where M A is the set of meta-arguments and -→ is the meta-attack relation. For a set of arguments B ⊆ M U , the unflattening function g is given by g(B) = {a | acc(a) ∈ B}, and for sets of subsets of arguments AA ⊆ 2 M U , it is given by g(AA) = {g(B) | B ∈ AA}.

  where X a,b , Y a,b are the metarequirements corresponding to the conflict relation (a CF b), Z a,b is the metarequirement corresponding to the requires relation (a RQ b), R a,b is the metarequirement corresponding to the OR-decomposable relation (a OR -dec b), and T a,b is the meta-requirement corresponding to the AND-decomposable relation (a AN D -dec b). The flattening function f is given by f (EAF ) = M A,-→, where M A is the set of meta-requirements and -→ is the meta-conflict relation. For a set of requirements B ⊆ M U , the unflattening function g is given by g(B) = {a | acc(a) ∈ B}, and for sets of subsets of requirements AA ⊆ 2 M U , it is given by g(AA) = {g(B) | B ∈ AA}.

  r n , and -. . . acc(r n ) -→ T rn,a iff a AN D -dec r 1 , . . . , r n , and -T r1,a -→ acc(a) iff a AN D -dec r 1 , . . . , r n , and -. . . -T rn,a -→ acc(a) iff a AN D -dec r 1 , . . . , r n .

Fig. 1 .

 1 Fig. 1. Example of AND-decomposition. Accepted meta-requirements are represented in grey and rejected meta-requirements in white.

Fig. 2 .

 2 Fig. 2. Example of OR-decomposition.

Definition 9 .

 9 Given a requirement-based extended argumentation framework REAF = A, →, CF, RQ, AN D-dec, OR-dec, EQ , the set of meta-requirements M A ⊆ M U is {acc(a) | a ∈ U}∪{X a,b , Y a,b | a, b ∈ U}∪{Z a,b | a, b ∈ U}∪{R a,b | a, b ∈ U} ∪ {T a,b | a, b ∈ U} and -→⊆ M A × M A is a binary relation on M A such that: acc(a) -→ X a,b iff a CF b and -X a,b -→ Y a,b iff a CF b and -Y a,b -→ acc(b) iff a CF b and acc(b) -→ X b,a iff a CF b and -X b,a -→ Y b,a iff a CF b and -Y b,a -→ acc(a) iff a CF b.

Fig. 3 .

 3 Fig. 3. Example of conflict dependency where the extension {G1} is shown.

  binary relation on M A such that: acc(b) -→ Z a,b iff a RQ b, and -Z a,b -→ acc(a) iff a RQ b.

Fig. 4 .

 4 Fig. 4. Example of requires dependency.

Proposition 3 . 4 . 4 .

 344 Given a REAF with goals a, b and c, if there is an attack such that a → c if a RQ b and b → c, then the extensions do not change, using our meta-argumentation model and one of Dung's semantics. Proof. We use reasoning by cases. Case 1: acc(a) is accepted, then also acc(b) is accepted following Proposition 2, and given b → c, a → c can be deleted without changing the extension. Case 2: acc(a) is not accepted, then a → c can be deleted. Our representation of the requires relation is based on the fact that a requires b is modeled by the flattening function with a path from acc(b) to acc(a), i.e. acc(a) is accepted only if acc(b) is accepted. Notice that, given a RQ b, in metaargumentation we condense all the attacks which are both on b and thus on a (both from b and thus from a) using only meta-requirement Z a,b , as we show in Proposition Proposition Given a REAF , if there is an attack such that c → a if a RQ b and c → b, then the extensions do not change, using our meta-argumentation model and one of Dung's semantics.

Fig. 5 .

 5 Fig. 5. Example of equivalence

Fig. 6 .

 6 Fig. 6. Example of goal oriented requirement modeling.

Fig. 8 .

 8 Fig.8. The object level of the example with the goals accepted in the first extension.

Fig. 9 .

 9 Fig.9. The meta-argumentation framework and the extension where goal G11 is accepted.

We do not consider here the third extension ∅ because we want to provide the stakeholders with alternatives where the two conflicting goals are included.

quirements and at providing them a decision support system for inconsistencies resolution.

Related work

Frameworks to reason about goals have already proven to be useful to support goal-based requirements management. In van Lamsweerde et al. [START_REF] Van Lamsweerde | Managing conflicts in goal-driven requirements engineering[END_REF], for instance, goals are specified in a formal way to support reasoning on their content. In Giorgini et al. [START_REF] Giorgini | Goal-oriented requirements analysis and reasoning in the Tropos methodology[END_REF], an approach is proposed to analyze goal hierarchies in order to establish goals satisfiability (full, partial or none). The idea is to show the impact of the adoption of some goals on the other goals of the system. Approaches relaying on argumentation have already been proposed to check the consistency of a requirement set [START_REF] Besnard | Elements of argumentation[END_REF][START_REF] Bagheri | Consolidating multiple requirement specifications through argumentation[END_REF]. Our approach relies on meta-argumentation while the proposal of Bagheri and Ensan [START_REF] Bagheri | Consolidating multiple requirement specifications through argumentation[END_REF] adopts an extension of Dung's framework with preferences over the arguments. Jureta et al. [START_REF] Jureta | Analysis of Multi-Party Agreement in Requirements Validation[END_REF] present a formal model to analyze the discussions between the stakeholders about the validity of the requirements engineering artifacts using argumentation theory. In particular, they introduce the Acceptability Evaluation framework (ACE) which is a propositional reasoning framework. In this framework, an acceptability condition is proposed on an artifact such that if the condition holds then it means that the relative validity for the artifact is verified. They use argumentation theory to model the discussions among stakeholders where inference, attack and preference relationships are used. There are several points which distinguish our approach from the work of Jureta et al. [START_REF] Jureta | Analysis of Multi-Party Agreement in Requirements Validation[END_REF]: first, we rely on abstract argumentation theory