Daniel Sinnig

Ferhat Khendek
email: khendek@ece.concordia.ca

Patrice Chalin
email: chalin@encs.concordia.ca

Partial Order Semantics for Use Case and Task Models

Keywords: Use Case Models, Task Models, Partially Ordered Sets, Semantics, Formal Framework

Use case models are the specification medium of choice for functional requirements, while task models are employed to capture User Interface (UI) requirements and design information. In current practice, both entities are treated independently and are often developed by different teams, which have their own philosophies and lifecycles. This lack of integration is problematic and often results in inconsistent functional and UI design specifications causing duplication of effort while increasing the maintenance overhead. To address these shortcomings, we propose a formal semantic framework for the integrated development of use case and task models. The semantic mapping is defined in a two step manner from a particular use case or task model notation to the common semantic domain of sets of partially ordered sets. This two-step mapping results in a semantic framework that can be more easily reused and extended. The intermediate semantic domains have been carefully chosen by taking into consideration the intrinsic characteristics of use case and task models. As a concrete example, we provide a semantics for our own DSRG use case formalism and an extended version of ConcurTaskTrees, one of the most popular task model notations. Furthermore, we use the common semantic model to formally define a set of refinement relations for use case and task models.

Introduction

Use case models are the artifact of choice for functional requirements specification [START_REF] Cockburn | Writing Effective Use Cases[END_REF] while User Interface (UI) design typically starts with the creation of a task model [START_REF] Pressman | Software engineering: A practitioner's approach[END_REF]. In current practice, UI design and the specification of functional requirements are generally carried out by different teams using different theories, models and lifecycles [START_REF] Seffah | Software and Usability Engineering: Prevalent Myths, Obstacles and Integration Avenues, chapter in Human-Centered Software Engineering -Integrating Usability in the Software Development Lifecycle[END_REF]. As a consequence, interrelated artifacts, such as use cases and task models, are often created independently of each other. The following issues result directly from this lack of integration: Possible conflicts during implementation; software engineering and UI design processes do not have the same reference specification and thus may result in inconsistent designs. Duplication in effort during development and maintenance due to redundancies and overlaps in the (independently) developed UI and software engineering models. A process allowing for UI design to follow as a logical progression from a functional requirements specification does not exist [START_REF] Sinnig | Common Semantics for Use Cases and Task Models[END_REF]. Our primary research goal is to define an integrated methodology for the development of use cases and task models within an overall software process. Such an integrated development methodology could serve

Use case and task modeling

In this section we provide the necessary background information on use case and task modeling. For each concept we present the main features, concrete notations (i.e., DSGR-style use case models and ECTT task models), and a comprehensive example. Finally, both concepts are compared and main commonalities and differences are contrasted.

Use case models

Use cases were introduced in the early 90s by Jacobson [START_REF] Jacobson | Object-Oriented Software Engineering: A Use Case Driven Approach[END_REF]. He defined a use case as a "specific way of using the system by using some part of the functionality." Use case modeling is making its way into mainstream practice as a key activity in the software development process (e.g. Rational Unified Process). There is accumulating evidence of significant benefits to customers and developers [START_REF] Merrick | The Rationale for OO Associations in Use Case Modelling[END_REF]. The use case model captures the complete set of use cases for an application, where each use case specifies possible usage scenarios for a particular functionality offered by the system. As such, the use case model documents the majority of software and system requirements and serves as a contract between stakeholders about the envisioned system behavior [START_REF] Cockburn | Writing Effective Use Cases[END_REF].

While some of the original concepts in use case modeling have evolved through the work of researchers and practitioners, the fundamental idea remains the same; that is, a use case describes the way a system is employed by its actors to achieve their goals [START_REF] Armour | Advanced Use Case Modeling[END_REF]. In other words, a use case captures the interaction between actors and the system under development. Actors represent users or entities (e.g., secondary systems) that interact with the system. By definition actors are outside of the system boundary. It is distinguished between primary and secondary actors. The primary actor, typically a user, initiates the use case in order to accomplish a pre-set goal. Secondary actors play the role of supporting the execution of the use case and may participate in the interaction later [START_REF] Gomaa | Designing Software Product Lines with UML[END_REF].

Different notations for expressing use cases possessing different degrees of formality have been suggested. The extremes range from purely textual constructs written in prose [START_REF] Cockburn | Writing Effective Use Cases[END_REF] to entirely formal specifications written in Z [START_REF] Butler | A Z Specification of Use Cases[END_REF], as Abstract State Machines (ASM) [START_REF] Grieskamp | Testable Use Cases in the Abstract State Machine Language[END_REF][START_REF] Barnett | Validating use-cases with the AsmL test tool[END_REF], or as graph structures [START_REF] Mizouni | Formal Composition of Partial System Behaviors[END_REF]. While the use of prose makes use case modeling an attractive tool for facilitating communication among stakeholders, its informal Partial Order Semantics for Use Case and Task Models 3 nature makes it prone to ambiguities and thus leaves little room for tool support. In this article, we adopt an intermediate solution, called DSRG-style use case model, which enforces a formal structure but also preserves the intuitive nature of use cases. I.e., we provide support for formalizing the sequencing of use case steps and their types, but the respective actions, as well as the associated conditions are specified informally. The property section of the use case, except for the discrete goal-level property is specified using narrative language.

Fig. 1 portrays the structure of the DSRG-style use case notation first introduced in [START_REF] Sinnig | Consistency between Task Models and Use Cases[END_REF]. Similar to Cockburn [START_REF] Cockburn | Writing Effective Use Cases[END_REF], each use case starts with a header section containing the various properties. The "primary actor" property identifies the actor who initiates the interaction specified by the use case. The "goal" property captures the very intent the primary actor has in mind when executing the use case. "Level" indicates the goal-level of the use case. While different goal-levels exist, -the most important ones are summary, user goal and sub-function. The "precondition" property denotes a condition that must hold, in order to carry out the use case.

The core part of a use case is its main success scenario, which follows immediately after the header. It indicates the most common way in which the primary actor can reach his/her goal by using the system. A use case is completed by specifying the use case extensions. These extensions define alternative scenarios which may or may not lead to the fulfillment of the use case goal. They represent exceptional and alternative behavior (relative to the main success scenario) and are indispensable to capturing full system behavior. Each extension starts with a condition (relative to one or more steps of the main success scenario), which makes the extension relevant and causes the main success scenario to branch to the alternative scenario. The condition is followed by a sequence of use case steps, which may lead to the fulfillment or the abandonment of the use-case goal and/or further extensions. From a requirements point of view, exhaustive modeling of use case extensions is an effective requirements elicitation device.

The main success scenario as well as each extension consists of a sequence of use-case steps, which can be of seven different kinds. Atomic steps are performed either by the primary actor or the system and do not contain any sub-steps. Choice steps provide the primary actor with the choice between several interactions. Each such interaction is (in turn) defined by a sequence of steps. Concurrent steps define a set of steps which may be performed in any order by the primary actor. Goto steps denote jumps to steps within the same use case. Include steps define the inclusion of a sub-use case. Success and Failure denote the successful or unsuccessful termination of use case scenario, respectively.

An example use case is given in Fig 2 . The use case captures the interactions for the "Order Product"

All Choice Sequence

Legend:

Fig. 1. DSRG-style use case structure functionality of an Invoice Management System (IMS). The main success scenario of the use case describes the situation in which the primary actor directly accomplishes his/her goal of ordering a product. The extensions specify alternative scenarios which lead to the abandonment of the use case goal. Since this "Order Product" use case is used as a running example for the subsequent syntax and semantics definitions, each use case step is further attributed an abbreviating label, which serves as a short-hand for the narrative action description.

Task models

Task modeling is a well accepted technique supporting user-centered UI design [START_REF] Paternò | Model-Based Design and Evaluation of Interactive Applications[END_REF]. In most UI development approaches, the task set is the primary input to the UI design stage. Task models capture the complete set of tasks that users perform using the application, as well as how the tasks are related to each other. The origin of most task modeling approaches can be traced back to activity theory [START_REF] Kuutti | Activity theory as a potential framework for human-computer interaction research, chapter in Context and consciousness: activity theory and human-computer interaction[END_REF], where a human operator carries out activities to change part of the environment in order to achieve a certain goal [START_REF] Dittmar | Higher-Order Task Models[END_REF]. Like use cases, task models describe the user"s interaction with the system. Their primary purpose is to systematically capture the way users achieve a goal when interacting with the system [START_REF] Souchon | Task Modelling in Multiple contexts of Use[END_REF]. More precisely, a task model specifies how the user makes use of the system to achieve a goal but also indicates how the system supports the involved (sub)tasks. Various notations for task models exits. Among the most popular ones are ConcurTaskTrees (CTT) [START_REF] Paternò | Model-Based Design and Evaluation of Interactive Applications[END_REF], GOMS [START_REF] Card | The Psychology of Human Computer Interaction[END_REF], TaO Spec [START_REF] Dittmar | Tool Support for Task Modelling -A Constructive Exploration[END_REF], and HTA [START_REF] Duncan | Task Analysis and Training Design[END_REF]. Even though all notations differ in terms of presentation, level of formality, and ex- 1. ECTT defines two novel temporal operators Stop and Resume which allow modeling error and failure cases, and provide a mechanism to "catch" errors and prevent their propagation. Intuitively, Stop and Resume denote the deactivation and reactivation of the respective operand task. As such their interplay is similar to the throw and corresponding catch of an exception of programming languages like Java. A task which "throws" a Stop exception cannot enable any tasks. Stop denotes an exceptional case, which, "untreated", leaves the superordinate task incomplete and thus inevitably leads to the premature termination of a scenario. Resume is used to "catch" a Stop exception and as such counteracts and limits the effects of Stop. After Resume, the execution of the affected task returns back to "normal"; i.e. its execution will enable respective subsequent tasks.

2. ECTT is defined in a modular fashion allowing task model to be developed in a true top-down manner while taking advantage of encapsulation. Each ECTT task model consists of a set of atomic tasks and task definitions, where each task definition denotes a high-level task. High-level tasks are further decomposed into so-called task expressions, which are compositions of lower-level task definitions or task references. Task references denote the inclusion of already existing task definitions. In contrast to CTT (which only allows the inclusion of tasks within the same task-tree hierarchy), an ECTT task definition allows the inclusion of any task definition which belongs to the ECTT task model, regardless of whether it is part of the same task hierarchy or not.

Similar to CTT, tasks are arranged hierarchically, with more complex tasks decomposed into simpler sub-tasks. ECTT includes a set of binary and unary temporal operators. The former are used to temporally link sibling tasks, at the same level of decomposition, whereas the latter are used to identify optional and iterative tasks. A summary of ECTT operators together with their intuitive interpretation is given in Table 1. We note that most binary operators (except for suspend/resume) have similar (yet not semantically identical) counterparts in LOTOS [START_REF] Interactions | ISO 8807: LOTOS -A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour[END_REF].

An example of an ECTT task model is given in Fig. 3. It corresponds to the "Order Product" use case defined in The task model is visualized as a task tree, which clearly portrays the hierarchical breakdown of high-level tasks into lower-level tasks. The execution order of tasks is determined by temporal operators that are defined between peer tasks. An indication of task types is given by the used symbol to represent tasks. ECTT distinguishes between three different task types: interaction tasks, application tasks, and abstract tasks. While interaction tasks are performed by the user (through the UI), application tasks are performed by the system and have an externally visible outcome to the user. Abstract tasks denote high-level tasks which can involve both interaction and application tasks.

Use case vs. task models

In the previous sections, the main characteristics of use case and task models were presented. In what follows, we will analyze and compare both kinds of artifacts and outline noteworthy differences and commonalities. Use case and task models are both scenario-based and as such capture sets of usage scenarios of the system. On one hand, a use case describes system functionality by means of a main success scenario and extensions. On the other hand, a task specification captures user-system interactions within a hierarchical task tree. At a certain level of abstraction, both models can be used to capture the same information. In current practice, however, use case models are employed to document functional requirements whereas task models are used to describe UI requirements and/or designs. We identify two main differences that are pertinent to their purpose of application:

In use case models, requirements are captured at a higher level of abstraction whereas task models are more detailed. Hence, the atomic actions of a task specification are often lower-level UI details that are irrelevant (actually contraindicated [START_REF] Cockburn | Writing Effective Use Cases[END_REF]) in the context of a use case.

Task models concentrate on aspects that are relevant for UI design and as such, usage scenarios are strictly depicted as input-output relations between the user and the system. System interactions that are hidden from the end user (e.g. involvement of secondary actors or internal computations), as specified in use case models, are not captured. Ideally, the functional requirements captured in use cases are independent of a particular user interface [START_REF] Cockburn | Writing Effective Use Cases[END_REF]. On the contrary, the requirements and design information captured in task models take into account the specifics of a particular type of user interface. In other words, the use case model captures the bare functional requirements of the system, which are then "instantiated" to a particular type of user interface by means of a task model specification. If the application supports multiple UIs (e.g. Web UI, GUI, Mobile, etc.) then one use case is refined by several task models; one for each "type" of user interface. If given the choice, a task model may only implement a subset of the scenarios specified in the use case model. Task models are geared to a particular user interface and as such must obey its limitations. E.g., a voice user interface will most likely support less functionality than a fully-fledged graphical user interface. Generally, refinement between the two models can take two different forms: (1) Structural (event) refinement, which consists of breaking previously atomic use case steps or tasks into sub-steps and sub-tasks respectively; and/or (2) Behavioral refinement, which restricts the set of possible scenarios.

If we compare the "Order Product" use case (Fig 2) with the "Order Product" ECTT task model (Fig. 3) we note that the task model has more UI details. For example use case step 1 ("Specification of Product Category") has been refined by two sequential tasks ("Selection Criteria" and "Submit Criteria"). Moreover, the task model only implements a subset of the functionality of the use case. From a pure functionality point of view (use case) the system supports both payment by credit card and payment by debit card. The capabilities of the UI (task model), however only allows the user to pay by credit card. Finally it is noticeable that the task model does not specify corresponding tasks for use case steps 4 and 7. These steps denote internal system interactions which are irrelevant for UI design.

Formal framework

In this section we provide a general overview of our framework for formalizing use case and task models. Fig. 4 illustrates how our framework promotes a two-step mapping from a particular use case or task model notation to the common semantic domain which is based on sets of partially ordered sets (sets of posets). The semantic mapping is performed in two steps: First, the source models are mapped to respective intermediate semantic domains, followed by mappings to the common semantic domain. The main reason behind a two-step mapping, rather than a direct mapping, is to provide a semantic framework that can be more easily reused and extended. The intermediate semantic domains have been carefully chosen by taking into consideration the intrinsic characteristics of task models and use cases, respectively, so that the mappings to the intermediate semantic domains are straightforward and intuitive: task models are mapped into what we call Generic Task Expressions (GTE); use cases are mapped to Use Case Labeled Transition Systems (UC-LTS). Since the second level mappings to sets of posets are more involved, the intermediate semantic domains have been chosen so as to be as simple as possible, containing only the necessary core constructs. As a consequence of this two-step semantic definition, we believe that our framework can be easily extended to incorporate new task model or use case notations by simply defining a new mapping to the intermediate semantic domain.

In the next sections we define the various components of the framework. We start by providing an abstract syntax for a particular use case and task model notation, namely the before-mentioned DSRG-style use case models and Extended Concurrent Task Trees (ECTT). Then we introduce UC-LTS and GTE as intermediate semantic domains and define the involved mappings. Finally we provide formalizations of the semantic mapping to sets posets.

Abstract syntax

Abstract syntax for DSRG-style use case models

We define a DSRG-style use case model as a collection of use cases with one use case designated as the root use case.

Definition 1 (DSRG-style use case model). A DSRG-style use case model is a pair

where, is the name of the root use case and is a map of use case definitions (with a finite domain) such that . If then we shall write , sometimes omitting the subscript, when it is clear from the context.

The abstract syntax for an individual use case is given in Fig. 5 as an Isabelle/HOL theory 1 [START_REF] Nipkow | Isabelle/HOL: A Proof Assistant for Higher-Order Logic[END_REF]. Analogously to the informal definition discussed in Section 2.1, each use case is defined as a record consisting of a use case name, a set of properties, a main success scenario, and a set of extensions. The main success scenario consists of a list of use case steps among which we distinguish between seven different step kinds (datatype ). A use case extension is defined as a record consisting of an identifier, a condition, and a list of use case steps. The latter denote an alternative flow, relative to the main success scenario (or a super-ordinated extension). In case of atomic use case steps we further distinguish between three different step types: steps of type interaction are performed by the primary actor, whereas steps of types application and internal are carried out by the system, with the difference that the former have an externally visible effect (to the primary actor) while the effects of the latter are invisible.

1 Expressing parts of our formal system in Isabelle allowed us to use the Isabelle theorem prover to verify basic well-formedness properties such as syntax and type checking CTT ….. As well-formedness conditions, we required that (1) all use case steps and extension IDs be unique, (2) for every step or extension reference, there exist a corresponding use case step or use case extension within the same use case, respectively, (3) for every we require that and that there be no circular inclusions, and (4) the last element of every use case step sequence be either , , or . In order to illustrate the syntactic definition of a use case, let us reconsider the previously depicted "Order a Product" use case. Fig. 6 portrays parts of its formalization in Isabelle/HOL. For the sake of conciseness, for each atomic step, instead of the full description, the abbreviating label has been used.

Generic Task Expression (GTE)

Sets of POSETS

' |), MainSuccessScenario = [ Atom ''s1'' INTERACTION ''spCA'' {}, Atom ''s2'' APPLICATION ''diSR'' {}, Atom ''s3'' INTERACTION ''slPQ'' {''e1''}, Atom ''s4'' INTERNAL ''vaPQ'' {''e2''}, Atom ''s5'' APPLICATION ''diPS'' {}, Choice ''s6'' [ [Atom ''s6A1'' INTERACTION ''paCC'' {} ], [Atom ''s6B1'' INTERACTION ''paDB'' {} ] ] {''e3''}, Atom ''s7'' INTERNAL ''vaPA'' {''e4''}, Atom ''s8'' APPLICATION ''inCO'' {}, Success ''s9'' ],

Abstract syntax for ECTT task models

In this section, we define an abstract syntax for ECTT task models. In contrast to CTT, the various task definitions ( ) do not need to be connected by some task-subtask hierarchy. This allows for a more modular setup, enabling the UI designer to work on multiple task hierarchies concurrently and eventually connect them using references. The creation of a single monolithic task tree (as required by CTT) is not necessary. For an ECTT task model to be well-formed, we require that contain only non-recursive task definitions, that the task type of atomic tasks be either or and that direct and indirect operands of ||, |>, [> be of type interaction. In order to illustrate the before-mentioned definitions let us reconsider the "Order Product" task model visualized by Fig. 3. The corresponding formalization as an ECTT task model is depicted in Fig. 7. Leaf task names are abbreviated by the label displayed underneath the respective task symbols.

Definition 2 (ECTT task model). An

Intermediate semantic domains

In this section we introduce use case labeled transition systems (UC-LTSs) and generic task expressions (GTEs) as intermediate semantics domains for use case and task models, respectively. We also formally define the mappings from DSRG-style use case models and ECTT task models to their respective intermediate semantic domains.

UC-LTS

The intermediate semantic domain for use case models is UC-LTSs. Its definition is similar to the definition of an ordinary LTS [START_REF] Baeten | Process algebra[END_REF] with the exception that transitions are associated with sets of labels rather than single labels.

Definition 3 (Use case labeled transition system). A Use case labeled transition system (UC-LTS) is a tuple

, where is the set of labels representing atomic use case steps, is a set of states, is the initial state, is the set of final states and is the (total) transition function.

We believe that UC-LTSs are defined in a manner which easily and intuitively captures the nature of use cases, as we explain next. A use case primarily describes the possible execution order of user and system actions in the form of use case steps: from a given state, the execution of a step leads into another state. Accordingly, in UC-LTSs, the execution of a step (or set of steps, as we shall explain shortly) is denoted by a transition from a source state to a target state. Each transition is associated with a non-empty set of labels, where each label represents an atomic use case step. The execution order of use case steps is modeled using transition sequences, where the target state of a transition serves as the source state of the following transition. For a given transition, if the associated label set contains more than one label, then no specific execution order exists between the corresponding use case steps. I.e., a transition is triggered when all associated primitive steps are executed; the execution order, however, is arbitrary. The mapping from a DRSG-style use case model to a UC-LTS is defined in two steps: 1. Generation: For each use case of the DSRG use case model, the main success scenario and extensions are mapped to UC-LTSs. Each such UC-LTS is a partial description of the respective use case, i.e., it represents either the main success scenario or an extension. Throughout generation, a global equivalence relation ( ) is successively populated, which identifies equivalent states among the various UC-LTSs.

Merging:

The various UC-LTSs are merged into a single UC-LTS. The merge is performed on the basis of the global equivalence relation ( ). Definitions of the mappings require: (1) An input use case model in canonical form, (2) proper initialization of a global environment (

) and (3) the global equivalence relation ( ). In the following, details of each requirement will be given.

Definition 4 (Canonical form of a use case model). A use case model is in a canonical form, if and only if:

i. it is well formed, ii. each use case extension is associated with exactly one step, and iii. each use case (except for the root use case) is invoked by exactly one step.

While the "Order Product" use case (Fig. 6) is already in canonical form, an arbitrary well-formed use case model can be transformed into canonical form in a straight-forward manner. In order to satisfy condition (ii), instead of the original extension, use case steps are associated with distinct copies of the respective extensions. If steps of the original extension are referenced by means of a step, the respective reference is to be updated accordingly. Similarly, in order to satisfy condition (iii) instead of the original sub-use case , each step is associated with a distinct copy ( ) of . For example, if, throughout the use case model, use case is included three times by steps , and , then we create three copies of ( , , ) and modify the inclusion steps as follows:

, and . We also require the proper initialization of a global environment, . As defined by Fig. 8 (left hand side), has three fields, named , and , where: is a function that maps use case names to which, according to Fig. 8 (right hand side), defines for each use case the initial state ( ) of the UC-LTS representing the main success scenario and the set of states representing the successful ( ) and unsuccessful ( ) termination of the use case. and are bijective functions that map a given step id or extension id to the initial state of the UC-LTS representing the use case step and use case extension, respectively. Recall that according to the well-formedness conditions of a DSRG-style use case model, step and extension ids are unique within any given use case model.

is an equivalence relation (reflexive, symmetric, and transitive) defined over , the set of all states. During merging, all equivalent states will be merged to a single state denoting its respective equivalence class. In order to satisfy the reflexivity requirement, is initialized as follows: .

Generation

Given a use case model in canonical form, the generation of a set of UC-LTSs is performed in a bottom-up manner. We start with the mapping of an individual use case step. As defined in the abstract use case syntax (Fig. 5), there are 7 kinds of use case steps. Each step kind has its own specific mapping to a UC-LTS.

As depicted in Fig. 9, depending on the step type (denoted by t) atomic steps are mapped into different UC-LTSs. The rationale behind each case is as follows: Each internal (a) use case step has different outcomes, among which one is captured in the main success scenario and the remaining outcomes are captured by the corresponding extensions. Hence, the resulting UC-LTS consists of transitions; one transition for the main success scenario and transitions for each defined extension. The former results in a final state, which will be used for the sequential composition of use case steps. The latter result in a set of non-final states. During merging, these states will be joined with the initial states of the UC-LTSs representing the various extensions. This is defined by adding the respective state pairs to the global equivalence relation (∼).

In contrast to internal use case steps, which are performed by the system and are hidden from the user, steps of type interaction are performed by the user. As such, they do not have an alternative outcome per se, but may be associated (by virtue of one or more extensions) with alternative steps which are performed instead of the actual step. As a result, the corresponding UC-LTS consists of only one transition (from to ), representing the use case step (b). Alternative steps are captured in the UC-LTSs representing the corresponding extensions. During "Merging" the initial states of each UC-LTS representing an extension are identified with . This is defined by updating ∼ accordingly. Steps of type application are performed by the system and have an externally visible effect to the user. They are performed in response to an internal or interaction step. As a consequence, they are not associated with any extension, and the corresponding UC-LTS consists of only one transition (c).

The mapping of the remaining step kinds is briefly outlined next. The full details can be found in [START_REF] Sinnig | Use Case and Task Models: Formal Unification and Integrated Development Methodology[END_REF]. A Choice step is mapped to a UC-LTS which results from merging the initial states of the UC-LTSs representing the Having defined the mapping for individual UC steps, we continue with defining the mapping of step sequences to UC-LTS. The mapping of a list of use case steps corresponds to the binary sequential composition ( ) of the UC-LTSs of the individual steps. As schematically depicted in Fig. 10, the sequential composition consists of unifying the final states of the first operand and the initial state of the second operand.

Definition 5 (Mapping a step sequence to a UC-LTS). Given

, a non-empty step sequence of steps, we define the mapping of step sequences to a UC-LTS as follows:

. An entire use case is mapped into a set of UC-LTSs. The resulting set contains one UC-LTS for the main success scenario and one UC-LTS for each defined extension.

Definition 6 (Mapping a use case to a set of UC-LTSs). Let be a use case with e

. We then obtain the corresponding set of UC-LTSs as follows:

. Finally, we define the mapping of a set of use cases to a set of UC-LTSs as the union of the sets of UC-LTSs representing the various use cases.

Definition 7 (Mapping a set of use cases to a set of UC-LTSs). Let be a set of use cases. We then obtain the corresponding set of UC-LTSs as follows:

.

For illustrative purposes, Fig. 11 portrays the set of UC-LTSs of the "Order Product" use case model. As depicted, the set consists of five UC-LTSs; one for the main success scenario of "Order Product" and one for each of the four extensions. States that belong to the same equivalence class (by means of ∼) are circled by a dashed line. During "Merging", these states will be combined to a single state to obtain a single consolidated UC-LTS.

Merging

A use case model is mapped to UC-LTS by merging the UC-LTSs representing the various entailed use cases. The merge is performed on basis of the global equivalence relation (~).

Definition 8 (Mapping a use case model to UC-LTS). Let be a well-formed use case model in canonical form, be the range of , and be the result of with and . The mapping to UC-LTS is then defined as follows:

with , , ,

, where is the generalized canonical projection map defined as , and .

The set of states of the resulting UC-LTS is the set of equivalence classes in ( ) with respect to . The initial and final states are the equivalence-class counterparts of the initial and final states of the root use case . Rather than on states, the transition function δ is defined on equivalence classes of states. For a given equivalence class and a set of labels, it denotes the set of equivalence classes of all states that are reachable from any member of having accepted . Fig. 12 portrays the UC-LTS obtained by merging the various UC-LTSs given in Fig. 11. The resulting UC-LTS has five final states:

denoting the successful outcome of the use case (i.e., the customer succeeded to order the product), and denoting the case where the user cancels the use case, denoting the case where the product is not available, and denoting case where the payment was not authorized. Notice that the resulting UC-LTS has fewer states than the accumulated number of states of the involved UC-LTSs. This is because, during merging, two or more states are combined into a single state, representing the respective equivalence class.

{spCA} {diSR} {slPQ} {vaPQ} {diPS} {prPI} { p a D B } {vaPA} {inCO} [q 0 ] [q 1 ] [q 2 ] [q 3 ] [q 11 ] [q 4 ] [q 5 ] [q 6 ] [q 8 ] [q 7 ] [q 9 ] [q 12 ] [q 10 ] [q 16 ] {inIQ} {inCA} {inPF} {vaPQ} { i n C A } [ q 2 0 ] { p a C C } {vaPA} {vaPA} {vaPA} [q 14 ] [q 18 ]
Fig. 12. UC-LTS representing "Order Product" use case

Generic task expressions

In this section we define the intermediate semantic domain for task models called Generic Task Expressions (GTE). We also specify how well-formed ECTT task models are mapped into a corresponding GTE.

Definition 9 (Generic task expression). Let and be generic task expressions and be an atomic task, then the set of generic task expression

is the smallest set closed under following rules: (1) is a generic task expression and (2) , , , , , , are also generic task expressions.

In contrast to an ECTT task model (Definition 2), a generic task expression abstracts away from high-level task names (i.e. task definitions). Instead of using task definitions, the behavior of the task model is captured in a single generic task expression. While high-level task names are important at the modeling stage to foster the comprehension of the task model, they are irrelevant for capturing behavioral information. Compared to an ECTT task expression, a generic task expression may not contain high-level operators (e.g., order independency, disabling, or suspend / resume). These operators are important, as syntactic sugar, at the modeling stage to obtain a concise and comprehensible task model. However, they do not enrich the expressiveness of an ECTT task expression and can be rewriting using low-level operators. In what follows we present a mapping which transforms each ECTT task expression into a corresponding generic task expression.

Definition 10 (Mapping an ECTT task expression to a generic task expression).

Let be ECTT task expressions, be a task name and be a finite map of ECTT task definitions. We then define the mapping to generic task expressions, relative to a given task definition map , as follows:

While most expressions (i.e., , , , , , ) are directly mapped to a corresponding GTE expression, ECTT task expressions of form (disabling) or (suspend / resume) are first rewritten into an ECTT task expressions without and , before the semantic function is applied. For this purpose the auxiliary functions deep optionalization ( ) and interleaved insertion ( ) have been defined. The former is a function that defines every sub-task of its target task expression as optional. However, if the sub-tasks are executed, they have to be executed in their predefined order. The latter is a function that "injects" the task specified by its second operand at any possible position in between the (sub) tasks of the first operand. Formal definitions of and together with additional explanations why disabling and suspend / resume can be rewritten using lower-level operators, are given in Appendix A. The GTE of the "Order Product" task model is given below.

Common formal semantics

In this section we define the second-level mappings (Fig. 4) to the semantic domain of Sets of Partial Order Sets (set of posets). We start by providing necessary definitions. Then, we present a procedure that, given a UC-LTS, generates the corresponding set of posets. We also define a semantic function that maps a generic task expression (GTE) to a corresponding set of posets.

Definitions

Fundamental to our approach is a differentiation between events and event names as well as a formalization of the set operation disjoint union (+).

Mathematical Definitions and Preliminaries

Definition 11 (Events). Let represent the set of all possible event names. We then define an event as a pair consisting of an event name and an index . Correspondingly, the set of all events is defined as: For all we define the obvious projection function and its generalization, applied to sets of events being applied to all elements of the set. We reserve the name ; its semantics will be given later.

In what follows, event names may be used to represent events with index ; i.e., as needed, we assume the implicit conversion from

We will use the symbol , possibly decorated with primes (

) and/or subscripts ( ), to represent a subset of . Next we define the set operation disjoint union. It is used as an auxiliary function for the definition of composition operators for partially ordered sets, which are needed for the semantic mapping.

Definition 12 (Disjoint union). Using standard notation, we represent the disjoint union ( ) of two event sets as:

, where for with

Our definition of the disjoint union is similar to what has been proposed by Blyth [START_REF] Blyth | Set theory and abstract algebra[END_REF]. In both cases an index set is used to distinguish between events that have the same name. In contrast to Blyth, however, we use a natural number instead of an n-ary tuple over . We generalize and to binary relations over ; i.e., given we define and .

Semantic Domain: Sets of Posets

The building blocks for the semantic domain presented in this section are partially ordered sets (posets).

Definition 13 (Poset over events).

A partially ordered set (poset) over events is a tuple , where is a set of events and is a partial order relation (reflexive, anti-symmetric, transitive) defined over . This relation specifies the causal order of events.

In order to be able to compose posets we define the operations sequential and parallel composition.

Definition 14 (Sequential and parallel composition of posets).

Let and be posets. We define the sequential composition ( ) and parallel composition ( ) as follows.

Intuitively, if the event set of does not contain , then the sequential composition places all events of strictly after all the events of . Otherwise, simplifies to regardless of . In contrast to the sequential composition, the parallel composition does not make a case distinction between posets that contain or do not contain an event named

. The insertion and the removal of STOP to/from a poset are the so-called closing and opening operations and are defined as follows:

Definition 15 (Closing and opening of a poset). Let be a poset. We define the closing operation and the opening operation .

In [START_REF] Sinnig | Use Case and Task Models: Formal Unification and Integrated Development Methodology[END_REF], we have formally proven that posets are closed under the operations sequential composition, parallel composition, opening and closing. Also fundamental to our model is the notion of a trace. In general, a trace of a partial order set corresponds to a totally ordered event-name sequence such that the corresponding sequence of events is a linear extension of the partial order. It is important to note that events with event name are not part of a trace. Note that holds true, if either or and are unrelated (by means of ).

Definition 16 (Set of all traces). Let be a poset. We define the function which yields the set of all traces of as follows:

The common semantic domain for use case and task models is sets of partially order sets and is defined as follows:

Definition 17 (Set of partial order sets). A set of partial order sets is a possibly infinite collection of posets . Sets of posets can be composed by the operators defined in Definition 18. In contrast to the operators defined on posets we additionally introduce alternative composition and closure. Both are needed for the semantic mappings defined in the next sections. Note that similar to the Kleene star operation for regular expressions [START_REF] Hopcroft | Introduction to automata theory, languages, and computation[END_REF], closure returns the set of posets that are formed by computing the union of all possible (repeated) sequential compositions of a given set of posets.

Definition 18 (Operators for sets of posets). Let and be sets of posets. We define the sequential composition ( ), parallel composition ( ), alternative composition ( ), closing, opening, and closure ( ) as follows:

where is defined as Finally, we define the set of all traces for a set of posets. It forms the essential basis for establishing refinement relations (Section 7) between use case and task models.

Definition 19 (Set of all traces of a set of posets).

The set of all traces of a set of posets is defined as:

Based on the definition of the set of all traces, we can derive certain trace properties for each defined set of poset operation. These are given in Appendix B.

Semantic rules

In this section we define the semantic mappings from the intermediate semantic domains (namely UC-LTS and GTE) to sets of posets.

Mapping UC-LTSs to sets of posets

Definition 20 (Mapping UC-LTS to a set of posets). Let be a UC-LTS. We then define the mapping to a set of posets as follows:

. For this purpose we have devised the algorithm . Fig. 13 gives the corresponding pseudo code.

Without loss of generality, the algorithm assumes that there are no outgoing transitions from any of the final states in the input UC-LTS. This is a valid assumption since, according to the well-formedness rules for DSRG-style use cases (Section 4.1), Failure and Success steps are always at the end of any step sequence and cannot have any extensions. We also note that the main idea for the algorithm stems from the well-known algorithm that transforms a deterministic finite automaton into an equivalent regular expression [START_REF] Hopcroft | Introduction to automata theory, languages, and computation[END_REF]. Instead of stepwise composing regular expressions, we compose sets of posets.

The procedure starts (1) with the creation of an initial generalized UC-LTS internally represented by a twodimensional array ("SPO"). The array is populated with all transitions of the given UC-LTS specification. Indexed by a source and a target state, an array cell contains a set of posets constructed from the label(s) associated to the representative transition. If the label is a singleton set, then the corresponding set of posets contains a single poset containing the respective event. If the label consists of multiple events, indicating the concurrent or unordered execution of use case steps, the set of posets will contain a poset which consists of several elements. Those elements, however, are not causally related. We note that the idea of a generalized UC-LTS is similar to the concept of a generalized finite state machine [START_REF] Hopcroft | Introduction to automata theory, languages, and computation[END_REF]. Instead of labeling the transitions with regular expressions, transitions are labeled with sets of posets.

The core part of the algorithm consists of two nested loops. The outer loop (2) iterates through all states of the generalized UC-LTS (except for the initial and the final states) whereas the inner loop (3) iterates through all pairs of incoming and outgoing transitions for a given state. For each found pair , we perform the following (4): Compute the alternative composition of:

SPO[

] The set of posets associated with the transition from to . If such a transition does not exist we take the set of posets to be . Next (5) we add a new transition from the source state of the incoming transition to the target state of the outgoing transition. Note that the corresponding cell in has already been populated with the result of (4). Back in the outer loop, we eliminate (6) the currently visited state from the generalized UC-LTS and proceed with the next state. Once the generalized UC-LTS consists of only the initial state and the final states we exit the outer loop and perform the following two computations, in order to obtain the final result. First (7) we perform an alternative composition of the sets of posets of all the transitions from the initial state to a final state. Second, if the initial state additionally contains a self loop (8) then we sequentially compose the result of the closure composition of the set of posets denoted by that self loop and the result of the before-mentioned alternative composition.

If we apply the algorithm to the "Order Product" UC-LTS we obtain the set of posets depicted in Fig. 14. For the sake of conciseness events are represented only by their name, while the index has been omitted. This simplification was possible because none of the entailed posets contains two or more events sharing the same name. The various parts of the resulting set of posets are interpreted as follows: Having indicated the desire to order a product, the primary actor searches for a product and as a result (1, 3) elects to quit the system, (2) the selected product is not available in the desired quantity or he/she decides to checkout and pay. In the latter case, the debit or credit card payment is either authorized (4b, 5b) or rejected (4a, 5a).

(

Mapping GTM to sets of posets

This section specifies how a generic task expression is mapped into a corresponding set of posets. As given in Definition 21, is defined in the common denotational style. An atomic generic task expression (denoted by ) is mapped to a set containing the corresponding singleton poset. Composite task expressions are represented by sets of posets, which are composed using the operators, defined in the Section 6.1.2.

Definition 21 (Set of posets semantics of generic task expressions).

Let be generic task expressions and be an atomic task. We then define the mapping to sets of posets as follows:

In what follows we illustrate the semantic rules by mapping the "Order Product" generic task expression to a set of posets.

According to Definition 21 the application of to the entire generic task expression is successively broken down into the application of to sub-expressions and the corresponding set of posets operations. Fig. 15 depicts the resulting set of posets expression, using the same shorthand notation as introduced in the previous section. It allows a subset of the traces allowed by the set of posets of the corresponding use case. Upon initiation, the user searches for a product until he/she either (1, 3) elects to quit, (2) the selected item is out of stock or the product is available and the attempt to pay by credit card is either rejected (4a) or authorized (4b). The option to pay by debit card (as specified in the use case) is not available. This may be due to restrictions of the supported user interface, which may not be equipped with a debit card reader.

(1)

(2) (3) (4a) (4b) (5a) (5b)

Refinement between use case and task models

In the spirit of modern software development, use case and task models are best developed iteratively through a series of refinement steps. For each refinement step it is important to verify that the resulting model is a valid refinement of its source specification. Having defined a common semantics for use case and task models we are now able to formalize refinement between these two kinds of artifact.

In Section 2.3, we noted that use cases are used to capture functional requirements, whereas task models are used to capture UI interaction requirements and design details. While use case models are exclusively used at the requirements stage, task models may be used at the requirements and at the design stage. When the task model is used as a requirements artifact, this detailed specification of the UI is considered part of the contract between stakeholders about the envisioned interactive application, whereas when exclusively used as a design document it is not part of the requirements contract. Based on this observations, it becomes evident that two notions of refinement are necessary depending on the purpose of the refining model; i.e., whether the refining model is a requirements artifact or a design artifact. In the following, both cases are discussed in detail.

At the requirements stage, a use case or task model may be refined by a more detailed artifact. In such a case, the refinement is deemed valid if the refining model does not allow more scenarios than its base model. The refining model, however, may further restrict the set of allowed scenarios. In practice, such a restriction may be the result of filtering the requirements in order to establish a base line. As a consequence, requirements with a low priority or that are considered too risky may be dropped in the refining model. In our semantics, the restriction of scenarios can be expressed in terms of trace inclusion.

Definition 22 (Refinement at requirements stage). For

, let be (well formed) DSRG-style use case models, be (well formed) requirements ECTT task models and and be the respective sets of posets representations. We then define refinement between use case and task models as follows:

The artifacts gathered during requirements specification are part of the contract between stakeholders about the envisioned application. When moving from a requirements model to a design model, it is important to ensure that the refining model truly implements the requirements. As a consequence, the refining model may only add information in terms of structural refinement (refinement of previously atomic use case steps or tasks), but must not restrict or extend the number of possible scenarios. For example, when moving from a use case model to a design-level task model we have to ensure that the task model adopts the entirety of the functional requirements specified in the use case model and integrates them into the UI design. Similarly, if a requirements task model is refined by a designlevel task model we require that each task of the requirements model be present in the design-level task model and that the execution orders of all "implemented" requirements-level tasks be preserved. In our semantics, scenario equivalence is expressed in terms of trace equivalence: Definition 23 (Refinement at design stage). Let be a (well formed) DSRG-style use case model, be a (well formed) requirements ECTT task model, , be (well formed) design ECTT task models and

(1)

(2)

(3) We then define refinement between use case and task model as follows:

(4a) (4b)
A precondition for the application of the definition is that the involved sets of posets are defined over the same event-name alphabet. In what follows, we discuss two techniques to resolve alphabet conflicts, called refinement mapping and event hiding. 1. A mapping from events of the base specification to events of the refining specification is referred to as refinement mapping. We distinguish between two main types:

-Choice Mapping: An atomic element of the base specification may be refined by a set of atomic elements which are alternatively composed by either the ECTT choice ( ) operator or a Choice use case step. -Many-To-One mapping: An atomic element of the base specification may be refined into a set of subelements. In contrast to choice refinement, the execution of the entirety of sub-elements resembles the execution of the base element. 2. The second technique that can be used to unify the event-name alphabet of two specifications is event hiding. As already mentioned, use case models are used to document functional requirements while task models specify UI requirements and design details. As such, they abstract from internal system actions, which are irrelevant for UI design. Hence, in order to compare use case and task models for refinement, we have to abstract from all internal system steps in the use case model. This is achieved by removing all events that represent internal events in the set of posets representing the use case model. In order to illustrate the application of the introduced refinement definitions, let us recall the "Order Product" use case and the "Order Product" task model. In order to formally verify that the task model is a valid requirements-level refinement of the use case, we need to prove that the set of all traces of the set of posets representing the task model is a subset of the set of all traces of the set of posets representing the use case. After hiding, all events representing internal system steps (displayed in gray in Fig. 14) in the set of posets representing the use case, we obtain the following trace set.

The set of posets representing the task model, after the refinement mapping, is given in Fig. 16. In particular we applied the many-to-one mapping from tasks "Select Criteria" (slCR) and "Submit Criteria" (sbCR) to use case step "Specify Product Category" (spCA) and the many-to-one mapping from tasks "Select Product" (slPD), "Select Quantity" (slQT) and "Submit" (sbPS) to use case step "Specify Product and Quantity" (slPQ). We then obtain the following set of traces:

Clearly

, and hence we conclude that at the requirements stage the "Order Product" task model is a valid refinement of the "Order Product" use case. Recall that each task model is geared to a particular user interface and as such is confined by its limitations. In this case, the user interface may not be equipped with a debit card reader and hence does not offer the user this payment option (even though from a pure functionality point of view a debit card payment could have been processed by the system (as specified by the use case). We conclude this section by noting that at the design stage, the "Order Product" task model is not a valid refinement of the use case. With the requirements contract (as specified by the use case) is not fulfilled by the design which supports only a subset of the offered functionality.

Related work

In this paper, we have defined a common formal semantics for use cases and task models. Both are used to model behavioral aspects of the system. The formalization of behavioral specifications has been attempted by various researchers. Börger et al. [START_REF] Börger | Modeling the Dynamics of UML[END_REF][START_REF] Börger | On formalizing UML state machines using ASMs[END_REF] propose a formal framework for UML statecharts based on an multiagent ASM formalism. The behavior of the statechart is controlled by a set of ASM agents, which execute actions depending on the currently active state(s). The actions are formalized by a set of ASM rules. Reggio et al. [START_REF] Reggio | Analysing UML Active Classes and Associated State Machines -A Lightweight Formal Approach[END_REF] define an operational semantics for UML statecharts based on algebraic specifications. Pursuing the goal statechart verification Kwon [START_REF] Kwon | Rewrite Rules and Operational Semantics for Model Checking UML Statecharts[END_REF] proposes a formalizations in PROMELA/SPIN and SMV, respectively. Activity diagrams are used to describe the flow of behavior within a system. Similarly to use cases, activity diagrams are equipped with constructs to express sequences, choices and parallelism. Several attempts have been made to define formal semantics for activity diagrams. E.g., the research by Börger et al. [START_REF] Börger | An ASM Semantics for UML Activity Diagrams[END_REF] defines a semantics by translating activity diagrams to abstract state machines. Bolton and Davies [START_REF] Bolton | Activity graphs and processes[END_REF] provide a formalization of activity diagrams using CSP.

UML interaction diagrams (e.g., collaboration/communication and sequence diagrams) are used to model system functionality and the control flow within a system. Engels et al. [START_REF] Engels | UML Collaboration Diagrams and Their Transformation to Java[END_REF] define a formal semantics for UML collaboration diagrams based on graph transformation rules. Storrle [START_REF] Storrle | Semantics of interactions in UML 2.0[END_REF] and Haugen et al. [START_REF] Haugen | STAIRS towards formal design with sequence diagrams[END_REF] define trace-based semantics for sequence diagrams. The semantics proposed by Grosu and Smolka [START_REF] Grosu | Safety-liveness semantics for UML 2.0 sequence diagrams[END_REF] employs safety and liveness properties to formally distinguish between valid and invalid behaviors. For the closely related message sequence charts (MSCs), Zheng [START_REF] Zheng | Validation and Refinement of Timed MSC Specifications[END_REF], proposes a non-interleaving semantics based on timed labeled partial order sets (lposets). Partial order semantics for (regular, un-timed) MSCs have been proposed by Alur et al. [START_REF] Alur | An Analyzer for Message Sequence Charts[END_REF] and Katoen and Lambert [START_REF] Katoen | Pomsets for Message Sequence Charts[END_REF]. Alur et. al. propose a semantics for a subset of MSCs which only allow message events as possible MSC events types. In contrast, the semantics of Katoen and Lambert is more complete. They map MSCs to a set of partial order multi-sets (pomsets).

The definition of formal semantics for use case models has been attempted by various researchers. Fröhlich and Link [START_REF] Fröhlich | Automated Test Case Generation from Dynamic Models[END_REF] present a transformation algorithm that derives a UML state chart model from a given set of textual use cases. Similar to our approach, a distinction is made between use case steps that are performed by the system and steps performed by the primary actor. The former are represented by actions, whereas the latter are modeled as events, causing state transitions. Övergaard and Palmkvist [ÖvP98] propose an ODAL [START_REF] Milner | A Calculus of Mobile Processes[END_REF] formalization of use cases and their relationships (uses and extends). It is assumed that use cases are pre-formalized in a proprietary methods / operations notation. The formalizations of uses roughly corresponds to our include step, the formalizations of extends corresponds to our notion of a use case extension. Stevens [START_REF] Stevens | On Use Cases and Their Relationships in the Unified Modelling Language[END_REF] discusses how use cases and their relationships may be formalized using labeled transition systems (LTS). Use cases are interpreted as processes, which are internally represented by LTSs. Relationships between use cases are modeled by relating the corresponding LTSs.

Rui et al. suggest a process algebraic semantics for use case models, with the overall goal of formalizing use case refactorings [START_REF] Rui | Refactoring Use Case Models[END_REF]. In their approach, scenarios are represented as basic MSCs by partially adapting the ITU MSC semantics [START_REF]Recommendation Z.120-Message Sequence Charts[END_REF]. Fernandes et al. [START_REF] Fernandes | Designing Tool Support for Translating Use Cases and UML 2.0 Sequence Diagrams into a Coloured Petri Net[END_REF] present an approach to translate use cases into Colored Petri net models. It is assumed that each use case is represented by a UML sequence diagram. The translation is performed in a top down manner: First, the use case model is mapped into a global Petri net which contains placeholders for each individual use case. Then, each placeholder is replaced by a sub-Petri net capturing the various scenarios of the use case. Probably the most comprehensive approach has been defined by Somé [START_REF] Somé | Petri Nets Based Formalization of Textual Use Cases[END_REF]. He proposes execution semantics for use cases by defining a set of mapping rules from well-formed use cases to basic Petri nets. A use case is deemed well-formed if it syntactically corresponds to a predefined meta-model and satisfies a set of consistency and well-formedness rules. The mapping to Petri nets is defined over the various components of the use case (e.g. use case step, extension, control flow construct, etc.).

Paternò and Santoro define formal semantics for a subset of the task modeling notation CTT (ConcurTaskTrees) based on LOTOS [START_REF] Paternò | Support for Reasoning about Interactive Systems through Human-Computer Interaction Designers" Representations[END_REF]. Tasks and subtasks from the CTT task model are mapped in a one-to-one fashion to LOTOS process specifications. Temporal relations between tasks are mapped to LOTOS process composition operators. Ait-Ameur et al. [START_REF] Ait-Ameur | Encoding a process algebra using the Event B Method. Application to the validation of user interfaces[END_REF] specify a mapping from CTT to Event-B [START_REF] Abrial | Extending B without changing it (for developing distributed systems)[END_REF]. Main motivation behind their work is the formal validation of whether a concrete implementation of a UI is consistent with its design specification. Klug & Kangasharju [KlK05] propose a formalization for task models where a task is not regarded as an atomic entity (like in CTT) but has a complex lifecycle, modeled by a so-called task-state machine. In the approach by van den Bergh and Coninx [START_REF] Van Den Bergh | From Task to Dialog Model in the UML[END_REF] entire task expressions are translated into state charts, including high-level tasks. Bomsdorf [START_REF] Bomsdorf | The WebTaskModel Approach to Web Process Modelling[END_REF] defines an elaborated life cycle for tasks. The work is focused on the development of web applications and considers external events related to web technology (e.g. session timeouts and user aborts).

The approach presented in this paper is inspired by the approach by Zheng [START_REF] Zheng | Validation and Refinement of Timed MSC Specifications[END_REF], who proposed a noninterleaving semantics for timed MSC 2000 [START_REF]Recommendation Z.120-Message Sequence Charts[END_REF] based on timed labeled partial order sets (lposets). Compared to the poset definition introduced in this paper, a timed lposet additionally contains labeling and timing functions. The labels serve as an indicator for the corresponding event type. Possible event types are: message input, message output, internal action, start timer, stop timer and timeout. Furthermore Zheng defines two functions which attach timing constraints to events in order to specify the time range within which an event could occur and define delays between two events. The semantic mapping is performed by associating an MSC with a set of timed lposets which capture the possible execution scenarios of the MSC.

According to our integrated development methodology, use case and task models are successively refined into more detailed specifications. Refinement relations for event-based specifications have been investigated for decades and definitions have been proposed for various models [Den87; IYK90; But92; BuB06; SiC07; BSB02]. Khendek et. al [START_REF] Khendek | Stepwise Design with Message Sequence Charts[END_REF] propose a refinement relation for basic MSCs. It ensures that a scenario, described in the source MSC specification, is also available in the refined specification. In much the same vein, a scenario that is forbidden in the source specification must never occur (or be derivable) in the refined specification [START_REF] Li | Translating Use Cases to Sequence Diagrams[END_REF]. In other words, the behavior of the source MSC must be preserved in the target MSC. Events defined in the source MSC should also occur in the target MSC, and the relative order of these events needs to be preserved. The order of newly introduced events is not restricted. In our work, we used a similar approach by defining refinement through trace inclusion and trace equivalence. While the former is applied at the requirements level, the latter is used at the design-level to express the condition that the design shall faithfully fulfill the contract statement as laid out by the requirements.

Conclusion

The lack of a common formal semantics for use case and task models hinders the effective verification of wellformedness properties, leaves little room for tool support, and hampers the definition of an integrated development methodology. As a consequence, ambiguities and inconsistencies may go undetected, and are likely to propagate in subsequent development stages, resulting in higher costs to repair them. To address these shortcomings, we have defined a common semantics for use case and task models. The formal framework defines a two-step mapping from use case or task model notations to the common semantic domain of sets of posets. Our two-step mapping results in a semantic framework that can be more easily reused and extended. The intermediate semantic domains have been carefully chosen by taking into consideration the intrinsic characteristics of task models and use cases. In particular, we defined a Use Case Labeled Transition System (UC-LTS) as an intermediate semantic domain for use cases. It was demonstrated that UC-LTSs allow for a natural representation of the order in which actions are to be performed. In the case of task models, we defined generic task expressions (GTE) as an intermediate semantic domain. Similar to task models, a generic task expression is hierarchically composed of sub-task expressions using a set of standard operators. Hence the mapping from a concrete task model to GTE remains straightforward and intuitive.

As a concrete example, we demonstrated how our framework can be used to define a common semantics for DSRG-style use case models and ECTT task models. Both have been defined as improvements to their respective state-of-the-art counterparts, Cockburn-style use case models and CTT. Each improvement has been carefully selected to ensure that the intent and nature of each model is preserved. In the case of DSRG-style use case models, we introduced step kinds and step types as distinguishing factors for use case steps. In case of ECTT, as our main contribution, we defined two novel temporal operators: Stop and Resume, that allow the developer to model error and failure cases, and provide a mechanism to catch errors and prevent their propagation. Also, in order to overcome the predominant, yet obsolete, monolithic task-tree structure, we defined ECTT in a modular fashion allowing task models to be developed in a true top-down manner while taking advantage of encapsulation.

The common semantics presented here formally relates use cases and task models and allows for cross-artifact refinement checks. We have defined two refinement relations based on trace inclusion and trace equivalence. The former is used at the requirements level, whereas the latter is used when moving from the requirements to the design level. The presented refinement definitions are one possible utilization of the common formal semantics for use cases and task models. Depending on the usage context, more elaborate notions of refinement (other than trace inclusion or equivalence) can be defined as well. A set of prototypical tools were developed as proofs of concept for the syntactic and semantic definitions. We developed an Isabelle/HOL theory which allows for validating syntactic and wellformedness properties of DSRG-style use cases. We also developed the tool Use Case -Task Model Verifier, which partly implements the semantic mappings to the intermediate semantic domains.

Future avenues deal with extension of the proposed semantics to capture state information. State information is often employed in use case or task models to express and evaluate conditions. For example, the precondition of a use case denotes the set of states in which the use case is to be executed. In addition, every use case extension is triggered by a condition that must hold before the steps defined in the extension are executed. To be able to evaluate conditions, the semantic model must provide a means to capture the system state and should be able to map state conditions to the occurrence of events.

Operation Trace Property

, where denotes the sequential composition of two event name sequences.

, where is defined as [START_REF] Roscoe | The Theory and Practice of Concurrency[END_REF]:

, where is defined as:

The corresponding proof for the proposition is given in [START_REF] Sinnig | Use Case and Task Models: Formal Unification and Integrated Development Methodology[END_REF].

Fig. 3 .

 3 Fig. 3. "Order Product" task model in ECTT

Fig. 4 .

 4 Fig. 4. Two-step semantic mapping

Fig. 5 .

 5 Fig. 5. DSRG-style use case syntax formalized in Isabelle.

Fig. 6 .

 6 Fig. 6. Formalized syntax of "Order Product" use case

Fig. 8 .Fig. 9 .Fig. 10 .

 8910 Fig. 8. Definition of global environment and UCStateInfo

Fig. 11 .

 11 Fig. 11. UC-LTSs of the "Order Product" use case

  and the result of the sequential composition of the following three sets of posets: SPO Set of posets associated to the incoming transition SPO The closure of the set of posets associated to a possible self-transition defined over the currently visited state. If such a self transition does not exist then the closure composition yields . SPO Set of posets associated to the outgoing transition.

Fig. 13 .

 13 Fig. 13. LTS_to_SPO algorithm transforming a UC-LTS to a set of posets

Fig. 14 .

 14 Fig. 14. Set of posets representation of "Order Product" use case

Fig. 15 .

 15 Fig. 15. Set of posets representation of "Order Product" task model

Fig. 16 .

 16 Fig. 16. Set of posets representation of "Order Product" task model after refinement mapping

Extensions 3a. Customer is not satisfied with the search results

  Customer elects to pay by debit card and submits account information. (paDB) 7. System interacts with the Payment authorization system to carry out the payment. (vaPA) 8. System informs Customer that order is confirmed. (inCO) 9. Use case ends successfully

	Use case: Order Product
	Properties
	Goal: Customer places an order for a specific product.
	Primary Actor: Customer
	Goal-Level: User-goal
	Precondition: Customer is logged into the system
	Main Success Scenario
	1. Customer specifies the desired product category. (spCA)
	2. System displays search results that match the Customer"s supplied criteria. (diSR)
	3. Customer selects a product and identifies the desired quantity. (slPQ)
	4. System validates that the product is available in the requested quantity. (vaPQ)
	5. System displays the purchase summary. (diPS)
	6. Customer chooses one of the following
	7A.1. Customer elects to pay by credit card and submits account information. (paCC)
	OR
	7B.1

: 3a1. Customer indicates to cancel the use case. (inCA) 3a2. Use case unsuccessfully. 4a. The desired product is not available in sufficient quantities: 4a1. System informs Customer that product unavailable in desired quantity. (inIQ) 4a2. Use case ends unsuccessfully. 6a. Customer decides to cancel the use case: 6a1. Customer indicates to cancel the use case. (inCA) 6a2. Use case ends unsuccessfully. 7a. The payment was not authorized: 7a1. System informs Customer that payment was not authorized. (inPF) 7a2. Use case ends unsuccessfully. Fig 2. "Order Product" use case pressiveness they share the following common tenet: Tasks are hierarchically decomposed into sub-tasks until an atomic level has been reached. In what follows we describe in detail the task-modeling notation Extended CTT (ECTT). ECTT was first introduced in [SWF07] and extends ConcurTaskTrees (CTT) in two dimensions:

Table 1 .

 1 Temporal operators of ECTT Either t 1 or t 2 is executed. The execution of one task disables the other one.

	Operator	Syntax	Interpretation
	Enabling	t 1 >> t 2	Upon successful termination of t 1 , t 2 becomes enabled.
	Choice	t 1 [] t 2
	Order	t 1 t 2	Execution of t 1 and t 2 in any order.
	Independence
	Concurrency	t 1 t 2	Interleaved execution of t 1 and t 2 and their subtasks.
	Disabling	t 1 [> t 2	t 1 becomes deactivated as soon as the first task of t 2 is performed.
	Suspend-	t 1 |> t 2	At any time the execution of t 1 may be interrupted by t 2 . After t 2 has finished its execution t 1
	resume		resumes.
	Iteration	t *	t may be executed repetitively (0 or many times).
	Optional Tasks [t]	t may be executed or not.
	Stop	stop(t)	t cannot enable any tasks.
	Resume	resume(t)	Counteracts the effect of stop.

Table 2 .

 2 Trace properties for sets of posets operations

Instead of a "list" it would be semantically more accurate to use a "set". However Isabelle/HOL does not support using "sets" within recursively defined datatypes.

Acknowledgments

This work has been partially supported by the Natural Sciences and Engineering Research Council (NSERC) of Canada.

A. Rewriting of disabling and suspend / resume

In this section we give formal definitions of the auxiliary operators deep optionalization ( ) and interleaved insertion ( ). Both are needed in Definition 10 for the rewriting of the ECTT operators disabling und suspend/resume, respectively. Intuitively the meaning of the disabling operator is defined as follows: Both tasks specified by its operands are enabled concurrently. As soon as the first (sub-) task specified by the second operand is executed, the task specified by the first operand becomes disabled. If the execution of the task(s) specified by the first operand is completed (without interruption) the task(s) specified by the second operand are subsequently executed. In other words, none of the (sub-) tasks of the first operand must necessarily be executed, whereas the execution of the tasks of the second operand is mandatory. Hence, an ECTT task expression including the disabling operator can be rewritten as the optional execution of the deep optionalization ( ) of all tasks involved in the first operand, followed by the execution of the second operand (

). We note that the definition of the CTT disabling operator has been inspired by the disabling operator of the LOTOS process algebra [START_REF] Interactions | ISO 8807: LOTOS -A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour[END_REF]. Yet, the interpretations of both operators are not identical. In particular, in LOTOS the subsequent execution of the second operand, after completion of the first one is not allowed.

The interpretation of the suspend/resume operator is similar to the one of the disabling operator. Both tasks specified by its operands are enabled concurrently. At any time the execution of the first operand can be interrupted by the execution of the first (sub-) task of the second operand. An exception to this rule are tasks within the scope of the concurrency operator ( ). Such tasks, although interrupted, may (concurrently) continue their execution. Contrary to the disabling operator, the execution of the task specified by the first operand is only suspended and will (once the execution of the second operand is complete) be reactivated from the state reached before the interruption [START_REF] Paternò | Model-Based Design and Evaluation of Interactive Applications[END_REF]. At this point, the task specified by the first operand may continue its execution or may be interrupted again by the execution of the second operand. In order to model this behavior, we have defined the auxiliary binary operator interleaved insertion ( ). It "injects" the task specified by its second operand at any possible position in-between the (sub-) tasks of the first operand. Using the auxiliary operator it is now possible to rewrite a term containing the suspend/resume operator as follows:

.

Definition 24 (Deep optionalization and interleaved insertion). Let , be ECTT task expressions, be a task identifier and be a finite map of ECTT task definitions. We then define the operators deep optionalization ( ) and interleaved insertion ( ) inductively as follows:

B. Trace properties

Based on the definitions of Section 6.1.2, we derive the following trace properties for sets of posets operations.

Proposition (Trace properties of sets of posets operations).

The sets of posets operations: sequential composition ( ), parallel composition ( ), alternative composition( ), closure (*), close and open have the following trace properties (Table 2):