Simon Cruanes

Satisfiability Modulo Bounded Checking

We describe a new approach to find models for a computational higher-order logic with datatypes. The goal is to find counterexamples for conjectures stated in proof assistants. The technique builds on narrowing [14] but relies on a tight integration with a SAT solver to analyze conflicts precisely, eliminate sets of choices that lead to failures, and sometimes prove unsatisfiability. The architecture is reminiscent of that of an SMT solver. We present the rules of the calculus, an implementation, and some promising experimental results.

Introduction

Computational higher-order logics are widely used to reason about purely functional programs and form the basis of proof assistants such as ACL2 [START_REF] Kaufmann | ACL2: An industrial strength version of Nqthm[END_REF], Coq [START_REF]The Coq Proof Assistant[END_REF], and Isabelle [START_REF] Lawrence C Paulson | Isabelle: A generic theorem prover[END_REF]. Searching for models in such logics is useful both for refuting wrong conjectures and for testing -it is often faster and easier to test a property than to prove it. In this work we focus on a logic with algebraic datatypes and terminating recursive functions. Once proven terminating, these functions have a natural interpretation in any model as least fixpoints.

The typical use case is for the users to specify a property they believe to hold for the program they wrote and let a solver search for a (counter-)example until some resource is exhausted -time, patience, etc. Our goal is to build a tool that can be used for finding counter-examples in proof assistants. Figure 1 presents such a problem in TIP syntax [START_REF] Claessen | TIP: Tons of Inductive Problems[END_REF] that defines natural numbers, lists, and operations on lists, where the (unsatisfiable) goal is to find a list of natural numbers that is a palindrome of length 2 with sum 3.

In the functional programming community, tools such as QuickCheck [START_REF] Claessen | QuickCheck: a lightweight tool for random testing of Haskell programs[END_REF] and SmallCheck [START_REF] Runciman | Smallcheck and lazy smallcheck: automatic exhaustive testing for small values[END_REF] have been used to test conjectures against random values or up to a certain depth. Feat [START_REF] Duregård | Feat: Functional Enumeration of Algebraic Types[END_REF] is similar to SmallCheck but enumerates inputs by increasing size, rather than depth. However, QuickCheck is limited when invariants have to be enforced (e.g. red-blackness of trees), forcing users to write custom random generators, and SmallCheck and Feat can get lost quickly in large search spaces. Lazy SmallCheck (LSC) is similar to SmallCheck but relies on the lazy semantics of Haskell to avoid enumerating inputs that are not needed to evaluate the property. LSC is close to narrowing [START_REF] Antoy | A Needed Narrowing Strategy[END_REF][START_REF] Lindblad | Property directed generation of first-order test data[END_REF], a symbolic approach that has ties to functional logic programming [START_REF] Hanus | A unified computation model for functional and logic programming[END_REF] and builds a model incrementally. Nevertheless, LSC and narrowing-based tools explore the space of possible inputs quite naively, making many counter-examples very hard to find. All these approaches lack a way of analyzing why a given search path failed.

(declare-datatypes () ((Nat (Z) (S (prec Nat))))) (declare-datatypes () ((List (Nil) (Cons (hd Nat) (tl List))))) (define-fun-rec plus ((x Nat) (y Nat)) Nat (match x (case Z y) (case (S x2) (S (plus x2 y))))) ; some definitions omitted (define-fun-rec rev ((l List)) List (match l (case Nil Nil) (case (Cons x l2) (append (rev l2) (Cons x Nil))))) (assert-not (forall ((l List))

(not (and (= l (rev l)) (= (length l) (S (S Z))) (= (sum l) (S (S (S Z))))))))

Fig. 1. Looking for impossible palindromes

Modern SMT solvers are often efficient in difficult combinatorial problems. They rely on a SAT solver to analyze conflicts and interleave theory reasoning with propositional choices. However, their focus is first-order classical logic, where symbols are neatly partitioned between theory symbols that have a precise definition and user-provided symbols that are axiomatized. When a user want to introduce their own parameterized operators, they must use quantifiers and full first order logic, where solvers are usually incomplete. Some work has been done on handling datatypes [START_REF] Barrett | An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types[END_REF][START_REF] Reynolds | A decision procedure for (co) datatypes in SMT solvers[END_REF] and recursive functions in SMT solvers such as CVC4 [START_REF] Reynolds | Model Finding for Recursive Functions in SMT[END_REF] or calling an SMT solver repeatedly while expanding function definitions as in Leon [START_REF] Suter | Satisfiability modulo recursive programs[END_REF], but each reduction step (e.g. function call) is very expensive.

Bridging the gap between QuickCheck and SMT solvers is HBMC [START_REF] Claessen | SAT-based Bounded Model Checking for Functional Programs[END_REF] (Haskell Bounded Model Checker -not published yet). HBMC progressively encodes the evaluation graph into propositional constraints (effectively "bit-blasting" recursive functions and datatypes), leveraging the powerful constraint propagations of modern SAT solvers. However, it suffers from the same weakness as SMT-based techniques: every evaluation step has to be encoded, then performed, inside the SAT solver, making computations slow.

We present a new technique, Satisfiability Modulo Bounded Checking (SMBC) that occupies a middle ground between narrowing and HBMC. On the one hand, it can evaluate terms more efficiently than pure bit-blasting although not quite as fast as native code; on the other hand it benefits from propositional conflictdriven clause learning (CDCL) of modern SAT solvers to never make the same bad choice twice. Two main components are involved: (i) a symbolic evaluation engine (Sect. 3), and (ii) a SAT solver with incremental solving under assumptions (Sect. 4). Those two components communicate following lazy SMT techniques [START_REF] Barrett | Splitting on demand in SAT modulo theories[END_REF]. Inputs are lazily and symbolically enumerated using iterative deepening (Sect. 5) to ensure fairness, but we use the ability of the SAT solver to solve under assumptions to avoid the costly re-computations usually associated with that technique. In addition, building on CDCL allows SMBC to sometimes prove the unsatisfiability of the problem, something evaluation-based tools are incapable of.

We can extend SMBC to support uninterpreted types and unspecified functions (Sect. 6). After presenting refinements to the calculus (Sect. 7) and an implementation (Sect. 8), we run some experiments (Sect. 9) to compare SMBC with some of the previously mentioned tools on various families of problems. Detailed proofs and additional content can be found in our report. 1

Logic

We consider a multi-sorted higher-order classical logic, without polymorphism. A finite set of mutually recursive datatypes d 1 , . . . , d k is defined by a system

d i def = c i,1 (α i,1 ) | • • • | c i,ni (α i,ni ) i∈{1,...,k}
where the α i,j are tuples of type arguments. We consider only standard models, in which the domain of a datatype is the set of terms freely generated from its constructors. Similarly, mutually recursive functions f 1 , . . . , f k are defined by a set of equations f 1 (x 1 )

def = t 1 , . . . , f k (x k ) def = t k
that we assume total and terminating. The term language comprises bound variables, datatype constructors, shallow pattern-matching over datatypes, λ-abstractions λx : τ. t, and applications f t 1 . . . t n . Constructors are always fully applied. tσ is the application of a substitution over bound variables σ to t. Bool def = { , ⊥} is a special datatype, paired with tests if a b c that are short for case a of → b | ⊥ → c end. A value is a λ-abstraction or constructor application. The operators ∧ : Bool → Bool → Bool and ¬ : Bool → Bool have the usual logical semantics; evaluation of ∧ is parallel rather than the usual sequential semantics it has in most programming languages: t ∧ ⊥ reduces to ⊥ even if t is not a value. We will speak of parallel conjunction. Other boolean connectives are encoded in terms of ∧ and ¬. We also define an ad hoc polymorphic equality operator = that has the classic structural semantics on datatypes and booleans; comparison of functions is forbidden. An unknown is simply an uninterpreted constant which must be given a value in the model. This logic corresponds to the monomorphic fragment of TIP [START_REF] Claessen | TIP: Tons of Inductive Problems[END_REF] or the extension of SMT-LIB [START_REF] Barrett | The SMT-LIB Standard Version 2.6[END_REF] with recursive functions, with the additional assumption that they always terminate.

A data value is a term built only from constructor applications, bound variables, and λ-abstractions (without defined symbols, matching, or unknowns). The depth of a data value is recursively defined as 1 on constant constructors, 1 + depth(t) for λx. t, and 1 + max i=1...n depth(t i ) on constructor applications c(t 1 , . . . , t n ). 2 A goal set G is a set of boolean terms. A model of G is a mapping from unknowns of G to data values, such that t∈G t evaluates to . The depth of a model is the maximal depth of the data values in it.

In the rest of this paper, t, u will represent terms, k will be unknowns, c, d will be constructors, and e will stand for explanations (conjunctions of literals). We will use an injective mapping to propositional variables denoted • .

Evaluation with Explanations

The semantics of our logic relies on evaluating expressions that contain tests, pattern matching, and (recursive) functions. Because expressions can contain unknowns, their reduction is influenced by assignments to these unknowns. We need an evaluator that keeps track of which choices were used to reduce a term. In this way, when a goal term reduces to ⊥, we know that this combination of choices is wrong.

In Figure 2, we show the evaluation rules for terms, given a substitution ρ on unknowns. The notation t ρ --→ e u means that t reduces to u in one step, with explanations e (a set of boolean literals), under substitution ρ. We denote t ρ --→ * e u for the transitive reflexive closure of the reduction. We write t ↓ ρ (the normal form of t under ρ) for the unique term u such that t ρ --→ * e u and no rule applies to u. In a first approximation, ignoring the explanations, the rules correspond to a normal call-by-need evaluation strategy for the typed λ-calculus. This matches the definition of values given earlier: a value is a weak head normal form. It is possible to use environments instead of substitutions, carrying bindings in every rule, but we chose this presentation for reasons related to hash-consing, as often used in SMT solvers. The choice of call-by-need rather than call-by-value is justified by the maximal amount of laziness it provides in presence of unknowns: instead of waiting for function call arguments, matched terms, or test conditions to be fully evaluated (and therefore, for their unknowns to be fully decided in the partial model), we can proceed with only a weak head normal form.

The rules id and trans specify how explanations are combined in the reflexive transitive closure; The rule case reduces a pattern matching once the matched term is a value (i.e. starts with a constructor, by typing). The rule app allows to reduce the function term in an application (until it becomes a value, that is, a λ-abstraction); rule β is the regular β-reduction; rule def unfolds definitions (in particular, recursive definitions are unfolded on demand). The rule decision replaces an unknown with its value in the current substitution ρ (i.e. the partial model). The other rules define the semantics of boolean operators and equality. We forbid checking equality of functions as is it not computable.

Whether to use small-step or big-step semantics (i.e. reducing a term by one step if a subterm reduces, or waiting for the subterm to become a value) is of little importance for most cases. The only exception is the rules for conjunction, in which big-step semantics is required (i.e. a ∧ b does not always reduce when, e.g., a reduces). To see why, assume small-step semantics and consider a ⊥, e 1 ∪e 3 is sufficient. The resulting explanation is not as general as it could be, and a smaller part of the search space will be pruned as a result.

ρ - -→ * e1 a ρ - -→ * e3 ⊥ and b ρ - -→ * e2 b where a, b : Bool. The following reduction a ∧ b ρ - -→ * e1 a ∧ b ρ - -→ * e1∪e2 a ∧ b ρ - -→ * e1∪e2∪e3 ⊥ ∧ b ρ - -→ * e1∪e2∪e3 ⊥ id a ρ --→ * ∅ a a ρ --→e 1 b b ρ --→ * e 2 c trans a ρ --→ * e 1 ∪e 2 c c is a constructor t ρ --→ * e c(t1, . . . , tn) case case t of c(x1, . . . , xn) → u | • • • end ρ --→e u[t1/x1, . . . , tn/xn] f ρ --→e g app f t ρ --→e g t β (λx. t) u ρ --→ ∅ t[u/x] x def = t def x ρ --→ ∅ t ρ(k) = t decision k ρ --→ { k:=t } t a ρ --→ * e ⊥ and-left a ∧ b ρ --→e ⊥ b ρ --→ * e ⊥ and-right a ∧ b ρ --→e ⊥ a ρ --→ * ea b ρ --→ * e b and-true a ∧ b ρ --→e a ∪e b a ρ --→ * e not-true ¬a ρ --→e ⊥ a ρ --→ * e ⊥ not-false ¬a ρ --→e a ρ --→e a eq-left a = b ρ --→e a = b b ρ --→e b eq-right a = b ρ --→e a = b c, d are constructors c = d eq-conflict c(t) = d(u) ρ --→ ∅ ⊥ c is a constructor eq-sub c(t1, . . . , tn) = c(u1, . . . , un) ρ --→ ∅ n i=1 ti = ui
Evaluation of a normal form t that is not a value in a substitution ρ is blocked by a set of unknowns block ρ (t):

block ρ (λx. t) = ∅ block ρ (c(u 1 , . . . , u n )) = ∅ if c is a constructor block ρ (f t) = block ρ (f ) block ρ (case t of . . . end) = block ρ (t ↓ ρ ) block ρ (k) = {k} if k is an unknown block ρ (a = b) = block ρ (a) ∪ block ρ (b) block ρ (¬a) = block ρ (a ↓ ρ ) block ρ (a ∧ b) = block ρ (a ↓ ρ ) ∪ block ρ (b ↓ ρ )
In some cases, the blocking unknowns are found in the normal form of subterms of t. This corresponds to the evaluation rules that wait for the subterm to become a value before reducing.

Lemma 1 (Uniqueness of values for

ρ - -→ * ). If t ρ - -→ * e1 v 1 and t ρ - -→ * e2 v 2 where v 1 and v 2 are values, then v 1 = v 2 .
Proof. The rules are deterministic, and values are always normal forms since no rule applies to them.

Lemma 2. If t = t ↓ ρ is a normal form, then block ρ (t) = ∅ iff t is a value.
Proof. By induction on the shape of t.

Delegating Choices and Conflict Analysis to SAT

We now have evaluation rules for reducing terms given a substitution on unknowns but have not yet explained how this substitution is built. As in narrowing [START_REF] Antoy | A Needed Narrowing Strategy[END_REF][START_REF] Lindblad | Property directed generation of first-order test data[END_REF], it is constructed by refining unknowns incrementally, choosing their head constructor (or boolean value) and applying it to new unknowns that might need to be refined in turn if they block evaluation. 3 However, in our case, the SAT solver will do the refinement of an unknown k once it has been expanded; the first time k : τ blocks the evaluation of a goal g (i.e., k ∈ block ρ (g)), some clauses are added to the SAT solver, forcing it to satisfy exactly one of the literals

k := c i (k i,1 , . . . , k i,ni )
, where c i is a constructor of τ . Once one of the literals k := t i is true in the SAT solver's partial model -implying that ρ(k) = t i , as we will see next -evaluation of the goal g can resume using rule decision (in Figure 2) and k is no longer blocking.

The state of the SAT solver is represented below as a pair M F where M is the trail (a set of literals not containing both l and ¬l), and F is a set of clauses. The operation subst(M ) extracts a substitution on unknowns from positive literals in the trail:

subst(M )(k) = t if k := t ∈ M
The interactions between the SAT solver and the evaluation engine are bidirectional. When the SAT solver makes some decisions and propagations, yielding the new state M F , the substitution subst(M ) is used to evaluate the goals in G. If all the goals evaluate to , we can report M as a model. Otherwise, if there is a goal t ∈ G such that t subst(M ) ------→ * e ⊥, M must be discarded. This is done by adding to F a conflict clause C def = a∈e ¬a that blocks the set of choices in e. The SAT solver will backjump to explore models not containing e. Backjumping with clause C and state M F returns to a state M F where M is the longest prefix of M in which C is not absurd.

Lemma 3 (Monotonicity of Models).

A model of G, expressed as a trail M ,

satisfies t∈G t subst(M ) ------→ * e .
No subset of M reduces t∈G t to ⊥.

Enumeration of Inputs and Iterative Deepening

We have not specified precisely how to enumerate possible models. This section presents a fair enumeration strategy based on Iterative Deepening [START_REF] Korf | Depth-first iterative-deepening: An optimal admissible tree search[END_REF].

A major issue with a straightforward combination of our evaluation function and SAT solver is that there is a risk of non-termination. Indeed, a wrong branch might never be totally closed. To overcome this issue, we solve a series of problems where the depth of unknowns is limited to increasingly large values, a process inspired from iterative deepening. Because the SAT solver controls the shape of unknowns, we use special boolean literals depth ≤ n to forbid any choice that causes an unknown to be deeper than n; then we solve under assumption depth ≤ n . If a model is found, it is also valid without the assumption and can be returned immediately to the user. Otherwise, we need the SAT solver to be able to provide unsat cores -the subset of its clauses responsible for the problem being unsatisfiableto make the following distinction: if depth ≤ n contributed to the unsat core, it means that there is no solution within the depth limit, and we start again with depth ≤ n + Step (where Step ≥ 1). The last case occurs when the conflict does not involve the assumption depth ≤ n : then the problem is truly unsatisfiable (e.g., in Figure 1).

The iterative deepening algorithm is detailed below, in three parts: (i) the main loop, in Algorithm 1; (ii) solving within a depth limit, in Algorithm 2;

(iii) expanding unknowns, in Algorithm 3. These functions assume that the SAT solver provides functions for adding clauses dynamically (AddSatClause), adding a conflict clause (Conflict), performing one round of decision then boolean propagation (MakeSatDecision and BoolPropagate), and extracting unsat cores (UnsatCore). These functions modify the SAT solver state M F . In practice, it is also possible to avoid computing unsat cores at line 7 in Algorithm 1, by checking for pure boolean satisfiability again, but without the depth-limit assumption. Most computations (including the current normal form of t∈G t) can be done incrementally and are backtracked in case of conflict.

Application to the Introductory Example

We illustrate our technique on an example. 4 Pick the same definitions as in Figure 1, but with the goal set G def = {rev(l) = l, length(l) = 2, sum(l) = 2} where the unknown is a list l. Unlike in Figure 1, this problem is satisfiable. Assuming

Step = 1, we start solving under constraint depth ≤ 1 . Under the empty substitution, G reduces to a set of terms all blocked by a pattern matching on l; expansion of l into {Nil, Cons(x 1 , l 1 )} follows, where x 1 : Nat and l 1 : List are fresh unknowns. Suppose the SAT solver picks l := Nil . G reduces to { , ⊥, ⊥} with explanations { l := Nil }, so the conflict clause ¬ l := Nil is asserted, added to the partial model with no effect, and the solver backtracks.

The next boolean decision must be l := Cons(x 1 , l 1 ) . Subsequently, G reduces to {append(rev(l 1 ), Cons(x 1 , Nil)) = Cons(x 1 , l 1 ), length(l 1 ) = 1, x 1 + sum(l 1 ) = 2} (more precisely, to a less readable version of these terms where function definitions are unfolded into some pattern matching). The resulting set is blocked both by l 1 (in the first two terms) and x 1 (in x 1 + sum(l 1 )). Expansion of these terms yields {Nil, Cons(x 2 , l 2 )} and {Z, S(y 1 )}, but the choice Cons(x 2 , l 2 ) is blocked by depth ≤ 1 . The solver must choose l 1 := Nil , which entails

length(l) = 2 ρ - -→ * { l:=Cons(x1,l1) } length(l 1 ) = 1 ρ - -→ * { l1:=Nil } 0 = 1 ρ - -→ * ∅ ⊥
The conflict clause ¬ l := Cons(x 1 , l 1 ) ∨ ¬ l 1 := Nil triggers an Unsat result, but only because of the assumption depth ≤ 1 .

The main loop (Algorithm 1) then proceeds to depth 2, and tries to solve the problem again under the assumption depth ≤ 2 . The SAT solver can now pick l 1 := Cons(x 2 , l 2 ) . At some point, it will pick l 2 := Nil (the other choice is too deep), x 1 := S(y 1 ) , y 1 := Z , x 2 := S(y 2 ) , and y 2 := Z . Other choices would reduce one of the goals to ⊥: once the shape of l 1 is fixed by the length constraint, rev(l) = l reduces to x 1 = x 2 and sum(l) = 2 becomes

x 1 + x 2 = 2,
empty(τ [n-1...] ) ⇒ empty(τ [n...] ) depth ≤ n ⇒ empty(τ [n...] ) k = elt n (τ ) ∨ ¬ empty(τ [n+1...] ) ∧ k := k
where k : τ [n+1...] is a fresh unknown belonging in the next slice of τ . To express constraints on τ , the input language provides finite quantifiers ∀x : τ. F and ∃x : τ. F (which abbreviates ¬(∀x : τ. ¬F )). The quantifier is interpreted with the following rules:

ρ( empty(τ [n...] ) ) = forall-empty ∀x : τ [n...] . F ρ - -→ { empty(τ [n...] ) } ρ( empty(τ [n...] ) ) = ⊥ forall-pair ∀x : τ [n...] . F ρ - -→ {¬ empty(τ [n...] ) } F [elt n (τ )/x] ∧ ∀x : τ [n+1...] . F

Functional Unknowns

With uninterpreted types often come functions taking arguments of uninterpreted types. We can also wish to synthesize (simple) functions taking booleans or datatypes as parameters. It is possible to build functions by refinement, using currying (considering only one argument at a time) depending on its argument's type. Expansion of a functional unknown f : a → b depends on a:

-If a = Bool, f ∈ {λx. if x t 1 t 2 } where t 1 , t 2 : b are fresh unknowns of type b that are deeper than f . -If a is uninterpreted, f is λx. switch(x, m)
where m is a table mapping (elt i (a)) i=0... to fresh unknowns of type b (built lazily, in practice) and switch is otherwise similar to case.

-If a is a datatype, f is either a constant function λx. k f where k f is an un- known of type b or λx. case x of c i (y) → k i y | • • • end
where each k i is a fresh unknown taking the corresponding constructor's arguments as parameters.

The constant case is used to be able to build functions that only peek superficially at inputs -otherwise, all function descriptions would be infinite in the model. The choice between the two forms for f is performed by the SAT solver; the non-constant case might be blocked by depth constraints. If a is infinite, bounded completeness is lost immediately, as we cannot generate all functions a → b. -Otherwise, a is a function type and we should reject the initial problem.

7 Refinements to the Calculus

Multiple Conflict Clauses

Sometimes, a partial model causes a failure for several reasons: in the presence of parallel conjunction, both formulas can reduce to ⊥. It would be wasteful to keep only one reason, because all of them might be useful to prune other branches. In this case, instead of just picking one explanation and discard the others, as suggested in Figure 2, we add a new explanation constructor, e 1 ⊕ e 2 , that combines two unrelated explanations, such that ⊕ is associative and commutative and (e 1 ⊕ e 2 ) ∪ e 3 ≡ (e 1 ∪ e 3 ) ⊕ (e 2 ∪ e 3 ). Intuitively, a ρ --→ e1⊕e2 b means that a evaluates to b under substitution ρ assuming the choices in e 1 or in e 2 are made -those choices are never incompatible, but they might not be the same subset of subst(M ). We add a new rule for ∧:

a ρ - -→ * ea ⊥ b ρ - -→ * e b ⊥ and-left-right a ∧ b ρ - -→ ea⊕e b ⊥ In case of conflict t∈G ρ - -→ * i∈I ei ⊥ ,
we obtain a set of conflict clauses a∈ei ¬a | i ∈ I that will prune distinct parts of the partial model.

Unification Rules

Equality already has many rules, but we can optimize it further. In our implementation, relying on hash-consing, we simplify t = t into in constant time, even when t contains unassigned unknowns. We can optimize equality further in the special case where reduction leads to a term c(t 1 , . . . , t n ) = k or k = c(t 1 , . . . , t n ) where k is an unknown and c a constructor or domain element. This term reduces with no explanation to if check k :=c(u1,...,un) (

n i=1 t i = u i ) ⊥,
where check k :=c(u1,...,un) : Bool is a new term construct that requires c(u 1 , . . . , u n ) to be one of the cases resulting from the expansion of k. In the ⊥ case, the explanation forces the SAT solver to pick c(u 1 , . . . , u n ) instead of ruling out the wrong choice d(u 1 , . . . , u m ); if there are more than two constructors, this forces directly the right choice instead of trying every wrong choice.

c(u 1 , . . . , u n ) is a case of k unify k = c(t 1 , . . . , t n ) ρ - -→ ∅ if check k :=c(u1,...,un) ( n i=1 t i = u i ) ⊥ ρ(k) = c(u 1 , . . . , u n ) check-true check k :=c(u1,...,un) ρ - -→ {k:=c(u1,...,un)} ρ(k) = d(u 1 , . . . , u m ) d = c check-false check k :=c(u1,...,un) ρ - -→ {¬(k:=c(u1,...,un))} ⊥

Implementation

We implemented SMBC in OCaml5 using a modular SAT solver 6 that is flexible enough that we can add clauses dynamically and parameterize it with a theory solver. It also supports incremental solving under assumptions, which is necessary for the efficiency of the iterative deepening exploration. The core solver is around 3,200 lines long, including the term data structures, the symbolic evaluation and the main loop. This implementation is a prototype that can be used, but we believe it could be made much faster with more work and perhaps by using a lower-level language. The code is free software, under a permissive license.

Our description of evaluation rules in Figure 2 is quite high-level and can be implemented in various ways. 7 We chose to represent terms as perfectly shared directed acyclic graphs in which binders and bound variables rely on De Bruijn indices. The perfect sharing diminishes memory usage and makes let statements superfluous. We store in every term a pointer to a pair (explanation, term) that stores the current normal form of this term, effectively implementing a crude form of memoization. Any assignment of this pair must be undone upon backtracking -in a similar way as in congruence closure algorithms [START_REF] Barrett | Splitting on demand in SAT modulo theories[END_REF]. Similarly, unknowns are records with mutable pointers to a list of possible cases (once they have been expanded) and to their current assignment, which is reverted during backjumping thanks to a central backtracking stack that is controlled by the SAT solver. A good representation of explanations is required for efficiency, because union will be performed very often during the evaluation of terms and should be as fast as possible.

In addition, the evaluation function performs acyclicity checks to prune impossible branches early, and aggressively caches the normal forms of terms, stashing their old value on the central backtracking stack. Since we follow the architecture proposed by Barrett et al. [START_REF] Barrett | Splitting on demand in SAT modulo theories[END_REF], SMBC can delegate all branching to the SAT solver. Every time a boolean decision is made by the SAT solver (followed by propagation), the evaluation engine is called so as to prune bad models early. It does so by re-evaluating the set of goals G, which must contain at least one term not reduced yet, and cannot contain ⊥ (see Algorithm 2). This re-evaluation is made faster by starting from the cached normal forms instead of the original goals. If all goals in G reduce to , the model is valid; if one of them reduces to ⊥, the SAT solver immediately receives a conflict clause that will make it backtrack.

Experiments

We ran a few experiments to compare SMBC with other approaches, namely LSC, HBMC, CVC4 [START_REF] Reynolds | Model Finding for Recursive Functions in SMT[END_REF], and Inox, a standalone version of Leon [START_REF] Suter | Satisfiability modulo recursive programs[END_REF]. We do not compare against QuickCheck, SmallCheck, or Feat, because they are not designed to solve such tightly constrained problems. All the data and the code of SMBC can be found at https://cedeela.fr/ ~simon/files/cade_17.tar.gz. For this experiment, we wrote some problems and borrowed some others from HBMC's test suite. We tried to pick diversified benchmarks so as to expose the strengths and weaknesses of each tool. TIP does not come yet with an exhaustive set of satisfiable benchmarks that would rely primarily on recursive functions. Benchmarks from our previous work on CVC4 [START_REF] Reynolds | Model Finding for Recursive Functions in SMT[END_REF] are expressed in SMT-LIB rather than TIP and use quantified axioms instead of recursive definitions, which makes them hard to use in our purely computational setting. The same holds of SMT-LIB and TPTP in general.

The solvers were run on a 4-cores Intel i5 CPU with 60 seconds timeout and a limit of 8 GB of RAM. Below, we give some numbers in Table 1 and then analyse the results on some categories of problems. The second column of the table is the number of satisfiable and unsatisfiable problems. Categories out of scope are marked with "-".

Expr Given arithmetic expressions, an evaluation function and several flawed simplifications, the goal is to find an expression such that its simplification does not evaluate to the same term. Here HBMC and Inox shine, but SMBC In other words, we fold a function f on all elements, and the goal is to pick f such that it can distinguish between close, but distinct, lists. This problem is outside the scope of all the tools the author knows about, simply because it combines an uninterpreted type with an unknown of function type, but SMBC has no problem synthesizing what is in essence a state machine transition function. Palindromes After defining unary natural numbers and lists, we look for lists that are palindromes (i.e., rev(l) = l) that have some additional constraint on their sum or length. Some of those problems are more difficult variations of the problem from Section 5.1. Some of the problems are satisfiable and some are unsatisfiable. For example, the goal in long rev sum2.smt2 is to disprove the existence of a palindrome of length 200 with sum 1; HBMC times out because there are too many computations, and LSC cannot detect unsatisfiability. Those problems are easy but the toplevel goal is a parallel conjunction that needs to be treated properly, which is why LSC fails to solve even the satisfiable instances. Pigeon A computational version of the classical pigeon hole problem, here with 4 holes for 5 pigeons. This requires handling uninterpreted types and unsatisfiable problems. Regex Basic regular expressions are represented by a datatype featuring constants, star, and disjunction. The goal is generally to find a regular expression that matches a given string. Here, LSC shines and HBMC is in trouble, because (comparatively) many computations are required to check each input. SMBC has a good success rate here, even though its relatively naive interpreter is much slower than LSC's native compiled code. Sorted Some problems about finding sorted lists of natural numbers that have additional properties (on their length, reverse, sum, etc.). The problems are fairly easy, but some of them are unsatisfiable.

Problems (SAT-UNSAT) SMBC HBMC LSC CVC4 Inox Expr (3-1) 2-0 3-0 2-0 0-0 3-0 Fold (2-0) 2-0 - - - - Palindromes (1-2) 1-2 1-1 0-0 0-0 0-1 Pigeon (0-1) 0-1 - - 0-1 0-0 Regex (12-0) 7-0 2-0 11-0 - 0-0 Sorted (2-2) 2-2 2-2 2-0 0-1 2-1 Sudoku (1-0) 1-0 1-0 0-0 0-0 0-0 Type Checking (2-0) 2-0 2-0 0-0 0-0 0-0
Sudoku A sudoku is represented as a list of lists of a datatype with 9 constructors. Some functions to check whether the sudoku is valid (no duplicate in any line, column or block) are defined, an initial state is given, and the goal is simply to solve the sudoku. This is also a combinatorial problem on which HBMC takes only 2 s, SMBC takes 12 s, and LSC times out. Here, it pays to bit-blast because the SAT solver can propagate constraints among the sudoku cells. Type Checking This example comes from the HBMC draft report [START_REF] Claessen | SAT-based Bounded Model Checking for Functional Programs[END_REF]. Terms of the simply typed λ-calculus are defined by a datatype (variables being mapped to De Bruijn indices), along with a type-checking function that takes a term t, a type τ and an environment Γ (i.e. a list of types), and returns iff Γ t : τ holds. The goal is to find a term that has type (a → b) → (b → c) → (a → c) in the empty environment: in other words, to synthesize the composition operator from its type. The task is difficult because of the fast growth of the search space, in which LSC drowns, but SMBC manages well.

Overall, SMBC appears to be well balanced and to have good results both on problems that require computations and on problems where pruning of impossible cases is critical. Given the simplicity of our implementation, we believe these results are promising, and that SMBC occupies a sweet spot between handling computations well and traversing the search space in a smart way.

Conclusion

After describing a new technique for finding models in a logic of computable functions and datatypes, we presented ways of extending the language and described a working implementation. By combining symbolic evaluation with SAT-based conflict analysis, the approach is aimed at difficult problems where the search space is large (e.g., because of parallel disjunction and independent sub-problems) and large amounts of computations must be performed before discovering failure. It can be described as a spiritual heir to evaluation-driven narrowing [START_REF] Lindblad | Property directed generation of first-order test data[END_REF] that replaces traditional exploration of the space of possible inputs by conflict driven clause learning. We hope that this work will benefit model finders in proof assistants, in particular Nunchaku [START_REF] Cruanes | Extending Nunchaku to Dependent Type Theory[END_REF][START_REF] Reynolds | Model Finding for Recursive Functions in SMT[END_REF].

Fig. 2 .

 2 Fig. 2. Evaluation rules under substitution ρ

  Consider the goal p(b) ∧ a + b = Z with unknowns {a, b}, where p(x) def = case x of Z → | S( ) → end is trivial, and + is defined on Peano numbers by recursion on its left argument. Then making the initial choice b = S(b 2 ) (to unblock p(b)) and proceeding to refine a in order to unblock a + b = Z will lead to an infinite number of failures related to a, none of which will backjump past b = S(b 2 ).

  and wrong choices quickly reduce those to ⊥. At this point, and we obtain the model l = Cons(1, Cons(1, Nil)).6 Extensions of the Language6.1 Uninterpreted TypesFinding counter-example for programs and formalizations that use only recursive function definitions might still involve uninterpreted types arising from type Skolemization or abstract types. To handle those in SMBC, e.g. for a type τ , which corresponds to a finite set of domain elements denoted elt 0 (τ ), elt 1 (τ ), . . . (domain elements behave like constructors for evaluation). We also introduce type slices τ [0...] , τ [1...] , . . . where τ def = τ [0...] . Conceptually, a type slice τ [n...] corresponds to the subtype of τ that excludes its n first elements: τ [n...] def = {elt n (τ ), . . . , elt card(τ )-1 (τ )}. Then, we introduce propositional literals empty(•) that will be given a truth value by the SAT solver; if empty(τ [n...] ) is true, it means τ [n...] ≡ ∅; otherwise, it means τ [n...] ≡ {elt n (τ )} ∪ τ [n+1...] . We assume ¬ empty(τ [0...] ) . Expansion of some unknown k : τ [n...] yields the following boolean constraints:

  Algorithm 1 Main Loop Using Iterative Deepening The function SolveUpTo in Algorithm 2 returns either Sat or Unsat. If it returns Sat, then the substitution subst(M ) from

	Require: Step ≥ 1: depth increment, G: set of goals 1: function MainLoop(G) 2: d ← Step 3: while d ≤ MaxDepth do 4: res ← SolveUpTo(G, d) 5: if res = Sat then return Sat 6: else if depth ≤ d ∈ UnsatCore(res) then return Unsat 7: else d ← d + Step 8: return Unknown Algorithm 2 Solving Within a Depth Limit 2: AddAssumption( depth ≤ d ) local assumption initial depth 3: M F ← ∅ G initial model and clauses 4: while true do 5: M F ← MakeSatDecision(M F ) model still partial 6: M F ← BoolPropagate(M F ) 7: G ← {(u, e) | t ∈ G, t subst(M ) -----→ * e u} current normal form of G 8: if (⊥, e) ∈ G then 9: M F ← Conflict(M F ∪ { a∈e ¬a}) backjump or Unsat 10: else if all terms in G are then return Sat 11: else 12: B ← (t,e)∈G block subst(M ) (t) blocking unknowns 13: for k ∈ B, k not expanded do 14: F ← F ∪ Expand(k, d) will add new literals and clauses Theorem 1 (Termination). The function SolveUpTo in Algorithm 2 ter-minates. Require: k: unknown of type τ , d: depth limit 1: function Expand(k, d) 2: let τ = c1(τ1,1, . . . , τ1,n 1 ) | . . . | c k (τ k,1 , . . . , τ k,n k ) 3: l ← {ci(ki,1, . . . , ki,n i ) | i ∈ 1, . . . , k} each ki,j:τ i,j is a fresh unknown 4: AddSatClause( t∈l k := t ) 5: AddSatClauses({¬ k := t1 ∨ ¬ k := t2 | (t1, t2) ∈ l, t1 = t2}) 6: for t ∈ l where depth(t) > d do 7: AddSatClause(¬ depth ≤ d ∨ ¬ k := t ) block this choice at depth d the boolean trail is a model. If it returns Unsat, then there are no solutions of Theorem 2 (Soundness). Algorithm 3 Expansion of Unknowns depth smaller than d.

Require: G: set of goal terms, d: depth limit 1: function SolveUpTo(G, d) Theorem 3 (Bounded Completeness). If there exists a model of depth smaller at most Step MaxDepth/Step , then Algorithm 1 will return Sat. Proof. The depth d is always a multiple of Step. Let d min ≤ MaxDepth be the smallest multiple of Step such that there is a model of depth ≤ d min . Iterations of the loop with d < d min return Unsat by soundness of SolveUpTo (Theorem 2); the iteration at depth d min returns Sat.

Table 1 .

 1 Results of the Experimentsand LSC have more trouble due to the large branching factor of the search tree.Fold Those examples are about synthesizing a function that distinguishes between lists by only looking at one element at a time (plus an accumulator).

https://cedeela.fr/ ~simon/files/cade_17_report.pdf

A more flexible definition depth(c(t1, . . . , tn)) = cost(c) + maxi=1...n depth(ti) can also be used to skew the search towards some constructors, as long as cost(c) > 0 holds for all c.

Our framework corresponds to the special case of needed narrowing when the only rewrite rules are those defining pattern matching.

The example is provided at https://cedeela.fr/ ~simon/files/cade_17.tar.gz along with other benchmarks.

https://github.com/c-cube/smbc/

https://github.com/Gbury/mSAT

For example, it might be possible to write an efficient interpreter or compiler for use-cases where evaluation is the bottleneck, as long as explanations are tracked accurately and parallel conjunction is accounted for.

Acknowledgments The author would like to thank Jasmin Blanchette, Martin Brain, Raphaël Cauderlier, Koen Claessen, Pascal Fontaine, Andrew Reynolds, and Martin Riener, and the anonymous reviewers, for discussing details of this work and suggesting textual improvements.


Bartosz Alchimowicz
email: bartosz.alchimowicz@cs.put.poznan.pl

Jakub Jurkiewicz
email: jakub.jurkiewicz@cs.put.poznan.pl

Jerzy Nawrocki
email: jerzy.nawrocki@cs.put.poznan.pl

Miroslaw Ochodek
email: miroslaw.ochodek@cs.put.poznan.pl

Mirosław Ochodek

Towards Use-Cases Benchmark

Keywords: Use cases, Requirements engineering, Metrics, Benchmark

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Functional requirements are very important in software development. They impact not only the product but also test cases, cost estimates, delivery date, and user manual. One of the forms of functional requirements are use cases introduced by Ivar Jacobson about 20 years ago. They are getting more and more popular in software industry and they are also a subject of intensive research (see e.g. [START_REF] Anda | Towards an inspection technique for use case models[END_REF][START_REF] Bernardez | Empirical Evaluation and Review of a Metrics-Based Approach for Use Case Verification[END_REF][START_REF] Denger | Achieving high quality of use-case-based requirements[END_REF][START_REF] Diev | Use cases modeling and software estimation: applying use case points[END_REF][START_REF] Somé | Supporting use case based requirements engineering[END_REF]). Ideas presented by researches must be empirically verified (in best case, using industrial data) and it should be possible to replicate a given experiment by any other researcher [START_REF] Shull | The role of replications in empirical software engineering[END_REF]. In case of use cases research it means that one should be able to publish not only his/her results but also the functional requirements (use cases) that has been used during the experiment. Unfortunately, that is very seldom done because it is very difficult. If a given requirements specification has a real commercial value, it will be hard to convince its owner (company) to publish it. Thus, to make experiments concerning use cases replicable, one needs a benchmark that would represent use cases used in real software projects.

In the paper an approach to construct use-cases benchmark is presented. The benchmark itself is the use-cases-based requirements specification, which has a typical profile observed in requirements coming from the real projects. To derive such a profile an extensive analysis of 432 use cases was performed.

The paper is organised as follows. In Section 2 a model of use-cases-based requirements specification is presented. This model is further used in Section 3, which presents an analysis of the use-cases, coming from eleven projects. Based on the analysis a profile of the typical use-case-based specification is derived, which is used to create a benchmark specification in Section 4. Finally, a case study is described in Section 5, which presents a typical usage of the benchmark specification in order to compare tools for use-case analysis.

2 Benchmark-oriented model of use-case-based specification

Although use cases have been successfully used in many industrial projects (Neil et al. [START_REF] Neill | Requirements Engineering: The State of the Practice[END_REF] reported that 50% of projects have their functional requirements presented in that form), they have never been a subject of any recognisable standardisation. Moreover, since their introduction by Ivar Jacobson [START_REF] Jacobson | Object-oriented software engineering: A use case driven approach[END_REF] many approaches for their development were proposed. Russell R. Hurlbut [START_REF] Hurlbut | A Survey of Approaches for Describing and Formalizing Use Cases[END_REF], gathered fifty-seven contributions concerning use cases modeling. Although, all approaches share the same idea of presenting actor's interaction with the system in order to obtain his goal, they vary in a level of formalism and presentation form. Thus it is very important to state what is understood by the term use-cases-based requirements specification.

To mitigate this problem a semi-formal model of use-cases-based requirements specification has been proposed (see figure 1). It incorporates most of the best-practices presented in [START_REF] Adolph | Patterns for Effective Use Cases[END_REF][START_REF] Cockburn | Writing effective use cases[END_REF].

It still allows to create specification that contains only scenario (or nonstructured story) and actors, which is enough to compose small but valuable use-case, as well as extend it with other elements, for example extensions (using steps or stories), pre-and post-conditions, notes or triggers.

Unfortunately, understanding the structure of specification is still not enough in order to construct a typical use-cases-based specification. What is missing, is the quantifiable data concerning the number of model-elements and proportions between them1 . In other words, one meta-question has to be asked for each element of the model -"how many?".

Analysis of use-cases-based specifications structure

In order to discover the profile of typical-specification, data from various projects was collected and analysed. As a result a database called UCDB (Use Cases Database) [START_REF]Use Case Database[END_REF] has been created. At this stage it stores data from 11 projects with the total number of 432 use cases (basic characteristics of requirements specifications as well as projects descriptions are grouped in table 1). All of the specifications have been analysed in order to populate the model with the information concerning average number of its elements occurrence and some additional quantifiable data.

One of the interesting findings is that 79.9% of the main-scenarios in the use cases consist of 3-9 steps, which means that they fulfil the guidelines proposed by Cockburn [START_REF] Cockburn | Writing effective use cases[END_REF]. What is more 72.9% of the analysed use cases are augmented with the alternative scenarios (extensions). There are projects which contains extensions for all steps in main scenario, however on the average use case contains 1.5 extension. Detailed information regarding number and distributions of steps in both -main scenario and extensions, is presented in figure 2.

Another interesting observation, concerning the structure of use cases, is that the sequences of steps performed by the same actor, frequently contains more than one step. What is even more interesting this tendency is more visible in case of main actor's steps (37.3% of main actor's steps sequences are longer than one step, and only 19.4% in case of secondary actor -in most cases system being built). This is probably because actions performed by main actor are more important, from the business point of view. This is contradict to the concept of transactions in use cases presented by Ivar Jacobson [START_REF] Jacobson | Object-oriented development in an industrial environment[END_REF]. Jacobson enumerated four types of actions which may form together use-case transaction. Only one

Project D Polish Industry

Web-based e-government Content Management System (CMS)

Project E Polish

Web-based Document Management System (DMS)

Project F Polish Industry

Web-based invoices repository for remote accounting

Project G English External

Protein Information Management System (PIMS)

Project H Polish Industry

Integration of two sub-system s in ERP scale system

Project I Polish Industry

Banking system

Project J Polish Industry

Single functional module for the webbased e-commerce solution

Project K Polish Industry

Web-based workflow system with Content Management System (CMS)

of them belongs to a main actor (user request action). The rest of them are system actions: validation, internal state change, and response. It might look that those actions should frequently form together longer sequences. However, 80.6% of steps sequences performed by system consisted of single step only. The distributions and number of steps in main actor's sequences are presented in figure 3.

If we look deeper into the textual representation of the use cases, some interesting observation concerning their semantic might be made. One of them regards the way use-cases authors describe validations actions. Two different approaches are observed. The most common is to use extensions to represent alternative system behaviour in case of verification-process failure (46.6% of extensions have this kind of nature). Second one, and less frequent, is to incorporate validation actions into steps (e.g. System verifies data). This kind of actions are observed only in 3.0% of steps. There is also yet another interesting semantic structure

Number of steps in main scenario

A B C D F G H I J K 2 4 6 8

Project

Number of steps in extension

d)
Fig. 2. Scenarios lengths in analysed use cases a) histogram presents the number of steps in main scenario (data aggregated from all of the projects), b) box plot presents the number of steps in main scenario (in each project), c) histogram presents the number of steps in extension (data aggregated from all of the projects), d) box plot presents the number of steps in extension (in each project, note that project E was excluded because it has all alternative scenarios written as stories) used to represent alternative execution paths -conditional clauses (which in fact, are rather deprecated). Fortunately this kind of statements are observed only in 3.2% of steps (and they occur intensively only in 2 projects).

Analysed properties can be classified into two separate classes. The first one contains properties which are observed in nearly all of the projects, with comparable intensity. Those kind of properties are seem to be independent from the specification they belong to (from its author's writing style). The second class is an opposite one, and includes properties wich are either characteristic only for a certain set of use cases or their occurrence in different specifications are in between of two extremes -full presence or marginal/none. Such proper-

Building referential specification

Combining use-cases model and average values coming from the analysis, a profile of the typical use-cases-based requirements specification can be derived. In such specification all properties would appear with the typical intensity. In other words, analysis performed on such document could be perceived as an every-day task for use-cases analysis tools.

There might be at least two approaches to acquire instance of such specification. The first one would be to search for the industrial set of use cases, which would fulfil given criteria. Unfortunately, most of industrial documents are confidential, therefore they could not be used at large scale. The second, obvious approach would be to develop such specification from scratch. If it is built according to the obtained typical-specification profile, it might be used instead of industrial specification. Since it would describe some abstract system it can be freely distributed and used by anyone.

Therefore, we would like to propose approach to develop an instance of the referential specification for the benchmarking purpose. The document is available at the web site [START_REF]Use Case Database[END_REF] and might be freely used for further research.

Specification domain and structure

It seems that large number of tools for the use-cases analysis have their roots in the research community. Therefore the domain of the developed specification should be easy to understand especially for the academia staff. One of the wellrecognised processes at universities is a students admission process. Although developed specification will describe hypothetical process and tools, it should be easy to understand for anyone who have ever participated in a similar process. Another important decision concerns the structure of the specification (number of actors, use cases and business objects). Unfortunately the decision is rather arbitral, because number of use cases, actors and business objects may depend on the size of the system and level of details incorporated into its description. In this case a median number of use cases and actors from the UCDB set has been used as a number of use cases and actors in the constructed specification. The final specification consist of 7 actors (Administrator, Candidate, Bank, Selection committee, Students Management System, System, User), 37 use cases (3 business, 33 user, and 1 sub-function level), and 10 business objects.

Use cases structure

A breadth-first rule has been followed in order to construct referential specification. Firstly, all use cases were titled and augmented with descriptions. Secondly, all of them were filled with main scenarios and corresponding extensions. During that process all changes made in specification were recorded in order to check conformance with the typical profile. This iterative approach was used until the final version of the specification has been constructed. Its profile is presented in table 3, in comparison to the corresponding average values from the UCDB projects analysis (main actor's step sequences lengths for referential specification, are additionally presented in figure 4). The most important properties are those which are observed in all of the specifications (specification independent). In case of those metrics most values in the referential document are very close to those derived from the analysis. This situation differs in case of properties which were characteristic only for certain projects (or variability between projects were very high). If the constructed specification is suppose to be a typical one, it should not be biased by features observed only in some of the industrial specifications. Therefore dependent properties were also incorporated into the referential use cases, however they were not a subject of the tunning process.

Benchmarking use cases -case study

Having the example of the typical requirements specification, one can wonder how it could be used. Firstly, researchers who construct methods and tools in order to analyse use cases often face the problem of evaluating their ideas. Using some specification coming from the industrial project is a typical approach, however, this cannot lead to the conclusion that the given solution would give the same results for other specifications. The situation looks different when the typical specification is considered, then researchers can assume that their tool would work for most of the industrial specifications. Secondly, analysts who want to use some tools to analyse their requirements can have a problem to choose the best tool that would meet their needs. With the typical specification in mind it can be easier to evaluate the available solutions and choose the most suitable one. To conclude the example of the typical requirements specification can be used:

to compare two specifications and asses how the given specification is similar to the typical one to asses the time required for a tool to analyse requirement specification to asses the quality of a tool/method to compare tools and choose the best one In order to demonstrate the usage of the constructed specification we have conducted a case study. As a tool for managing requirements in form of use cases we chose the UC Workbench tool [START_REF] Nawrocki | Uc workbench -a tool for writing use cases[END_REF], which has been developed at Poznan University of Technology since the year 2005. Additionally we used the set of tools for defects detection [START_REF] Ciemniewska | Supporting use-case reviews[END_REF] to analyse the requirements. The aim of the mentioned tools is to find potential defects and present them to analyst during the development of the requirements specification. The tools are based on the Natural Language Processing (NLP) methods and use Standford parser [START_REF] De Marneffe | Generating typed dependency parses from phrase structure parses[END_REF] and/or OpenNLP [START_REF]OpenNLP[END_REF] tools to perform the NLP analysis of the requirements.

Quality analysis

In order to evaluate the quality of the used tools, a confusion matrix will be used [START_REF] Fawcett | Roc graphs: Notes and practical considerations for data mining researchers[END_REF] (see table 4).

Table 4. Confusion matrix

No

TP FP

No FN TN

Expert answer

System answer

Yes

Yes

The symbols used in table 4 are described below:

-T (true) -tool answer that is consistent with the expert decision -F (false) -tool answer that is inconsistent with the expert decision -P (positive) -system positive answer (defect occurs) -N (negative) -system negative answer (defect does not occur)

On the basis of the confusion matrix, following metrics [START_REF] Krawiec | Uczenie maszynowe i sieci neuronowe[END_REF] can be calculated:

-Accuracy (AC) -proportion of the total number of predictions that were correct. It is determined using the equation 1.

AC = T P + T N T P + F N + F P + T N (1)
-True positive rate (TP rate) -proportion of positive cases that were correctly identified, as calculated using the equation 2.

T P rate = T P T P + F N

-True negative rate (TN rate) is defined as the proportion of negatives cases that were classified correctly, as calculated using the equation: 3.

T N rate = T N T N + F P (3)
-Precision (PR) -proportion of the predicted positive cases that were correct, as calculated using the equation 4.

P R = T P T P + F P

The referential use-case specification was analysed by the mentioned tools (to perform the NLP processing Stanford library was used) in order to find 10 types of defects described in [START_REF] Ciemniewska | Supporting use-case reviews[END_REF]. Aggregated values of the above accuracy-metrics are as follows:

-AC = 0.99 -TP rate = 0.96 -TN rate = 0.99 -PR = 0.82 This shows that the developed tools for defects detection are rather good, however, the precision could be better and the researchers could conclude that more investigation is needed in this area.

If the researchers worked on their tool using only defect-prone or defect-free specifications the results could be distorted and could lead to some misleading conclusions (e.g. that the tool is significantly better or that it gives very poor outcome). Having access to the typical specification allows the researchers to explore main difficulties the tool can encounter during working with the industrial specifications.

Time analysis

One of the main characteristics of a tool being developed is its efficiency. Not only developers are interested in this metric, but also for the users -e.g. when analysts have to choose between two tools which give the same results, they would choose the one which is more efficient. However, it can be hard to asses the efficiency just by running the tool with any data, as this may result with distorted outcome. Use-cases benchmark gives the opportunity to measure the time, required by a tool to complete its computations, in an objective way. It can be also valuable for researchers constructing tools to consider using different third-party components in their applications.

For instance, in case of the mentioned defect-detection tool there is a possibility of using one of the available English grammar parsers. In this case study two of them will be considered -Standford parser and OpenNLP. If one exchanges those components the tool will still be able to detect defects, but its efficiency and accuracy may change. Therefore, the time analysis was performed to asses how using those libraries influence the efficiency of the tool. The overall time required to analyse the typical specification2 for the tool using Stanford parser was 54.37 seconds and for the one with OpenNLP it was 31.21 seconds. Although the first time value seems to be large, the examined tool needed on average 290 ms to analyse a single use-case step, so it should not be a problem to use it in the industrial environment. Of course, when comparing efficiency, one have to remember that other factors (like the quality of the results, memory requirements or the time needed for the initialization of the tools) should be taken into account, as they can also have significant impact on the tool itself. Therefore, time, memory usage and quality analysis is presented in table 5. This summarised statistics allow researchers to choose the best approach for their work.

Although this specification describes some abstract system, it shows the typical phenomenon of the industrial requirements specifications. The conducted case study shows that the developed referential use-case specification can be used in different ways by both researchers and analysts.

Conclusions

In the paper an approach to create a referential use-cases-based requirements specification was presented.

In order to derive such a specification 432 use cases were analysed. It has proved that some of the use-case properties are project-independent (are observed in most of the projects). They have been used for creating the referential specification. On the other hand, there is also a number of properties which depend very much on the author. In order to present potential usage of the benchmark specification, a case study was conducted. Two sets of tools for defect detection in requirements were compared from the point of view of efficiency and accuracy.

In the future it would be beneficial to extend the use-case database with more use-cases coming from commercial projects. This would require an iterative approach to updating the typical-profile as well as the referential specification.

Fig. 1 .

 1 Fig. 1. Use-Cases-based functional requirements specification model

A 5 10 15 Project

 515 B C D E F G H I J K Number of steps in main scenario b)

Fig. 4 .

 4 Fig. 4. Distributions of actors steps-sequences lengths in referential specification, a) histogram presents the length of the steps sequences performed by main actor, b) histogram presents length of the steps sequences performed by secondary actor -e.g. System

Table 1 .

 1 Analysed

			projects requirements-specifications (origin: industry -
	project developed by software development company, s2b -project developed by
	students for external organisation, external -specification obtained from the ex-
	ternal source which is freely accessible through the Internet -this refers to two
	specifications: UKCDR [21], PIMS [18]; projects D and K come from the same
	organisation)
	ID	Specification Language	Origin	Business Number of use cases All User Sub-function	Description
	S2B S2B Project C English External Project A English Project B English	17 37 39	0% 19% 46% 35% 76% 24% 18% 44% 33%	Web & standalone application for managing members of organization Web-based Customer Relationship Management (CRM) system UK Collaboration for a Digital Repository (UKCDR)
				77	0%	96%	4%
			S2B	41	0% 100% 0%
				10	0% 100% 0%
				90	0%	81% 19%
				16	19% 56% 25%
				21	38% 57%	5%
				9	0%	67% 33%
				75	0%	97%	3%

Table 2 .

 2 Use-Cases Database analysis according to the presented requirements specification model (see section 2)

	Overall A B C D E F G H I J K 432 17 37 39 77 41 10 90 16 21 9 75 4.87 4.76 4.92 2.95 4.34 5.78 3.90 5.10 3.38 4.33 3.67 6.36 2.48 0.97 1.46 2.69 2.25 1.26 1.20 2.41 0.50 2.01 1.32 3.25 72.9% 94.1% 51.4% 41.0% 55.8% 92.7% 100% 68.9% 81.3% 90.5% 55.6% 98.7% 1.50 1.29 0.57 0.95 0.92 1.63 1.00 1.28 2.94 2.33 1.00 2.69 1.84 0.77 0.60 1.72 1.12 0.62 0.00 1.30 2.98 1.58 1.58 2.91 2.51 1.80 2.52 1.00 1.45 N/A 1.10 2.77 2.30 1.64 1.44 3.09 1.62 0.84 0.87 0.00 0.59 N/A 0.32 1.87 0.65 0.67 0.53 1.80 3.0% 3.7% 5.5% 11.3% 1.8% 0.0% 0.0% 0.0% 27.8% 17.6% 3.0% 0.0% 46.6% 9.1% 76.2% 64.9% 63.4% 40.3% 100% 50.4% 78.7% 89.8% 100% 15.3% 62.7% 42.3% 93.1% 88.6% 37.0% 61.9% 87.5% 91.7% 47.4% 52.4% 50.0% 52.6% Project	20.1% 23.1% 3.5% 6.8% 34.8% 36.1% 12.5% 0.0% 0.0% 19.1% 42.9% 16.4%	9.8% 26.9% 3.5% 4.6% 16.3% 0.0% 0.0% 8.3% 31.6% 23.8% 7.1% 12.9%	3.9% 7.7% 0.0% 0.0% 6.5% 0.0% 0.0% 0.0% 21.1% 0.0% 0.0% 8.6%	3.5% 0.0% 0.0% 0.0% 5.4% 2.1% 0.0% 0.0% 0.0% 4.8% 0.0% 9.5%	80.6% 82.6% 96.3% 72.2% 67.9% 100% 100% 90.0% 50.0% 12.5% 62.5% 72.1%	13.3% 17.4% 3.7% 22.2% 29.6% 0.0% 0.0% 8.0% 16.7% 43.8% 37.5% 14.8%	3.3% 0.0% 0.0% 0.0% 0.0% 0.0% 0.0% 2.0% 33.3% 25.0% 0.0% 7.4%	1.9% 0.0% 0.0% 5.6% 2.5% 0.0% 0.0% 0.0% 0.0% 0.0% 0.0% 4.1%	0.9% 0.0% 0.0% 0.0% 0.0% 0.0% 0.0% 0.0% 0.0% 18.8% 0.0% 1.6% 38.0% 0.0% 0.0% 100% 0.0% 0.0% 0.0% 100% 56.3% 100% 0.0% 6.7% 13.7% 0.0% 0.0% 0.0% 32.5% 0.0% 0.0% 0.0% 0.0% 0.0% 0.0% 44.2% 1.98 0.00 0.00 0.00 3.20 0.00 0.00 0.00 0.00 0.00 0.00 1.09 1.69 N/A N/A N/A 2.02 N/A N/A N/A N/A N/A N/A 0.29 48.5% 82.4% 100% 0.0% 0.0% 97.6% 0.0% 0.0% 0.0% 23.8% 77.8% 0.0% 10.6% 0.0% 0.0% 97.4% 0.0% 0.0% 0.0% 0.0% 0.0% 0.0% 0.0% 0.0% 36.3% 100% 100% 100% 0.0% 100% 0.0% 0.0% 68.8% 57.1% 0.0% 0.0% 3.2% 1.2% 1.1% 17.4% 0.3% 0.0% 0.0% 0.0% 0.0% 0.0% 0.0% 9.0% 6.3% 0.0% 0.5% 0.0% 0.0% 0.0% 25.6% 14.2% 0.0% 0.0% 6.1% 33.3% 71.9% 27.3% 100% 8.1% 87.3% 0.0% 100% 100% 100% 100% 100% 100% 28.1% 72.7% 0.0% 91.9% 12.7% 100% 0.0% 0.0% 0.0% 0.0% 0.0% 0.0%
	Property	SD Number of steps in main scenario Mean Number of use cases Use cases with extensions Mean SD Number of extensions in use case Mean SD Number of steps in extension Steps with validation actions Extensions which are validations 1	2 Main actor's steps sequence length 3 in main scenario 4	>4	1	2 Secondary actor's steps sequence 3 length in main scenario 4	>4 Use cases with additional description Number of use cases with sub-scenario Mean SD Number of steps in sub-scenario Use cases with pre-conditions Use cases with post-conditions Use cases with triggers Steps with conditional clauses Number of steps with reference to use cases Number of extensions with scenario Number of extensions with stories
		Requirements specification independent					Requirements specification dependent

Table 3 .

 3 Referential specification profile in comparison to the average profile derived from the UCDB use-cases analysis

	SD SD SD Mean Mean Mean 1 Extensions of validation nature Property Number of steps in main scenario Use Cases with extensions Number of extensions in use case Number of steps in extension Steps of validation nature Steps with conditional clauses 2 3 4 Main actor's steps sequence length in main scenario >4 1 2 3 4 >4 Secondary actor's steps sequence length in main scenario	4.89 1.47 70.3% 1.50 0.69 2.49 2.12 Referential Specification Admission System 2.2% 46,2% 0.6% 62.3% 21.3% 9.8% 3.3% 3.3% 80.7% 12.9% 4.8% 1.6% 0.00%	4.87 2.48 72.92% 1.50 1.84 2.51 Observed in Use-Cases Database 1.62 3.0% 46.6% 3.2% 62.7% 20.1% 9.8% 3.9% 3.5% 80.6% 13.3% 3.3% 0.9% 1.9%

Table 5 .

 5 Case-study results (tools are written in Java, so memory was automatically managed -garbage collection)

		Summarised for all components		English grammar parser only
	English grammar parser used Stanford OpenNLP Stanford OpenNLP	54.37 31.21 AC 0.99 0.99 Overall processing time [s]	0.29 0.17 0.96 0.84 Mean time needed to analyse one step [s] Quality Maximal 212 339 0.99 0.99 memory utilization [MB] TP rate TN rate	37.44 14.58 PR 0.82 0.79 Overall processing time [s]	0.8 15.6 Startup time [s]	27 226 Initial memory usage [MB]	547 3925 Memory usage while processing single element [KB]

A number/proportion of any element of the model will be further addressed as a property of the specification

Tests were performed for the tools in two versions: with Stanford and OpenNLP parsers. Each version of the tools analysed the referential specification five times, on the computer with Pentium Core Duo 2.0GHz processor and 2GB RAM.

Acknowledgments. We would like to thank Piotr Godek, Kamil Kwarciak and Maciej Mazur for supporting us with industrial use cases.

This research has been financially supported by the Polish Ministry of Science and Higher Education under grant N516 001 31/0269.

This research has been financially supported by the Polish Ministry of Science and Higher Education grant N516 001 31/0269.


Oksana Nikiforova
email: oksana.nikiforova@rtu.lv

Natalja Pavlova
email: natalja.pavlova@rtu.lv

Open Work of Two-Hemisphere Model Transformation Definition into UML Class Diagram in the Context of MDA

Keywords: Business process diagram, class diagram, MDA, PIM, relationships among classes

Model Driven Architecture (MDA) is based on models and distinguish between a system functionality specification and this specification realization on a given technological platform. MDA consists of four models: CIM (Computation Independent Model), PIM (Platform Independent Model), PSM (Platform Specific Model) and code model, all these are parts of the MDA transformation line: CIM->PIM->PSM->code. A PIM model has to be created using a language which is able to describe a system from various points of view, system behavior, system's business objects, system actors, system use cases and so on. Current paper discusses the application of two-hemisphere model for construction of UML class diagram as a part of PIM. Several solutions for determination of elements of class diagram from two-hemisphere model are currently researched and described in the paper. As well as application of the transformations by example of insurance problem domain are presented in the paper.

Introduction

Model Driven Architecture (MDA) is a framework being built under supervision of the Object Modeling Group (OMG) [1]. MDA separates system business aspects from system implementation aspects. MDA defines the approach and tool requirements to specification of systems independently of platforms, specification of platforms, choosing of particular platforms to the systems, and transformation of specifications of business domains into specifications that include specific information of platforms, which have been chosen. MDA proposes a software development process in which the key notions are models and model transformations [START_REF] Kent | Model driven engineering[END_REF]. Software is built by constructing one or more models, and transforming them into other models in this process. The common view on this process is as follows: input is platform independent models and output is platform specific models. The platform specific models can be easily transformed into an executable format [START_REF] Kleppe | MCC: A model transformation environment[END_REF].

There is a more generic view in Model Driven Architecture [START_REF] Kleppe | MDA Explained: The Model Driven Architecture. Practise and Promise[END_REF]. A difference between platform independent models and platform specific models is not dominant in this case. The key of this view is that the software development process is implemented by an intricate sequence of transformation executions that are combined in various ways. This makes system development much more open and flexible [START_REF] Kleppe | MCC: A model transformation environment[END_REF].

The MDA idea is promising -raising the level of abstraction, on which systems are developed. Therefore, it will be possible to develop systems that are more complex in a qualitative way. The basic goal in recent researches in the area of MDA is to achieve a system representation, which corresponds to business requirements, at the highest level of abstraction as possible. Nowadays, MDA tools support formalization of transformations between PIM and PSM stages, and researchers try to "raise" it up as high as possible to fulfill the main statement of MDA [START_REF] Nikiforova | Formal Development of Platform Independent Model in the Framework of MDA: Myth or Reality[END_REF], [START_REF] Pavlova | Several Outlines of Graph Theory in Framework of MDA[END_REF]. The paper shows state of the art of two-hemisphere model application to generation of elements of class diagram and presents several solutions which address the problems stated above and try to "raise" up the level of transformations into the transformations inside PIM.

Section 2 describes two-hemisphere model and define main components of it suitable for generation of elements of UML class diagram. As well as structure of source and target models is defined in Section 2. Section 3 defines all possible transformations from elements of two-hemisphere model into elements of UML class diagram, which is defined as a target. A practical experiment with the transformations from two-hemisphere model into class diagram is processed in Section 4. Overall statements of the research are discussed in conclusions.

Model Transformations in Terms of Two-Hemisphere Model

Two-hemisphere model driven approach [START_REF] Nikiforova | Two-Hemisphere Model Driven Approach: Engineering Based Software Development[END_REF] proposes to use of business process modeling and concept modeling to represent systems in the platform independent manner and describes how to transform business process models into several elements of UML diagrams. For the first time the strategy was proposed in [START_REF] Nikiforova | General Framework For Object-Oriented Software Development Process[END_REF], where the general framework for object-oriented software development had been presented and the idea about usage of two interrelated models for software system development has been stated and discussed.

Two-hemisphere approach proposes to start software development process based on two-hemisphere problem domain model, where one model reflects functional (procedural) aspects of the business and software system, and another model reflects corresponding concept structures. The co-existence and inter-relatedness of models enables use of knowledge transfer from one model to another, as well as utilization of particular knowledge completeness and consistency checks [START_REF] Nikiforova | Two-Hemisphere Model Driven Approach: Engineering Based Software Development[END_REF].

MDA introduces an approach to system specification that separates the views on three different layers of abstraction: high level specification of what the system is expected to do (Computation Independent Model or CIM); the specification of system functionality (Platform Independent Model or PIM); and the specification of the implementation of that functionality on a specific technology platform (Platform Specific Model or PSM).

Currently available methods do not support formal transformation from CIM to PIM, wherein the PIM would be sufficient for PSM generation [START_REF] Nikiforova | Formal Development of Platform Independent Model in the Framework of MDA: Myth or Reality[END_REF]. The PIM received from the CIM should be refined in order to get the correct transformation into the PSM. Moreover, investigation of the PIM requires a more detailed description of it. That is why it was decided to divide the solution domain into two above-mentioned levels: the first one closer to the CIM and the second one closer to the PSM. As previously mentioned, the second level of the solution domain is an application level. Because this level is closer to the PSM, models with further automation should be represented here. A model on the application level of the solution domain is class diagram. A model on the application level should be sufficient for formal transformation to the Platform Specific Model. Therefore, data structure, attributes, system functions and main algorithms should be presented in the PIM ready to transformation into PSM [START_REF] Nikiforova | Formal Development of Platform Independent Model in the Framework of MDA: Myth or Reality[END_REF].

CIM presents specification of the system at problem domain level and can be transformed into elements of PIM. PIM provides formal specification of the system structure and functions that abstracts from technical details, and thus presents solution aspects of the system to be developed, which enables model transformation to the platform level (PSM), named implementation domain in Figure 1. The details in the right column of the table in Figure 1 correspond to the twohemisphere approach, which addresses the construction of information about problem domain by use of two interrelated models at problem domain level, namely, the process model and the conceptual model. The conceptual model is used in parallel with process model to cross-examine software developers understanding of procedural and semantic aspects of problem domain.

The main idea of MDA is to achieve formal system representation at the as high level of abstraction as possible. One of the most important and problematic stages in MDA realization is derivation of PIM elements from a problem domain, and PIM construction in the form that is suitable for the PSM [START_REF] Nikiforova | Formal Development of Platform Independent Model in the Framework of MDA: Myth or Reality[END_REF]. It is necessary to find the way to develop PIM using formal representation, so far keeping the level of abstraction high enough. PIM model should represent system static and dynamic aspects. Class diagram shows static structure of the developed system and is the central component of PIM. But UML is a modeling language and does not have all the possibilities to specify context and the way of modeling, which is required always to be defined in a methodology. Therefore the construction of class diagram has to be based on well defined rules for its elements generation from the problem domain model presented in the form suitable for that.

The MDA framework implies system development based on modeling, not on programming activities. System development is divided into three stages according to the level of abstraction. Every stage is denoted with a model. The model is often presented as a combination of drawings and text [1].

A transformation tool or approach takes a model on input and creates another model on output, see Figure 2 [START_REF] Kleppe | MDA Explained: The Model Driven Architecture. Practise and Promise[END_REF]. The two-hemisphere model has been marked as input with mapping rules, the class diagram and transformation trace has been received on output. Transformation trace shows the plan how an element of the twohemisphere model is transformed into the corresponding element of the class diagram, and which parts of the mapping are used for transformation of every part of the two-hemisphere model [1]. Figure 2 shows how a transformation tool takes input -the two-hemisphere model and receives output -the class diagram. All elements of the source model are shown in Table 1. It is elements of the business process model and concept model. A notation of the business process model is optional, however, it must reflect the following components of business process model: processes; performers; information flows; and information (data) stores [START_REF] Nikiforova | Two-Hemisphere Model Driven Approach: Engineering Based Software Development[END_REF]. Real-world classes relevant to the problem domain and their relationships are presented in concepts model. It is a variation of well known ER diagram notation [START_REF] Chen | The entity relationship model -towards a unified view of data[END_REF] and consists of concepts (i.e. entities or objects) and their attributes. The notational conventions of the business process diagram give a possibility to address concepts in concept model to information flows (e.g. events) in process model. The elements of the source model are listed in the first column of Table 1. The second column describes the main elements of the source model. Business Process usually means a chain of tasks that produce a result which is valuable to some hypothetical customer. A business process is a gradually refined description of a business activity (task) [START_REF]Language Guide[END_REF].

Business process diagram/Event name transfer name set option repeat option

Events are defined (as a rule) in the moment when they are mentioned for the first time in BP or TD diagrams. Events are an input/output object (or more precisely -the arrival of an input object and departure of an output object) of certain business process. These objects can be material things or just information [START_REF]Language Guide[END_REF]. BP diagram/Data store store name comment ER model<ER name>

The data store is a persistent (independent of the current task) storage of data or materials. In the case of an information system, the data store most likely will be converted to a database with a certain data structure (Entity Relationship Model). On the highest levels of business models, the data store can be used to denote an archive of data or it can also be used to represent a warehouse or stock of goods [START_REF]Language Guide[END_REF].

Concept model/Concept name

Conceptual classes that are software (analysis) class candidates in essence. A conceptual class is an idea, thing, or object. A conceptual class may be considered in terms of its symbolswords or images, intensions -definitions, and extensions -the set of examples [START_REF] Larman | Applying UML And Patterns: An Introduction To Object-Oriented Analysis And Design[END_REF].

Concept model/Attribute name type

An attribute is a logical data value of an object [START_REF] Larman | Applying UML And Patterns: An Introduction To Object-Oriented Analysis And Design[END_REF].

The elements of source model are important for further system analysis and design. Information from these elements is significant, and nothing from it should remain without any usage on the lowest levels of abstraction. Business processes or tasks present system functionality, its activities and operations. If this information is lost it is necessary to find system functions for implementing operations of classes in description of the problem domain. Events, data stores and data objects are parts of the data structure model. With these elements initial static structure is presented in the two-hemisphere model, and should be transited into the class diagram. Associations and attributes in the concept model are useful for definition of relationships between objects of system static structure (classes).

The elements of the target model are listed in Table 2. Only the main elements of the class diagram are shown there.

Element of Source model Description Class diagram/Class

A class is the descriptor for a set of objects with similar structure, behavior, and relationships [START_REF] Larman | Applying UML And Patterns: An Introduction To Object-Oriented Analysis And Design[END_REF].

Class diagram/Class/Attribute name type

An attribute is a logical data value of an object [START_REF] Larman | Applying UML And Patterns: An Introduction To Object-Oriented Analysis And Design[END_REF].

Class diagram/Class/Operation name return type argument precondition postcondition

The UML formally defines operations. To quote: "An operation is a specification of a transformation or query that an object may be called to execute" [START_REF] Rumbaugh | The unified modeling language reference manual[END_REF].

Class diagram/Relationship type multiplicity role

A relationship between instances of the two classes. There is an association between two classes if an instance of one class must know about the other in order to perform its work [START_REF] Larman | Applying UML And Patterns: An Introduction To Object-Oriented Analysis And Design[END_REF].

Class diagram/Class/Stereotype

Stereotypes, which provide a way of extending UML, are new kinds of model elements created from existing kinds [START_REF] Larman | Applying UML And Patterns: An Introduction To Object-Oriented Analysis And Design[END_REF].

Class diagram/Constraint

A constraint is a condition that every implementation of the design must satisfy [START_REF] Larman | Applying UML And Patterns: An Introduction To Object-Oriented Analysis And Design[END_REF].

It is necessary to find the way how source model elements can be transformed into target model elements according to the definition of transformations in the framework of MDA.

Application of Two-Hemisphere model for obtaining of elements of class diagram

For the research the source model is two-hemisphere model, or business process and concept diagrams, and the target model is class diagram in terms of UML class diagram. The possible combinations of transition from two-hemisphere model to class diagram will be discussed in this section. Input and output is necessary for any transformation. The transformation discussed here is a transformation inside the PIM -one of the MDA models. In other words, it is a transformation from two-hemisphere model to class diagram.

General Schema of Transformation Abilities

The detailed transformations between models proposed for the application of twohemisphere model in the paper are shown in Figure 3. Two-hemisphere model consists business process model (graph G1 on Figure 3) and concept model (graph G2 on Figure 3).

The notation of business process model have not a significant value, main requirement to the notation of business process model is possibility to define business processes, performers, events and data flows among business processes. For current research is used business process model constructed with GRAPES [START_REF]Language Guide[END_REF] notation. The second hemisphere is concept model. C.Larman defines concept model as "The concept model captures real-world concepts (objects), their attributes, and the associations between these concepts." [START_REF] Larman | Applying UML And Patterns: An Introduction To Object-Oriented Analysis And Design[END_REF].

In the case of two-hemisphere model authors avoid relations between classes in concept model at business level (of problem domain) and the relations will be defined according system realization at software level (of implementation domain).

For performing of transformation to class diagram the intermediate model (graph G3 on Figure 3) is introduced. Intermediate model is used to simplify the transition between business process and object interaction models, which now is presented in the form of UML collaboration diagram (graph G4 in Figure 3). Figure 3 shows all the transformations from the business process model (G1) and concept model (G2) into the class diagram (G5). Transformations are based on the hypothesis that elements of the class diagram can be received from the twohemisphere model by applying defined techniques of graph transformation [START_REF] Grundspenkis | Causal Domain Model Driven Knowledge Acquisition for Expert Diagnosis System Development[END_REF].

Intermediate model is generated from business process model using methods of directed graph transformation, when arcs of one graph (G1 on Figure 3) are transformed into nodes of another graph (G3 on Figure 3) and nodes of one graph (G1) are transformed into arcs of another graph (G2) [START_REF] Pavlova | Formalization of Two-Hemisphere Model Driven Approach in the Framework of MDA[END_REF]. Figure 3 presents the sequence of transformations from two-hemisphere model to class diagram with dotted arrows. Business process "perform action 1" is transformed into arc "perform action 1" of intermediate model (graph G3 on Figure 3). The next transformation create the method "perform action 1()" in collaboration diagram (graph G4 on Figure 3) from the arc of intermediate model. The last transformation of this business process defines the responsible class of this method in class diagram (graph G5). The element "performer 1" is transformed as a node of intermediate model, and as "actor 1" of collaboration model. This element is defined as "actor 1" in class diagram. Data types for elements "event 1" and "event 3" is defined as "Da-taType A" or "Concept A" of concept model.

Events are transformed into nodes of intermediate model, and then into objects like "Event1: Class A" in collaboration diagram, which serves as a base for classes of class diagram definition. All attributes for classes are determined based on attributes defined in concept model. • The element "performer 1" is transformed as a node of intermediate model, and as "actor 1" of collaboration model. This element is defined as "actor 1" in class diagram.

• Data types for elements "event 1" and "event 3" is defined as "DataType A" or "Concept A" of concept model. Events are transformed into nodes of intermediate model, and then into objects like "Event1: Class A" in collaboration diagram, which serves as a base for classes of class diagram definition.

• All attributes for classes are determined based on attributes defined in concept model. Summarization of mapping of source model into target of model is shown in Figure 4. As it is seen in Figure 4 not all the elements of class diagram defined in Table 2 are received from two-hemisphere model: stereotype and constraint are still under research. But the main components of class diagram are generated from different elements or their combinations of two-hemisphere model: classes, operations, methods and different types of relationships between classes. An illustrative example of definition of classes and their attributes and operations is described in Section 3.2. and transformation rules for definition of different types of relationships between classes in details are discusses in [START_REF] Nikiforova | Foundations of Generation of Relationships between Classes Based on Initial Business Knowledge[END_REF]. And not all the elements of two-hemisphere model are used for identification of elements of class diagram: data stores are avoided due to it duplication by element "task" with different meaning.

An illustrative example of class diagram generation from twohemisphere model

For better understanding of main idea, the example of such model transformations is shown for a fragment of problem domain concerned with insurance activities [START_REF] Pavlova | Approach for Development of Platform Independent Model in the Framework of Model Driven Architecture[END_REF]. Figure 5 presents only fragment of transformation. There is one process "Pay sum" which has output "policy". Concept "policy" defines data type for the output of process. It is transformed into fragment of intermediate model with arc "Pay sum" and node "Policy". Intermediate model allows to receive collaboration diagram, where initial process "Pay sum" is a method of object "Policy".

Concrete object "Policy" belongs to class "Policy", which is defined with corresponding concept. When a collaboration of objects is defined, it is possible to construct class diagram according to rules of object-oriented system modeling [START_REF] Nikiforova | General Framework For Object-Oriented Software Development Process[END_REF].

Practical Experiment with the Processing of Transformations from Two-Hemisphere Model into Class Diagram

During the investigation of receiving of class diagram from two-hemisphere model all possible combination of number and types of incoming and outgoing information flows from nodes of processes are examined [START_REF] Nikiforova | General Framework For Object-Oriented Software Development Process[END_REF]. Different combinations give a possibility to receive different relations among classes.

The tool for business process modeling GRADE (GRADE) [START_REF]GRADE tools[END_REF] gives a possibility to construct two interrelated models (business process and the concept ones) and to generate text description of models with permanent structure, therefore it is chosen as a tool for development of two-hemisphere model and further generation of textual files, which defines all the elements of the model and their relations each to other. Generated text files serve as an input information to support the processing algorithm of the transformations among graphs defined in the Section 3. And as the result the XML file, which contains description of structure of the class diagram generated from the source model. XML format of class specification gives a possibility to receive visual representation of class diagram in any tool, which support import from XML for class diagram development.

To check, that offered transformations are independent from problem domain an experiment with two-hemisphere model of insurance is performed. The transformations are applied for generation of class diagram from two-hemisphere mod-model developed for insurance problem domain (shown in Figure 6) and the result class diagram is shown in Figure 7.

As far as business process and conceptual models are the built-in demo example for system development in GRADE the authors may suppose that the models (e.g. source information) are correct and constructed independently from author participation. Therefore it is possible to address the truthful verification of an experiment. The class diagram in Figure 7 has undefined relations, and unrelated classes, for which additional, detailed, business process models are required. Classes, which are highlighted as gray in Figure 7 are defined as classes which have a restriction. For current level of details it is impossible to define relations of this classes and belonging of method "manage_assets ()" without creating a subprocess diagram for corresponding fragment of business process. After the de-tailed elaboration of the process it is possible to apply transformations one more time and receive more correct relations among classes.

According the restriction of graph transformation with multiple inputs and multiple outputs it can be possible to define processes, which requires additional detailed elaboration. This feature is realized only partly with reporting of the restriction places in the output text file. Not all elements of the class diagram are received from the two-hemisphere model on the current stage of research. Definition of such elements as operation arguments, operation return types, stereotypes, constraints and so on is still researched. There exists the probability that for definition of this attributes, an extension of the initial two-hemisphere model will be required.

The proposed transformations are applied for two-hemisphere model of insurance and classes with attributes and different kinds of relationships are identified based on elements of process and concept models. The ability to define all the types of transformations in a formal way gives a possibility to automate the process of class diagram development from correct and precise two-hemisphere model.

The title of the paper is called "Open work of …" it means that the research is under development. Authors try to find the way to receive the rest elements of class diagram and moreover to find the possibility of define system dynamic in a more precise way.

Fig. 1 .

 1 Fig. 1. Model transformation from problem domain level of knowledge representation into implementation domain level according 2HMD approach.

Fig. 2 .

 2 Fig. 2. Structure of model transformation tool in the framework of MDA.

Fig. 3 .

 3 Fig. 3. Essence of application of two-hemisphere model for generation of elements of class diagram.

Figure 3

 3 Figure 3 presents how elements of two-hemisphere model are transformed into elements of class diagram. The ways of receiving of the following elements are shown with arrows in Figure 3: • Business process "perform action 1" is transformed into arc "perform action 1" of intermediate model. The next transformation create the method "perform action 1()" in collaboration diagram from the arc of intermediate model. The last transformation of this business process defines the responsible class of this method in class diagram.

Fig. 4 .

 4 Fig. 4. Mapping of elements of source model into elements of target model.

Fig. 4 .

 4 Fig. 4. An example of process and concept elements transformation into class elements.

Fig. 6 .

 6 Fig. 6. Initial business process and concept models for Insurance problem domain.

Fig. 7 . 5 Conclusions

 75 Fig. 7. Class diagram for Insurance business.The visualization with indicating of a process is not realized because the tool developed for processing of transformations from two-hemisphere model into class diagram does not support yet diagramming abilities, but receiving of XML code gives a possibility to create class diagram with any tool, which support export from XML.

Table 1 .

 1 Elements of source model.

	Elements of Source model	Description
	Business process diagram/ Proc-
	ess
	process name
	description
	triggering condition
	performer
	expression
	duration
	start option
	end option
	no start option
	tag
	assignment

Table 2 .

 2 Elements of target model.

Acknowledgements

The research reflected in the paper is supported by the research grant No. R7389 of Latvian Ministry of Education and Science in cooperation with Riga Technical University "Development of tool prototype for generation of software system class structure based on two-hemisphere model." and by the European Social Fund within the National Programme "Support for the carrying out doctoral study program's and post-doctoral researches".