Iman Poernomo
email: iman.poernomo@kcl.ac.uk

Timur Umarov
email: t.umarov@kbtu.kz

A Mapping from Normative Requirements to Event-B to Facilitate Verified Data-Centric Business Process Management

This paper addresses the problem of describing and analyzing data manipulation within business process workflow specifications. We apply a modeldriven approach. We begin with business requirement specifications, consisting of an ontology and an associated set of normative rules, that define the ways in which business processes can interact. We then transform this specification into an Event-B specification. The resulting specification, by virtue of the Event-B formalism, is very close to a typical loosely coupled component-based implementation of a business system workflow, but has the additional value of being amenable to theorem proving techniques to check and refine data representation with respect to process evolution.

Introduction

Business process management (BPM) is an increasingly challenging aspect of the enterprise. Middleware support for BPM, as provided by, for example, Oracle, Biztalk and the recent Windows Workflow Foundation (WWF), has met some challenges with respect to performance and maintenance of workflow.

The central challenge to BPM is complexity: business processes are becoming widely distributed, interoperating across a range of inter-and intra-organizational vocabularies and semantics. It is important that complex business workflows are checked and analyzed for optimality and trustworthiness prior to deployment. The problem becomes worse when we consider the enterprise's demand to regularly adapt and change processes. For example, the growth of a company, changes to the market, revaluation of tasks to minimize cost. All these factors often require reengineering or adaptation of business processes along with continuous improvement of individual activities for achieving dramatic improvements of performance critical parameters such as quality (of a product or service), cost, and speed [START_REF] Van Der Aalst | Workflow Management: Models, Methods, and Systems[END_REF]. Reengineering of a complex workflow implementation is dangerous, due to existing dependencies between tasks.

Formal methods can assist in meeting the challenge of complexity, as their mathematical basis facilitates analysis and refining of a system specification. However, com-plex systems often involve a number of different aspects that entail separate kinds of analysis and, consequently, the use of a number of different formal methods.

A business process implementation within a BPM middleware requires detailed treatment of both information flow and information content. The abstraction gap is identified by Hepp and Roman in [START_REF] Hepp | An Ontology Framework for Semantic Business Process Management[END_REF]: an abstract workflow that ignores information content provides an abstract view of business processes that does not fully define the key aspects necessary for BPM implementation.

We argue that this abstraction gap can be addressed by developing event-driven data models in the Event-B language from an initial business process requirements specification. We employ a Model Driven Architecture approach.

The initial CIM might be written as models within a number of requirements specification frameworks. We use the ontologies and normative language of the MEASUR method [START_REF] Liu | Semiotics in Information Systems Engineering[END_REF]. The method has a 20 year history and is widely used within the organizational semiotics community, but less well-known in Computer Science. Its roots lie in the philosophical pragmatism of Peirce, the semiotics of Saussure and Austin's speech act theory. It is model-based, with ontologies and normative constraints forming the central deliverables of a requirements document. We employ MEASUR notation because our starting point is information systems analysis, where MEASUR has found the most application. Its normative constraints lend themselves to transformation into our PIM languages. However, our approach should be readily adaptable to a number of similar notations in use in the multi-agents and normative specification research communities.

The Event-B language is used in specifying, designing, and implementing software systems. The language is used to develop software by a process of gradual refinement, from an abstract, possibly nonexecutable system model, to intermediate system models that contain more detail on how to treat data and algorithms, to a final, optimized, executable system. In this process, (i) the first abstract model in this refinement chain is verified for consistency and (ii) each step in the refinement chain is formally checked for semantic preservation. Consistency will then be preserved throughout the chain. Therefore, the final executable refinement can be trusted to implement the abstract specification.

Our approach addresses the semantic gap by defining a transformation of MEASUR models to Event-B machines, permitting: (i) a full B-based formal semantics for vocabularies and data manipulation that is carried out within the modeled workflow, which can be validated for consistency; and (ii) an initial, abstract B model that can be refined using the B-method to a final optimal executable system in an object-oriented workflow middleware, such as WWF.

A notion of semantic compatibility holds over the transformed models, so that any property derived over the normative-ontological view of the system will hold over potential processes that arise from the Event-B machine.

The paper proceeds as follows:

-In Section 2, we sketch the nature of our CIM, the normative ontology language of MEASUR.

-Section 3 provides a brief introduction to Event-B specifications, focusing on the main points relevant to our formal semantics.

-Section 4 then outlines the transformation approach to generating Event-B specification. We discuss how the resulting specification provides a formal semantics of our data-centric business process, and how this enables consistency validation checks. -Section 5 discusses related work and conclusions.

MEASUR Models

The MEASUR can be used to analyze and specify an organization's business processes via three stages [START_REF] Liu | Semiotics in Information Systems Engineering[END_REF]: (i) articulation of the problem, where a business requirements problem statement is developed in partnership with the client; (ii) semantic analysis, where the requirements problem statement is encoded as an ontology, identifying the main roles, relationships and actions; and (iii) norm analysis, where the dynamics of the statement are identified as social norms, deontic statements of rights, responsibilities and obligations.

Space does not permit us to detail the first stage. Its processes are comparable to other well known approaches to requirements specification. The last two stages require some elaboration. For our purposes, they provide a Computation Independent Model, consisting of an ontology and collection of norms, that formally define the structure and potential behaviour of an organization and its processes from a non-technical perspective. We hereafter refer to the combination of a MEASUR ontology and associated norms as a normative ontology.

Ontologies

The ontologies of semantic analysis are similar to those of, for example, OWL, decomposing a problem domain into roles and relationships. As such, our ontologies enable us to identify the kinds of data that are of importance to business processes. A key difference with OWL is the ability to directly represent agents and actions as entities within an ontology. This is useful from the perspective of business process analysis, as it enables us to identify tasks of a workflow and relate them to data and identify what agent within the organization has responsibility for the task.

Semantic Analysis has its roots in semiotics, the philosophical investigation of signs. MEASUR applies to information system analysis a number of ideas and approaches from philosophy of language, drawing on the pragmatism of Peirce, semiotics of Saussure and the epistemology of Wittgenstein and Austin. The method's core assumption is knowledge and information exists only in relation to a knowing agent (a single human or a social organization). There is no Platonic reality which defines Truth. Instead, Truth is a derived concept that might be defined as agreement between a group of agents. An agent is responsible for its knowledge. When a group of agents agree on what is true and what is false, they accept responsibility for that judgement. Following Wittgenstein, MEASUR considers an information system as a "language game": a form of activity involving a party of agents that generates meaning. In an information-systemas-language-game, the meaning of data derives from usage by agents, rather than from a universal semantics.

Semantic Analysis represents the information system as language game in the form of an ontology diagram, identifying agents, the kinds of actions agents can perform and the relationships and forms of knowledge that can result from actions. These concepts are identified as types of affordance. An affordance is a collection of patterns of behaviour that define an object or a potential action available to an agent. Every concept in a MEASUR ontology is an affordance.

MEASUR subclasses the notion of affordance as follows. A business entity -such as a user account or a bank loan -is an affordance in the sense that it is associated with a set of permissible behaviours and possibilities of use. For the purpose of business process analysis, business entities are used to identify the main kinds of data that are of importance in an organization's processes. A relationship -such as a contractbetween business entities or agents is an affordance in the sense that it is defined by the behaviour it generates for the parties involved in the contract. Agents are affordances in terms of the actions they can perform and the things that may be done to them. Agents then occupy a special status in that they take responsibility for their own actions and the actions of others and can authorize patterns of behaviour. The structure of a business entity, relationship or agent is given via a list of associated properties, called determiners. Determiners are properties and attributes of affordances, such an address or telephone number associated with a user account. Units of measurement are typical data types that type determiners and other values associated with affordances. The latter two concepts are considered as affordances as their values constrain the possible behaviour of their owners.

In our treatment, affordances can be treated as types of things within a business system, with an ontology defining a type structure for the system. An actual executing system consists of a collection of affordance instances that possess the structure prescribed by the ontology and obey any further constraints imposed an associated set of norms.

Example 1. An ontology for the purchasing system is given in Fig. 1. Agents are represented as ovals and business entities as rectangles with curved edges. Communication acts and relations are shown as rectangles, with the former differentiated by the use of an exclamation mark ! before the act's name.

All affordances (including agents and business entities) have a number of typed attributes, defining the kinds of states it may be in. We permit navigation through an affordance's attributes and related affordances in the object-oriented style of the OCL. The system also involves processes that cross the boundaries of two subsystems: an order processing system, and a product warehouse system. These two subsystems are represented as agents in the ontology, eOrder and Warehouse, respectively. By default all agents contain start and end attributes.

Orders are requests for products, both represented as entities in the ontology with a requests relationship holding between them (multiplicities could be associated with the relationship to define the possibility of a number of products contained in an order). An order is associated with its customer, defined by the ordered by relationship holding between the customer agent and order entity. An order can stand in an ordered relationship with the eOrder agent, after it has been successfully processed. Communication act !receive order corresponds to the initial reception of data. tion act further deals with the newly arrived order and checks whether the clients credit limit allows for the purchase. Namely, it checks whether the total cost of the purchase is less than a customer's credit limit. This condition results in the following outcomes: if the credit limit is lower than the total cost then the system rejects the order, otherwise it initiates the invoicing process (denoted by the invoice if available communication act). It does so if the stock contains enough amount of the product for the order. If not, then the system requests to increase the stock by initiating request increase. This is followed by the actual process of increasing the stock increase stock. Finally, the system dispatches the order by dispatch order.

Norms

Norms are constraints and rules that determine how agents interact and control affordances. They also control the initialization and termination of particulars (affordance instances). We have adopted a typed language of deontic logic, logic of action, and the theory of normative positions to express logical constraints over business processes, using ontologies as atomic classes, relations, objects and actions for the logic. Our constraints take the form

A, B := R(ā) | ¬A | A _ B | A ^B | A ! B | 8 x : C • A | 9 x : C • B | Ob A | Pe A | Im A | E x A , ( 1
)
where C is an affordance (that acts as a type of a particular instance); R(ā) is an affordance with one or two antecedents Ā and ā is one or two particular instances of Ā; the meaning of ObA is that A is obliged to happen; the meaning of PeA is that A is permitted to happen; the meaning of ImA is that A is prohibited (impermissible) to happen; the meaning of E x A is that A results from, and is the responsibility of, agent particular x; the meaning of the other connectives follows standard first order logic. A conditional description of behaviour or conditional act description, which we otherwise regard as a behavioral norm, represents the general form for a constraint over our ontologies [START_REF] Liu | Semiotics in Information Systems Engineering[END_REF]:

(Trigger ^pre-condition) ! E agent Ob/Pe/Im post-condition. (2)
The informal meaning of the norm is the following: if Trigger occurs and the pre-condition is satisfied, then agent performs an action so that post-condition is Obliged/Permitted/Impermissible from resulting.

The idea of a behavioral norm is to associate knowledge and information with agents, who produce and are responsible for it. From a philosophical perspective, truth is then defined as something that an agent brings about and is responsible for. As shall be seen, from the perspective of determining how to implement a normative ontology as a workflow-based system, we view agents as corresponding to subsystems, business entities to specify data and behavioral norms to expected dynamic interaction protocols between subsystems.

Example 2. Consider the communication act !receive order from our example, corresponding to the initial reception of data by the order processing system. The idea that this reception can only occur over orders that are not yet processed is captured by the behavioral norm shown in Table 1. Both relationships and communication acts are represented as logical relations in our language, but communication acts are not used in pre-conditions, and may only be placed after a Deontic operator.

Communication acts often define resulting changes of state on related agents and entities. As shown in our ontology in Fig. 1, receive order relates three affordances: agents Customer and eOrder and business entity Order, instances of which are used as arguments for this communication act. As such, this communication act should affect the following relationships ORDERED and ORDERED BY that are involved in relating the pertinent affordances. Therefore, the reception of an order entails a change of state of affairs to include a newly arrived order, the status becomes set to "received", and the system initiates the processing stage by setting its attribute to true. This is formalized in Table 1. There have been a number of attempts to use semantic analysis normative ontologies as the language for a business process management engine. The mostly widely used is Liu's NORMBASE system [START_REF] Liu | Semiotics in Information Systems Engineering[END_REF]. In such systems, the ontology serves as a type system for data, while norms define the conditions under which tasks may be invoked to create and manipulate data.

Our approach is different: we treat normative ontologies as a useful and semantically rich requirements analysis document. However, we implement these requirements using a standard business process management infrastructure. We believe that further refinement and analysis is a necessary step to this goal. In particular, it is important to ensure that (i) the possible communication act traces permitted by a set of norms do not deadlock unexpectedly (in our example, this happens if the order processing system waits indefinitely for a response from the warehouse that stock is available); and (ii) the ontology and its associated norms do not allow for an inconsistent state of the system (this happens if an action entails that an order is processed and rejected at the same time).

Event-B

This section provides an overview of the Event-B notation which is inspired by the action systems approach [START_REF] Back | Refinement Calculus, Part II: Parallel and Reactive Programs[END_REF] and represents an evolution of the B-method. The Event-B language specifies a software system in terms of encapsulated modules, called machines, that consist of a mutable state and a number of related operations, called events, whose execution changes the values of the state. Each event consists of a logical guard and an action. The guard is a first order logical statement about the state of the machine and defines the conditions under which an action may occur. The action defines the way the machine's state may be modified as a first-order logical statement relating the initial values of the state prior to the action occurring and the final values of state.

Machines therefore have a formal operational semantics, that models system execution as a sequence of events. If an event's guard holds over the machine's state, its action may be executed. This will change machine's state, which may cause another event's guard to hold, and an action to be executed. The sequence continues until the system has halted (it is deadlocked). Note that execution is potentially nondeterministic: when a number of event guards are true, then one of the corresponding event actions is chosen at random.

A common requirement over business process descriptions is the preservation of certain properties throughout the whole course of execution of events. These properties are called invariants: they represent predicates built on the state variables that must hold permanently. This is achieved by proving that under this invariant and guards of events, the invariant still holds after modifications made to the state variables associated with event executions.

Every model written in Event-B is represented as a machine/context pair. The relationship between these two constructs is that the machine "sees" the context (read-only access, with no modification possible). The context contains the main sets, constants, axioms, and theorems. Carrier sets and enumerated sets are declared in the Sets section. Since, an enumerated set is a collection of elements, additionally, its members are defined as constants in the Constants section. An axioms section contains assignments according to which constants are defined as unique values.

A machine consists of state variables, invariants, and events. State variables represent states which the machine can be in. The Invariants box is comprised of the conditions that should hold throughout the whole execution of the machine. The events box contains the initialization construct and all events of the machine. Each event contains one or several guards and one or several actions.

Definition 1 (Consistent Event-B Machine

). An Event-B machine is consistent if the following conditions hold:

-Invariant preservation : for any event, assuming the invariant and guard are true, then the invariant and action are consistent (do not result in a contradiction). -Feasibility: given any event, if the guard holds, then it is possible for the action to be performed.

It is possible to define an operational semantics for Event-B machines, over which the runtime execution of the modeled system can be understood. Essentially, this is done by assuming the the initialization constraints to hold over the state of the machine (actual values assigned to its set of variables), and then successively selecting events based on guard checks over the variables. Each event selection will result in the action condition changing the state of the system. The resulting sequence of events is a trace of the machine. A machine will usually have a potentially infinite number of traces, due to the nondeterminism of guard selection and the nondeterminism within actual actions.

Semantic Embedding of Normative Ontologies in Event-B

In MDA terms, ontologies and norms represent a computation independent model (CIM) and Event-B machines represent platform indepedent model (PIM). CIM does not contain information of computational nature and usually describes the state of affairs verbally or using high-level logical expressions. Whereas in PIM, one can find model descriptions defined in a more mathematical manner.

In this section, we are providing a stepwise detailed mapping of our normative rule to the Event-B machine. It is important to note that we are applying our formal definition of the mapping described in Appendix.

General Mapping Strategy

The mapping of affordances is straightforward. The general framework is shown in Fig. 2.

All the elements of the source and target models are marked with different patterns to be able to segregate separate mappings of the subclasses of affordances to Event-B constructs: agents are mapped to machines, business entities and relations are mapped to Event-B sets, relations and state variables, and communication acts are mapped to events. Generating events is a rather detailed transformation and we describe it more extensively below.

The transformation of normative constraints is more difficult. Conceptually, norms of the form (2) appear similar in form to a machine event: -A trigger and pre-condition correspond to a guard. The former defines the situation that must hold before an agent can act. The latter defines the state that must hold before a machine can perform an action. -The responsibility modality E a corresponds to the location of the event within the machine corresponding to agent a. -The deontic modality Ob/Pe post-condition identifies whether the action corresponding to post-condition should be necessarily performed, or whether execution of another (skip action) is possible instead. The Im deontic modality means the negation of the post-condition holds.

Because the normative constraints are essentially abstract business rules, while the conditions of the B machine define further implementation-specific detail, the mapping will depend on how we interpret relations and functions of the ontology. For this purpose our transformation must be based on a given semantic mapping of individual relations and functions to B relations and functions. We assume this is defined by a domain expert with the purpose of wide reusability for the ontology's domain.

Example: A Stepwise Transformation of receive order

Space does not permit the full definition of the MDA transformation. Instead, we illustrate the idea by showing how the transformation applies to a single norm -that of receive order in the example. Let us consider a norm for receiving an order described in Table 1. This norm generates event receive order in machine e, because e is the responsible agent for the effect construct. Besides agent e, the norm contains another agent cc. Consequently, its corresponding mapping will also affect in certain ways the appropriate machine of cc as we illustrate below.

Norm receive order(oo,cc,e) contains a composite guard, well-formedness constraint of which is defined as follows

Each pre-condition, ¬ordered by(oo,cc) and ¬ordered(oo,e), contain instances of Entity and Agent. Furthermore, one of them contains an instance of an agent different than e. In our approach, since these guards are of the form R(a,c) we formally define them as follows: ¬ordered by(oo, cc)

' 7 ! p¬oo 2 ordered byq , (5)
where each variable is rigorously defined as

8 > > > > > > > > > > < > > > > > > > > > > : pooq 2
9 > > > > > > > > > > = > > > > > > > > > > ;
2 WFC 0 (GUARD(¬ordered by(oo, cc))) ;

(6) and ¬ordered(oo, e)

' 7 ! p¬oo 2 orderedq , (7)
where for each variable we have

Note that our transformation produces a well-formed condition that oo is both an external and an internal variable of machine e. This is not a problem, as we can assume that property of being external (ExtVAR) overrides being internal (IntVAR). This is because in Event-B a variable is rendered external simply by having its name shared between two machines.

Variable oo is defined as shared variable (ExtVAR), being an instance of Entity Order. Additionally, it can be seen that in [START_REF] Halle | Model Checking Data-aware Workflow Properties with CTL-FO +[END_REF] and ( 8) a definition of oo as an instance of Order is represented as an invariant construct (denoted as INV). Guard definitions ( 5) and ( 7) with an invariant specification are used in generating Event-B invariants and sets, where only instances of entities are involved (note: instances of Agent are irrelevant in generating sets). Applying this to our norm yields an invariant of the form oo 2 Order for both machines, because variable oo is shared. Shared variable ordered by and internal (to machine e) variable ordered are defined as subsets of Order and these constraints are specified as invariants ordered by ✓ Order and ordered ✓ Order, respectively. Furthermore, each machine has an event with its guard defined:

p¬oo 2 ordered byq 2 cc (9)
and p¬oo 2 orderedq 2 e . [START_REF] Aslam | From BPEL4WS Process Model to Full OWL-S Ontology[END_REF]. They are using overlap which exists in the conceptual models of BPEL4WS and OWL-S and perform mapping from BPEL4WS to OWL-S to avoid this lack of semantics.

Norms are used in different areas for regulating and constraining behavioral patterns in certain organized environments. For example, in the area of artificial intelligence and multi-agent systems [START_REF] Inverno | Understanding Agent Systems[END_REF], agents need to organize their action patterns in a way to avoid conflicts, address complexity, reach agreements, and achieve a social order. These patterns are specified by norms which constrain what may, must and must not be done by an agent or a set of agents. The fulfillment of certain tasks by agents can be seen as a public good if the benefits that they bring can be enjoyed by the society, organization or group [START_REF] Inverno | Understanding Agent Systems[END_REF][START_REF] Castelfranchi | Paolucci: Normative Reputation and the Costs of Compliance[END_REF].

There are several works in the scope of MDA devoted to CIM-to-PIM transformation. For example, Rodriguez, et al. [START_REF] Rodríguez | CIM to PIM transformation: A reality[END_REF] define CIM-to-PIM transformation using QVT mapping rules. The model of the information system that they obtain as a PIM are represented as certain UML analysis-level classes and the whole idea is reflected in a case study related to payment for electrical energy consumption. This work was continued [START_REF] Rodríguez | Towards CIM to PIM Transformation: From Secure Business Processes Defined in BPMN to Use-cases[END_REF] by extending CIM definitions of BPMN to define security requirements and transforming them into UML use cases using QVT mapping rules. Another approach described by Wil van der Aalst, et al. [START_REF] Van Der Aalst | Translating Workflow Nets to BPEL[END_REF] meets the difficulty of BPEL. While being a powerful language, BPEL is difficult for end-users to use. Its XML representation is very verbose and only readable for the trained eye [START_REF] Van Der Aalst | Translating Workflow Nets to BPEL[END_REF]. It describes implementation of the transformation from Workflow-Nets to BPEL which is built on the rich theory of Petri nets and can also be applied for other languages.

The Event-B language was successfully applied in several serious projects where there was a need for rigorous and precise specification of the system. For example, Rezazadeh, et al. [START_REF] Rezazadeh | Redevelopment of an Industrial Case Study Using Event-B and Rodin[END_REF] discuss redevelopment of the central control function display and information system (CDIS). CDIS is a computer-based system for controlling important airport and flight data for London terminal control center. The system was originally developed by Praxis and was operational but yet had several problems related to the questions of formalization. Namely, the problems included difficulty of comprehending the specifications, lack of mechanical proof of the consistency and difficulties in distribution and refinement. These problems were addressed in redeveloping the system using the advantages of the Event-B language and Rodin platform.

Future work will investigate how our B-based PIMs can be further transformed into an actual platform specific solution utilizing industrial BPM solutions. We hope that our specifications involving data and operations making them semantically richer will map naturally onto the modular technologies employed in, for example, WWF.

Fig. 1 .

 1 Fig. 1. Example normative ontology .

Fig. 2 .

 2 Fig. 2. The general framework of the transformation.

  WFC0 (GUARD(¬ordered by(oo, cc) ^¬ordered(oo, e))) ⌘ WFC 0 (GUARD(¬ordered by(oo, cc))) [ WFC 0 (GUARD(¬ordered(oo, e))) ,(3)and is recursively formalized as GUARD(¬ordered by(oo, cc) ^¬ordered(oo, e)) = GUARD(¬ordered by(oo, cc)) ^GUARD(¬ordered(oo, e)) .

pooq 2

 2 IntVAR(e), porderedq 2 IntVAR(e), poo 2 Orderq 2 INV(e), pordered ✓ Orderq 2 INV(e) ¬ordered(oo, e))) .

  The Processing communica-

	ORDERED_BY	ORDERED	CUSTOMER name : String limit : Float		EORDER start : Bool, end : Bool, in_stock : Bool, invoiced : Bool, processing : Bool	WAREHOUSE start, end : Bool stock_increase_request : Bool
	ORDER status: {received,				! RECEIVE_ORDER	receiving order
	pending, invoiced,
	dispatched, rejected}					processing order
	total : Float	! PROCESSING_SUCCESSFUL	! PROCESSING_UNSUCCESSFUL
					invoicing order	rejecting order
		! INVOICE_IF_AVAILABLE		! REJECT_ORDER
						increase request
		REQUESTS	PRODUCT	! INCREASE_REQUEST
						dispatching order
					! DISPATCH_ORDER

Table 1 .

 1 Communication act !receive order: norm and definition. DEFINITION 8 cc : Customer • 8 oo : Order • 8 e : eOrder • receive order(oo, cc, e) ! ordered by(oo, cc) ^ordered(oo, e) ^oo.status = received ^e.processing = >

!RECEIVE ORDER NORM 8 cc : Customer • 8 oo : Order • 8 e : eOrder• ¬ordered by(oo, cc) ^¬ordered(oo, e) ! Ee Ob receive order(oo, cc, e)

Table 2 .

 2 Norm mapping for receive order

	Norm	Generated Constructs
	MACHINE cc	MACHINE e
	VARIABLES		VARIABLES
	receive ordercall		receive ordercall, ordered
	oo, ordered by		oo, ordered by, status, processing
	INVARIANTS		INVARIANTS
	receive ordercall 2 BOOL oo 2 Order ordered by ✓ Order Event receive order trigger b =	receive ordercall 2 BOOL oo 2 Order ordered by ✓ Order ordered ✓ Order status 2 Order ! STATUS processing 2 BOOL Event receive order b =
	WHEN ¬oo 2 ordered by THEN receive ordercall := > receive order(oo, cc, e) ! ordered by(oo, cc)^ordered by := ordered by [ {oo} WHEN 8 cc : Customer • 8 oo : Order • 8 e : eOrder• ¬ordered by(oo, cc) ^¬ordered(oo, e) ! receive ordercall = > Ee Ob receive order(oo, cc, e) ¬oo 2 ordered ' THEN 7 ! 8 cc : Customer • 8 oo : Order • 8 e : eOrder• ordered := ordered [ {oo} ordered(oo, e) ^oo.status = received^status(oo) := received e.processing = > processing := > receive ordercall := ? END END
	END	END

Communication act receive order(oo,cc,e) relates the instance of Entity oo to instances of Agent cc and e. For this reason we are first generating an action for invoking this event. The machine that is calling event receive order is cc and the machine which contains this event is e, because the responsible agent in our norm is e. Therefore, for machine cc we have ACTION(receive order(oo, cc, e)) ⌘ preceive order call := >q ,

where we type a shared variable as:

which represents an invariant for machines cc and e. Shared variable receive order call is constrained strictly to machines cc and e: receive order call 2 ExtVAR(cc) ^ExtVAR(e) .

The definition of the calling event in machine cc will take the following form:

pEvent receive order trigger b =q WHEN ¬oo 2 ordered by 2 cc . THEN receive order call := > (14)

The guard for p'(receive order)q should include additionally to [START_REF] Rodríguez | CIM to PIM transformation: A reality[END_REF] the following constraint to enable the communication between machines cc and e:

preceive order call = >q 2 GUARD FOR ('(receive order), e)

under the side-condition that preceive order call = ?q 2 GUARD FOR (x, e)

for every event x 2 e such that x 6 = '(receive order) in order to prevent unwanted invocations of '(receive order) by other events in e. p'(receive order)q's final action should include preceive order call := ?q .

(17)

The mapping of meaning of the norm

and since status is a function, the transformation creates an appropriate invariant for it:

where STATUS is an enumeration set with the predefined values which are taken from the ontology and received 2 STATUS.

The full definition of event receive order of machine e will take the following form:

e . ordered by := ordered by [ {oo} status(oo) := received processing := > receive order call := ?

The overall mapping of norm receive order(oo, cc, e) is shown in Table 2.

Conclusion and Related Work

In this paper, we have provided a detailed description of our MDA mapping approach that we have applied for implementing the transformation from normative ontologies and norms to Event-B machines in order to address the semantic gap. For our source model we have combined MEASUR with the action logic and deontic logic in the light of the theory of normative positions. We have shown how semantic embedding of normative ontologies can be performed in Event-B for norm receive order. We have also given a description of the implementation by presenting different components of the transformation and their formal definitions, and provided a formal definition of the transformation in the appendix.

There are a number of related approaches for enriching workflow models [START_REF] Ehrig | Measuring Similarity Between Semantic Business Process Models[END_REF][START_REF] Halle | Model Checking Data-aware Workflow Properties with CTL-FO +[END_REF]. One of them is showing transformation from BPEL4WS to full OWL-S ontology to provide missing semantics in BPEL4WS. BPEL4WS does not present meaning of a business process so that business process can be automated in a computer understandable way


Anna Felkner
email: anna.felkner@gmail.com

Krzysztof Sacha
email: k.sacha@ia.pw.edu.pl

The Semantics of Role-Based Trust Management Languages

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

Introduction

The problem of guaranteeing that confidential data stored in computer systems is not disclosed to unauthorized users is increasingly significant for the owning organizations and for the society. A usual solution to this problem is an implementation of some access control techniques, by which users are identified, and granted or denied access to a system data and other resources.

Traditional access control schemes, like Mandatory Access Control (MAC), Discretionary Access Control (DAC) and Role-Based Access Control (RBAC), make authorization decisions based on the identity, or the role of the requester, who must be known to the resource owner. The most flexible of those schemes is role-based access control system [START_REF] Sandhu | Role-Based Access Control Models[END_REF][START_REF] Ferraiolo | Role-based Access Control[END_REF][START_REF] Ferraiolo | Proposed NIST Standard for Role-Based Access Control[END_REF], which groups the access rights by the role name and grants access to a resource to those users only, who are assigned to a particular role. This type of access control works well in a centralized system and is often used in enterprise environments.

Quite new problems arise in decentralized, distributed and open systems, where the identity of the users is not known in advance and the set of users can change. For an example, consider a university, in which the students are enrolled and registered to particular faculties, and no central registry of all the students of that university exists. The policy of the university is such that a student is eligible to attend a lecture given at each faculty, regardless of the faculty to which he or she is actually registered. However, how could a faculty (the lecture owner) know that John Smith is eligible to attend the lecture, if his name is unknown to this faculty? The identity of the student itself does not aid in making a decision whether he or she is eligible to attend or not. What is needed to make such a decision is information about the rights assigned to John Smith by other authorities (is he or she registered to a faculty), as well as trust information about the authority itself (is the faculty a part of this university).

To overcome the drawbacks of traditional access control schemes, trust management models have been proposed [START_REF] Blaze | Decentralized Trust Management[END_REF][START_REF] Blaze | The Role of Trust Management in Distributed Systems Security[END_REF][START_REF] Chadwick | Role-Based Access Control with X.509 Attribute Certificates[END_REF][START_REF] Chapin | Authorization in Trust Management: Features and Foundations[END_REF][START_REF] Felkner | Modeling Trust Mangement in Computer Systems[END_REF][START_REF] Li | Beyond Proof-of-Compliance: Safety and Availability Analysis in Trust Management[END_REF], as an approach to make access decisions in decentralized and distributed systems. Trust management is a specific kind of access control, in which decisions are based on credentials (certificates) issued by multiple principals. A credential is an attestation of qualification, competence or authority, issued to an individual by a third party. Examples of credentials in real life include identification documents, social security cards, driver's licenses, membership cards, academic diplomas, certifications, security clearances, passwords and user names, keys, etc. A credential in a computer system can be a digitally signed document.

The potential and flexibility of trust management approach stems from the possibility of delegation: a principal may transfer limited authority over a resource to other principals. Such a delegation is implemented by means of an appropriate credential. This way, a set of credentials defines the access control strategy and allows of deciding on who is authorized to access a resource, and who is not.

To define a trust management system, a language is needed for describing entities (principals and requesters), credentials and roles, which the entities play in the system. Responding to this need, a family of Role-based Trust management languages has been introduced in [START_REF] Li | Design of a Role-Based Trust-Management Framework[END_REF][START_REF] Li | RT: A Role-Based Trust-Management Framework[END_REF][START_REF] Li | Distributed Credential Chain Discovery in Trust Management[END_REF]. The family consists of five languages: RT 0 , RT 1 , RT 2 , RT T , RT D , with increasing expressive power and complexity. All the languages have a precise syntax definition, but a satisfactory semantics definition is still missing. A set-theoretic semantics, which defines the meaning of a set of credentials as a function from the set of roles into the power set of entities, has been defined for RT 0 only [START_REF] Li | Distributed Credential Chain Discovery in Trust Management[END_REF][START_REF] Gorla | Inferring Dynamic Credentials for Role-Based Trust Management[END_REF]. In this paper we define an elegant relational semantics, which applies not only to RT 0 , but also to other members of the family up to RT T .

The paper is structured as follows. The family of Role-based Trust management languages is described in Section 2 (including examples). Section 3, which is the core part of this paper, presents the set-theoretic semantics of RT T language. Final remarks and plans for future work are given in Conclusions 2 Role-Based Trust Management Languages Role-based Trust management languages are used for representing policies in distributed authorization systems. The languages combine features from trust management and role-based access control, and define a family of models of trust management systems with varying expressiveness and complexity.

All the RT languages use the notion of a role to define sets of entities, which are members of this role. Entities in RT languages correspond to users in RBAC. Roles in RT can represent both -roles and permissions from RBAC. Moreover, RT 1 and RT 2 introduce attributes of a role, in an attempt to fulfill the Attribute-Based Access Con- trol (ABAC) requirements. In ABAC systems, access control decisions are based on authenticated attributes of the entities. RT 0 is the core language of RT family, described in detail in [START_REF] Li | Distributed Credential Chain Discovery in Trust Management[END_REF]. All the subsequent languages add new features to RT 0 . A summary of the features supported by particular RT languages is shown in Table 1.

RT 1 adds to RT 0 parameterized roles, each of which can be described by a set of attributes. The attributes are typed, and can be integers, enumerations, floating point values, dates and times.

RT 2 further extends RT 1 to provide a notion of logical objects, which can group logically related entities, so that permissions to access specific resources can be assigned to them together.

RT T provides manifold roles and role-product operators, which can express threshold and separation-of-duty policies. A manifold role is a role that can be satisfied by a set of cooperating entities, e.g. in a requirement that two different bank cashiers must authorize a transaction. A single-element role can be treated as a special case of a manifold role, whose set of cooperating entities is the singleton. Threshold policies require a specified minimum number of entities to agree on some fact. The concept of separation-of-duty is related to threshold policies. In the case of a separation-of-duty policy, entities from different sets must agree before access is granted. It means that some transactions can not be completed by a single entity. This implies that no single entity can have all the access rights required to complete such a transaction.

RT D provides mechanism to describe delegation of rights and role activations, which can express selective use of capacities and delegation of these capacities. The semantics of this language is not covered in this paper.

The features of RT T and RT D can be combined together with the features of RT 0 , RT 1 or RT 2 . There are also few other languages based on RT 0 , which have not been taken into account here. A more detailed overview of the Role-based Trust management family framework can be found in [START_REF] Li | Design of a Role-Based Trust-Management Framework[END_REF].

The Syntax of RT Languages

Basic elements of RT languages are entities, role names, roles and credentials. Entities represent principals that can define roles and issue credentials, and requesters that can make requests to access resources. An entity can be identified by a user account in a computer system or a public key. Role names represent permissions that can be issued by entities to other entities or groups of entities. Roles represent sets of entities that have permissions issued by particular issuers. A role is described as a pair composed of an entity and a role name. Credentials define roles by pointing a new member of the role or by delegating authority to the members of other roles.

Language element Notation

Entity name A, B, C 2 E Set of entieties U, V, W ✓ E Role name r, s, t 2 R Role A.r, B.s, C.t 2 E ⇥ R Role expression e ::= B | B.s | B.s.t | B.s \ C.t | B.s C.t | B.s ⌦ C.t Credential c ::= A.

r e

In this paper, we use capital letters to denote entities and sets of entities (Table 2). Role names are denoted as identifiers beginning with a small letter. Roles take the form of an entity, or a set of entities, followed by a role name separated by a dot, e.g. A.r.

Role expressions and credentials shown in

Examples

The models discussed in this paper can be, in general, very complex. Therefore, we present here only simplified examples, with the intention to illustrate the basic notions and the notation. The first example demonstrates the use of RT 0 credentials, the second and the third ones show the use of RT 1 credentials and the fourth example presents the use of RT T credentials.

Example 1 (RT 0 ) A person has the right to attend a lecture, given at a university U, when he or she is a student to a faculty of this university. To be able to fulfill the role of a faculty, an organization ought to be a division of the university and should conduct research activities. John is a student registered to F, which is a division of U, and which conducts research activities. The following credentials prove that John have the right to attend a lecture:

U.lecture U.faculty.student ,

U.faculty U.division \ U.research , (1)
U.division F , (2)
U.research F , (3)
F.student John .

Example 2 (RT 1 ) The following example has been taken from [START_REF] Li | Design of a Role-Based Trust-Management Framework[END_REF]. A state university U, founded in 1955, gives special privileges to graduates, who received a diploma during the first four years of its operation, no matter which degree was conferred. Such a policy can be expressed by a single credential with attributes assigned to a role: U.privilages U.diploma(?, ?Year : [1955..1958]) .

In this example diploma is a role name that takes two parameters: The degree and the year of issue. The first question mark shows that the first attribute is insignificant. The second attribute (year), however, should take the values from 1955 through 1958.

Example 3 (RT 1 ) John wants to share pictures with his friends. However, he decided to restrict the access to his pictures to people over age 15.

John.pictures

John.friends(?Age : [15..120]) .

In this example, the acceptable values of the attribute Age are restricted to be in the range from 15 through 120.

Example 4 (RT T ) The following example has been adopted from [START_REF] Li | RT: A Role-Based Trust-Management Framework[END_REF]. A bank B has three roles: manager, cashier and auditor. Security policy of the bank requires an approval of certain transactions from a manager, two cashiers, and an auditor. The two cashiers must be different. However, a manager who is also a cashier can serve as one of the two cashiers. The auditor must be different from the other parties in the transaction.

Such a policy can be described using the following credentials:

B.twoCashiers B.cashier ⌦ B.cashier , (8)
B.managerCashiers B.manager B.twoCashiers ,

B.approval B.auditor ⌦ B.managerCashiers .

Now, assume that the following credentials have been added:

B.cashier Mary , (11)
B.cashier Doris ,

B.cashier Alice ,

B.cashier Kate ,

B.manager Alice ,

B.auditor Kate .

(16)

Then one can conclude that, according to the policy of B, the following sets of entities can cooperatively approve a transaction: {Mary, Doris, Alice, Kate}, {Mary, Alice, Kate} and {Doris, Alice, Kate}.

Set-Theoretic Semantics of RT Languages

The syntax of a language defines language expressions, which are constructs that are used to communicate information [START_REF] Harel | Modeling Languages: Syntax, Semantics and All That Stuff, Part I: The Basic Stuff[END_REF]. The primary expressions of Role-based Trust management languages are credentials and sets of credentials, which are used as a means for defining roles.

The semantics of a language defines the meaning of expressions. Such a definition consists of two parts [START_REF] Harel | Modeling Languages: Syntax, Semantics and All That Stuff, Part I: The Basic Stuff[END_REF]: A semantic domain and a semantic mapping from the syntax to the semantic domain. The meaning of a language expression must be an element in the semantic domain.

We define the meaning of a set of credentials as a relation over the set of roles and the power set of entities. Thus, we use a cartesian product of the set of roles and the power set of entities as the semantic domain of a Role-based Trust management language. The semantic mapping would associate a specific relation between roles and entities with each set of credentials. Such a relational approach allows us to define a formal semantics of RT T language.

The Semantics of RT 0

A set-theoretic semantics of RT 0 , which defines the meaning of a set of credentials as a function from the set of roles into the power set of entities, has been originally defined in [START_REF] Li | Distributed Credential Chain Discovery in Trust Management[END_REF]. A definition quoted in this subsection is a modified version of the same semantics, which has been introduced in [START_REF] Gorla | Inferring Dynamic Credentials for Role-Based Trust Management[END_REF]. Definition 1. The semantics of a set of credentials P is the least fixpoint of the following sequence of functions, which map roles to sets of entity names:

1. R 0 maps each role to an empty set , 2. R i+1 , L c2P f (R i , c),
where L is the point-wise extension of a function and f is a function that, given a (partial) semantics R i and a credential A.r e, returns all the entities that should be added to R i (A.r), as governed by e:

f (R i , A.r B) , {A.r 7 ! {B}} , (17)
f (R i , A.r B.s) , {A.r 7 ! R i (B.s)} , (18)
f (R i , A.r B.s.t) , {A.r 7 ! S C2Ri(B.s) R i (C.t)} , (19)
f (R i , A.r B.s \ C.t) , {A.r 7 ! R i (B.s) \ R i (C.t)} . ( 20
)
Although it has not been stated explicitly in [START_REF] Gorla | Inferring Dynamic Credentials for Role-Based Trust Management[END_REF], one can see that the argument of function R i is a composition of an entity and a role name, and the value of function R i is a subset of entities. Hence, the domain of function R i is a cartesian product of the sets of entities E and role names R, and the range of function R i is the power set of entities:

R i : E ⇥ R ! 2 E . (21)
Such a functional semantics has no potential to describe the meaning of RT T , which supports manifold roles and role-product operators.

The Semantics of RT T

Let E be the set of entities and R be the set of role names. P is a set of RT-credentials, which describe the assignment of sets of entities to roles, issued by other entities (or rather sets of entities).

The semantics of P, denoted by S P , is defined as a relation:

S P ✓ 2 E ⇥ R ⇥ 2 E , (22)
An instance of this relation, e.g.: ({A}, r, U), maps the role {A}.r governed by entity A 2 E to a set of entities U 2 2 E . The entities of set U must cooperate together in order to satisfy the role. If the cardinality of set U is greater than one, the role {A}.r is a manifold role. In case of RT 0 , which does not support manifold roles, all sets of entities are singleton sets.

Another instance of the relation, e.g.: ({A, B}, r, U), maps the role {A, B}.r governed jointly by two entities {A, B} 2 2 E to a set of entities U 2 2 E .

Denote the power set of entities by F = 2 E . Each element in F is a set of entities from E (a subset of E). Each element in 2 F is a set, compound of sets of entities from E.

The semantics of P can now be described in an alternative way as a function:

e S P : 2 E ⇥ R ! 2 F , (23)
which maps each role from 2 E ⇥ R into a set of subsets of entities. The members of each subset must cooperate in order to satisfy the role.

Knowing the relation S P , one can define the function e S P as follows:

e S P (U, r) = {V 2 2 E : (U, r, V) 2 S P } . (24)
The semantics of RT T can now be defined formally in the following way.

Definition 2. The semantics of a set of credentials P, denoted by S P , is the smallest relation S i , such that:

1. S 0 = , 2. S i+1 = S c2P f (S i , c), for i = 0, 1, . . ., which is closed with respect to function f , which describes the meaning of credentials in the following way (U, V, W, . . . are sets of entities, may be singletons):

f (S i , U.r V) = {(U, r, V)} , (25)
f (S i , U.r V.s) = {(U, r, W) : (V, s, W) 2 S i } , (26)
f (S i , U.r V.s.t) = [ W:(V,s,W)2Si {(U, r, X) : (W, t, X) 2 S i } , (27)
f (S i , U.r V.s \ W.t) = {(U, r, X) : (V, s, X) 2 S i ^(W, t, X) 2 S i } , (28)
f (S i , U.r V.s W.t) = {(U, r, X [ Y) : (V, s, X) 2 S i ^(W, t, Y) 2 S i } , (29)
f (S i , U.r V.s ⌦ W.t) = {(U, r, X [ Y) : (V, s, X) 2 S i ^(W, t, Y) 2 S i ^(X \ Y) = } .
(30)

Examples

We use example 1 and example 4 from section 2.2 to illustrate the definition of RT semantics.

Example 1 (RT 0 ) The sequence of steps to compute consecutive relations S i is shown in Table 3. Consecutive sections of the table describe relations S 0 through S 3 . The rows of the table correspond to entities (principals) and the columns correspond to role names. This way, a cell of the table shows the set of entities, which are members of the respective role issued by the corresponding principal. The starting relation S 0 is, by definition, empty. According to Definition 2, only credentials 3, 4 and 5, are mapped in S 0 into nonempty sets by function f . These sets are shown in relation S 1 in Table 3. In S 1 , credential 2 is mapped into instance ({U}, faculty, {F}) of relation S 2 , and in S 2 , credential 1 is mapped into instance ({U}, lecture, {John}). The resulting relation S 3 cannot be changed using the given set of credentials, hence:

S P = S 3 . (31)
Because the RT language considered in this example is RT 0 , all the sets of entities assigned to roles are singleton sets.

Example 4 (RT T ) The sequence of steps to compute consecutive relations S i in this example can be represented in a table similar to Table 3. However, all the roles in this example are issued by a single entity B, hence; there is no use of showing other entities. Therefore, each section of Table 4 The mapping of credential 8 in S 1 adds the following instances: (33)

S 2 = S 1 [ { (
The mappings of credentials 9 in S 2 and 10 in S 3 can be calculated analogously. The six sets in column managerCashiers are the union sets of set {Alice} and the six sets from column twoCashiers. The three sets in column approval are the union sets of set {Kate} and these sets from column managerCashiers, which are disjoint with set {Kate}. The resulting relation S 4 cannot be changed using the given set of credentials, hence: S P = S 4 .

Because the RT language considered in this example is RT T , there are sets of sets of entities assigned to roles. The interpretation of results shown in Table 4 is such that there are three sets of entieties, enumerated in the right bottom cell of the table, which can cooperatively approve a transaction.

Conclusions

This paper deals with modeling of trust management systems in decentralized and distributed environments. The modeling framework is a family of Role-based Trust management languages.

The core part of the paper is a definition of formal semantics for a set of Role-based Trust management credentials, which is based on a set-theoretic interpretation. The semantics has been defined as a relation between roles and sets of entities. Members of such a set must cooperate in order to satisfy the role. This way, our definition covers not only the basic RT 0 language, but also the more powerful RT T , which provides the notion of manifold roles and is able to express structure of threshold and separation-of-duty policies. Using RT T one can define credentials, which state that an action is allowed if it gets approval from members of more than one role. This improves the possibility of defining complex trust management models in a real environment.

  {B}, twoCashiers, {Mary, Doris}), ({B}, twoCashiers, {Mary, Alice}), ({B}, twoCashiers, {Mary, Kate}), ({B}, twoCashiers, {Doris, Alice}), ({B}, twoCashiers, {Doris, Kate}), ({B}, twoCashiers, {Alice, Kate}) } .

Table 1 .

 1 Supported features of RT languages.

	RT language	Supported features
		-localized authorities for roles,
	RT0	-role hierarchies,
		-delegation of authority over roles,
		-attribute based delegation of authority,
		-role intersections.
		features of RT0 plus:
	RT1	-parameterized roles,
		-attribute-relationship based delegation,
		-attribute-field constraints.
	RT2	features of RT1 plus:
		-logical objects.
		features of RT0 plus:
	RT T	-manifold roles,
		-threshold policies,
		-separation-of-duty policies.
		features of RT0 plus:
	RT D	-selective use of role membership,
		-dynamic credential delegation.

Table 2 .

 2 Syntax of RT family.

Table 2

 2 This is a delegation of authority from A to all the members of the role B.s. The expression B.s.t is called a linked role. A.r B.s \ C.tintersection inclusion -role A.r includes all the entieties who are members of both roles B.s and C.t. This is a partial delegation from A to B and C. The expression B.s \ C.t is called an intersection role. A.r B.s C.t -role A.r includes one member of role B.s and one member of role C.t. This allows expressing the structure of a threshold. ⌦ C.t -role A.r includes one member of role B.s and one member of role C.t, but those members of roles have to be different. It enables to express separation-of-duty policies.

	should be interpreted in the following

B simple member -entity B is a member of role A.r. A.r B.s simple inclusion -role A.r includes (all members of) role B.s. This is a delegation of authority over r from A to B, as B may cause new entities to become members of the role A.r by issuing credentials that define B.s. A.r B.s.t linking inclusion -role A.r includes role C.t for each C, which is a member of role B.s.

Table 3 .

 3 The relations S0 through S3.

	Relation	Entity	lecture	faculty	student	division	research
		U
	S0	F John
	S1	U F John			{John}	{F}	{F}
	S2	U F John		{F}	{John}	{F}	{F}
	S3	U F John	{John}	{F}	{John}	{F}	{F}

  has exactly one row, which corresponds to B. The columns of the table correspond to role names. A cell of the table shows the set of sets of entities that cooperatively can satisfy the respective role issued by B. Credentials 11 through 16 are mapped in S 0 into relation:

	S 1 = { ({B}, cashier, {Mary}), ({B}, cashier, {Doris}), ({B}, manager, {Alice}), ({B}, auditor, {Kate}) } . ({B}, cashier, {Alice}), ({B}, cashier, {Kate}),	(32)

Table 4 .

 4 The relations S0 through S4.

		cashier	manager	auditor	twoCashiers managerCashiers	approval
	S0 S1 S2 S3 S4	{Mary} {Doris} {Alice} {Kate} {Mary} {Doris} {Alice} {Kate} {Mary} {Doris} {Alice} {Kate} {Mary} {Doris} {Alice} {Kate}	{Alice} {Alice} {Alice} {Alice}	{Kate} {Kate} {Mary, Doris} {Mary, Alice} {Mary, Kate} {Doris, Alice} {Doris, Kate} {Alice, Kate} {Kate} {Mary, Doris} {Mary, Doris, Alice} {Mary, Alice} {Mary, Alice} {Mary, Kate} {Mary, Kate, Alice} {Doris, Alice} {Doris, Alice} {Doris, Kate} {Doris, Kate, Alice} {Alice, Kate} {Alice, Kate} {Kate} {Mary, Doris} {Mary, Doris, Alice} {Mary, Alice} {Mary, Alice} {Mary, Kate} {Mary, Kate, Alice} {Mary, Alice, Kate} {Mary, Doris Alice, Kate} {Doris, Alice} {Doris, Alice} {Doris, Alice, Kate} {Doris, Kate} {Doris, Kate, Alice} {Alice, Kate} {Alice, Kate}


Bartosz Michalik
email: bartosz.michalik@cs.put.poznan.pl

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

Towards Decision Centric Repository of Architectural Knowledge

Keywords: Architectural knowledge management, Architectural design decisions, Architectural description

Architectural design and design decisions are the key components of architectural knowledge. However, concerns, rationales, and risks should be also captured to prevent knowledge vaporization. So, how to deal with architectural knowledge in incremental knowledge refinement? We believe that usage of the knowledge repository system can support architecture evolution. In this paper, a model of knowledge repository is presented. In this model, the decision-centric approach is complemented with the architectural views to support indirect interrelations between design decisions. Support for agile development was one of the key aspects of the model design, therefore knowledge vaporisation might be reduced.

Introduction

Software architecture has become an important concept in research and industry. Generally speaking software architectural description is a response to the customer concerns (requirements). Thus, this description serves as a primary vehicle for communication among stakeholders [START_REF] Clements | Documenting Software Architectures: Views and Beyond[END_REF]. Architectural knowledge is a more general concept. The design decisions, reasoning behind them, and dependencies as well as architectural risks or trade-offs compose it. All this information help us to better understand the nature of the system being built. In addition, management of the knowledge helps to mitigate the risk of project failure, as various problems can be discovered in the early phase of software development.

However, design of software architecture is an iterative and a collaborative task. Often work on architecture begins when only a part of the requirements set is specified. Moreover, requirements can be modified at every stage of the development process. This is especially visible in the agile approaches to the software development.

Although multiple models, method and tools were proposed by researchers they failed confrontation with practice [START_REF] Kruchten | Building up and Reasoning About Architectural Knowledge[END_REF]. We believe that the benefits of the architectural knowledge acquisition can be observed when the functional knowledge management tool is available.

In this paper the model of architectural knowledge management repository is presented. In the model the design decisions are complemented with the architectural perspectives. It captures the architectural knowledge artifacts stated above. In addition we try to address the following problems:

-How to maintain the consistency of architectural descriptions in iterative architecture refinement? -How to manage changes in requirements or architectural decisions? -How to assess impact of change?

This paper is organized as follows. First, the current research in the field of architectural knowledge is discussed. Then, in Section 3 the existing models are compared. Next, in Section 4, architecture knowledge repository model is presented. In Section 5 the Ksantypa system is taken to illustrate some features of the model. Finally, the paper is concluded with the discussion of future works.

Related Work

One of the most popular architecture description (AD) models is probably the 4+1 views model proposed by Kruchten [START_REF] Kruchten | The 4+ 1 View Model of architecture[END_REF]. In that approach architecture is described using 5 views: logical (functional requirements), development (software module organisation), process (system performance, distribution, integrity), physical (system topology) and scenarios (cooperation of components presented in previous views). Recently, basing on the 4+1 views, the "3+1 views in 3D" was proposed [START_REF] Kennaley | The 3+1 Views of Architecture (in 3d)": An Amplification of the 4+1 Viewpoint Framework[END_REF], which brings the idea of presenting the software architecture in 3-dimensional space.

Multiple perspectives are also used by Clements [START_REF] Clements | Documenting Software Architectures: Views and Beyond[END_REF] in the "Views and Beyond" approach. The work suggests components and connector (C&C) perspective for documenting the runtime entities and their interactions.

Finally, views are very important part of architecture model proposed in IEEE 1471 [START_REF]Recommended Practice for Architectural Description of Software Intensive Systems[END_REF]. In the model architectural description consist of multiple views from which, each conform to given viewpoint. Architectural description identifies customers concerns and provides rationales.

Although perspective base approach became a reference point for model presented in IEEE 1471, the drift toward design decisions can be observed in its successor ISO 42010 [START_REF](IEEE P42010), Systems and Software Engineering -Architecture Description[END_REF]. In this proposal design description is defined as "a choice made that addresses one or more architecture related concerns and affects (directly or indirectly) the architecture."

More precise definition was suggested by Bosch [START_REF] Jansen | Software Architecture as a Set of Architectural Design Decisions[END_REF]. In addition to foregoing definition, design decision is a set containing "rationales, the design rules, design constrains and additional requirements". Bosch defines software architecture as a set of the architectural design decisions. Every decision can bring a modification to the architectural model presented in C&C view. In his proposal the new view for presenting design decisions was provided. The need for capturing design decisions was also presented in earlier works [START_REF] Bass | Software Architecture in Practice[END_REF][START_REF] Clements | Documenting Software Architectures: Views and Beyond[END_REF][START_REF] Hofmeister | Applied Software Architecture[END_REF]. Multiple works discuss design decision dependencies [START_REF] Tang | A Rationale-based Architecture Model for Design Traceability and Reasoning[END_REF][START_REF] Kruchten | Building up and Reasoning About Architectural Knowledge[END_REF] and traceability [START_REF] Wang | Acca: An Architecture-centric Concern Analysis Method[END_REF].

Architecture knowledge management requires a tool support. The evaluation shows that there is a gap between tools for capturing rationale, software architecture and requirements [START_REF] Jansen | Evaluation of Tool Support for Architectural Evolution[END_REF]. The author claims that the gap can be closed with the tools that support design decisions concept. Several design decision oriented tools [START_REF] Babar | A Tool for Managing Software Architecture Knowledge[END_REF][START_REF] Capilla | A Web-based Tool for Managing Architectural Design Decisions[END_REF][START_REF] Jansen | Tool Support for Architectural Decisions[END_REF] are available. However, those are only research tools and to our best knowledge no industrially used tool exists.

Differences Between Description Models

The usage of architectural knowledge (AK) can follow several scenarios: incremental architectural review, review for specific concern, evaluation of impact, getting a rationale, study the chronology, adding or changing a decision etc. [START_REF] Kruchten | Building up and Exploiting Architectural Knowledge[END_REF]. Therefore, architectural knowledge should be captured, described and stored in a form easy to interpret and extract. Architectural knowledge management system should support stakeholders in designing architecture that meets their business needs. However, architecture knowledge refinement is iterative task. During this process stakeholders face imprecise and unstable requirements. They may make wrong choices. Therefore traceability and consistency management should be supported in AK models.

The view (perspective) base approach presents architecture as a whole. With the use of views, different aspects of design are documented. However, researchers expose some drawbacks of this approach. Problems with conveying changes, traceability, documenting implications are identified [START_REF] Tyree | Architecture Decisions: Demystifying Architecture[END_REF]. Moreover design rules and constrains can be easily violated in view based models [START_REF] Jansen | Software Architecture as a Set of Architectural Design Decisions[END_REF]. Another drawback is that the stakeholders' concerns are not easy to identify in this approach, as design decisions are not explicitly stated.

For documenting architecture in Model Driven Architecture(MDA) view based approach can be used. In MDA [START_REF] Kleppe | MDA Explained: The Model Driven Architecture-Practice and Promise[END_REF] architecture is presented at two levels of details. Platform Independent Model (PIM) describes a system without implementation details and Platform Specific Model (PSM) with full knowledge of the final implementation platform. From architectural knowledge management point of view this model helps to separate technical details from construction ones.

Design decision based approach directly addresses the architectural concerns. In other words requirements (architectural What?) immediately meet solutions (architectural How?). In this model all decisions are interrelated, so design space can be explicitly explored [START_REF] Jansen | Software Architecture as a Set of Architectural Design Decisions[END_REF]. This also provides space for precise rationale capturing. Agile documenting is supported because an architect can focus on currently defined requirements and build appropriate solutions. Some papers present the architecture as a set of related design decisions. However this approach does not facilitate overall look on architecture. Moreover in incremental architecture refinement maintainability problems can occur.

Design decisions model provides coarse-grained view on the architecture whereas view model provides fine-grained overview. We believe that advantages of both the view and decision based approaches can be combined. In our model design decisions are first class entities, yet views are also used.

Architectural Knowledge Description Model

To our best knowledge, first attempt to combine architectural perspective and design decisions was published by Bosch [START_REF] Jansen | Software Architecture as a Set of Architectural Design Decisions[END_REF]. Archium meta-model consists of architecture model (based on C&C view) and design decisions model. Each design decision contains design fragment, which describes an architecture modification (architectural fragment and delta) provided with the decision. However this model supports only two types of decisions proposed by Kruchten [START_REF] Kruchten | An Ontology of Architectural Design Decisions in Software Intensive Systems[END_REF] .

In our model structural, behavioral and technical design decisions are supported. Model of architectural knowledge repository architectural description can be seen as two related layers(see Fig. 1). They present the design decision space and architectural frame (C&C view is used). Architectural frame provides additional axis on which relation between decisions can be observed and provides view on logical structure of the system.

Design Decisions

To capture requirements we have adopted Bosch model, although design decision (DD) are treated as a part of architectural description in our proposal. We define design decisions using following elements:

Problem defines stakeholders' concern. Problems are referred by design decisions however this reference can be optional as DD may be consequence of others. Decision can solve multiple problems or be partial solution to one of them. It can address various problems but from our point of view non-functional and functional requirements are the most important. To handle non-functional requirements ISO25000 model [START_REF]Software Engineering -Software Product Quality Requirements and Evaluation (SQuaRE) -Guide to SQuaRE[END_REF] is recommended.

Rationale is the reasoning behind the decision being taken. It describes why specific solution was provided.

Decision type. Three types of design decisions were considered. Apart from suggested documentation manners textural representation of design decisions can be used in each type.

-Structural decisions are mostly used to describe components and connections captured in architectural frame (AF)(see Subsect. 4.2). Furthermore, they are used to document other structural aspect of the system as the deployment or project organisation. -Behavioral decisions convey information about the dynamic aspects of the system.

To document decisions of this type, process perspective can be used. -Technical decision presents the software components used to solve the problem or integration guidance. This type of decisions together with architectural frame can be interpreted as PSM.

Description provides information about the solution for the given concern. Both, textual and view based descriptions are in use. This description can contain design guidance, rules and constrains.

Alternatives describes alternative solutions that were considered during the system design. Again, alternatives can be described with the use of views or textural information.

State contains information about the status of decision. It can be employed for maintainability purposes and change impact or repository consistency analysis. We suggest usage of four states proposed, pending, approved and obsolete although other sets of states can be used [START_REF] Capilla | A Web-based Tool for Managing Architectural Design Decisions[END_REF][START_REF] Kruchten | An Ontology of Architectural Design Decisions in Software Intensive Systems[END_REF]. During knowledge repository refinement obsolete decision can be transformed to other decision alternative or detached from decisions graph. Decision can be marked pending after architecture evaluation (when conflict was discovered) or when related decision was changed. For architecture analysis one of the architecture analysis method can be taken [START_REF] Michalik | 3-step Knowledge Transition: a Case Study on Architecture Evaluation[END_REF].

Maintainability information. This information can be used for documentation maintenance purpose. In description multiple attributes can be used but date of change and decision owner should be specified.

Version. Each decision is versioned. With the use of version evolution of given decision is recorded. Version is described with following attributes: change author, change date and version number. Each decision in knowledge repository can be interrelated with others. Decisions can be related directly (with the use of dependence and refinement connectors) or indirectly (with the use of architectural frame). Indirect relations are explained in following section of the article. Two types of direct relation are specified. Decision can be a consequence (is consequence of relation) of other decisions or refine one of them (is refinement of ) (see Fig. 2). In addition, each decision can be bound with a risk in architecture. There are also sensitivity and trade-off points [START_REF] Clements | Evaluating Software Architectures[END_REF] which can be related to one or many decisions. Therefore, results of architecture analysis can be embedded into architectural knowledge model and used for further analysis.

The importance of decision can be assessed with use of decision attributes and relations. It can be seen as a combination of importance of requirements which it satisfies. When decision space is explored, one should understand why the given decision was taken. The motivation for formation of the decision consist of: decision's rationale, alternatives and problem which is solved.

Model describes problem and architectural spaces (see Fig. 2). Binding between architectural components and requirements is embedded in design decisions space.

In conclusions, design decision is a central point of our model. The decision space provides solutions to business needs reported by stakeholders. This layer address all problems directly and binds the requirements with the component model of the architecture. Additional artifact as risks, sensitivity and trade-off points are embedded in the layer. Decisions are interrelated on two axis: direct (with the use of decisions connectors) and indirect (with the use of architectural frame).

Architectural Frame

The architectural frame (AF) presents overall view on the designed system. The second usage of this perspective in our architectural knowledge management system model is to show another axis of decisions relations. To model AF Component and Connector view was implemented. In this view, components are used to model processing units and datastores. Connectors for interactions mechanisms [START_REF] Clements | Documenting Software Architectures: Views and Beyond[END_REF]. The C&C view provides mechanisms to capture complex architectures. The components and connectors are bound with the use of ports (components interfaces) and roles (connectors interfaces). The components have composite structure. In other words each component can contain other components. Additionally, each component and connection is versioned in our model. Moreover components are contained in main module called System.

To document C&C view three notations were considered:

-ACME [START_REF] Garlan | Acme: An Architecture Description Interchange Language[END_REF] is an architecture description language (ADL). ACME is built on a core ontology of seven types of entities for architectural representation. It treats architecture as an annotated graph of components and connectors. Both language object types can be attached with a set of properties. Apart from textural representation, graphical modeling is possible with a use of Acme Studio. -UML Real-Time profile [START_REF] Herzberg | UML-RT as a Candidate for Modeling Embedded Real-time Systems in the Telecommunication Domain[END_REF] (UML-RT) was originally developed for telecommunication industry. The profile provides a natural home for expressing runtime structures, and supplies a semantic mapping to UML. Modeling with use of this profile is supported by commercial tools. -UML Components diagram [START_REF] Bjerkander | Architecting Systems with UML 2.0[END_REF] was designed to support components modeling in UML. Each component can provide or require specific interface. These interfaces are used for modeling of communication between components. Multiple commercial and non-commercial modeling tools are available.

All presented languages can be used to describe architectural frame in our model, however to model Ksantypa 3 (see Section 5) UML Components diagram was used.

In proposed model to each component or connection multiple design decisions (DD) might be attached. This feature provides a way of mapping decision directly on logic structure of the system. Consequently system requirements also are mapped. There are two types of links between DD and AF. The direct link connects design decision with a specific component or connector. The inheritable link indicates that component and its internal elements can be influenced by given design decision. If more precise linkage should be provided, direct links must be used to point all affected parts of the model.

Architectural Knowledge Repository

When this model of repository is used several scenarios mentioned in previous section can be applied. In following paragraphs some of them are presented in details:

Incremental architectural refinement. In this scenario architectural knowledge is continuously updated. Multiple artifacts can be delivered by architect or after architecture or requirements analysis meetings. Support for agile development methods is also provided. Modules for existing requirements can be designed in details whereas decisions and components refinement for unstable or general requirements may be postponed to the time when requirements are enhanced. Thanks to versioning chronological aspect of changes can be captured. Additionally, new artifact are easy to assemble with existing knowledge. Design decision space can be supplemented with new decisions.

As component is composite it can be easily refined. In addition links between model elements in both layers can be used for consistency management. Each decision can be reattached to more specific component when it appears. Therefore, the decision scope can be stated accordingly to current needs and requirements knowledge.

Evaluation of change impact. When change is introduced its impact should be evaluated. There are changes in component model, problem and decision space possible. Changes in architectural frame are in most cases a result of decision space modification, although changes in decision space or requirements should be carefully reviewed. As binding between decision and problem spaces is handled in the decisions layer, impact of requirements change can be determined using decision-requirements graph. The impact change can be observed in two dimensions: direct decisions interrelation and architectural frame dependencies.

Exploration of decision space. We can explore decision space using various criteria. Firstly, we can track relation between decisions. Secondly, we can use states or types to extract decisions subsets. Moreover we can browse decisions which provides solutions to specified groups of requirements. For example all decision concerning security issues may be easily identified. Finally, architectural components can be used to identify related decisions.

Combining this criteria we can build complex queries to repository which is hard to achieve with the flat knowledge repository models. "Find approved decisions concerning performance issues which influence data abstraction component." can be given as example.

Getting a rationale. As model support rationale capturing this scenario is easy to conduct. Rationales and motivations for given decisions are maintained and can be easily found.

In brief, presented knowledge repository model supports incremental architecture refinement. Additionally, consistency of architectural knowledge can be maintained from very beginning. Model is equipped with mechanisms that simplify traceability and analysis of data. The exploration of space can be performed with use of dependencies or queries. In addition data mining of historical data (on other project in repository) is possible. Views are used to capture solution to customer concerns but the scope of information presented in the view depend on the decision attachment place. For example deployment issues may be presented on the level of whole system or for specific submodule.

Ksantypa Case

In the previous section model of the architectural knowledge management system was presented. In this section application of this model to the real system architecture description is described. For this purpose the Ksantypa system administration module was used. First, system concept is presented, after which part of the architectural model of the system is discussed.

Introduction

Each year Poznan University of Technology serves thousands of applications. There recruitment process is two phased. In first, the required documents are provided by candidates. Then recruitment committees creates rank lists of candidates for each specialisation applicants can choose. In the last step accepted candidates confirm their choices and become students. Unfortunately this process is time consuming for both sites. Applicants must visit university at least twice and spend their time in long queues. This can be big obstacle for candidates living far from Poznan. On the other hand process occupy university human resources. Moreover it is error prone, as dean offices employees transcribe application forms manually to existing system.

To solve this problems Ksantypa system was introduced. Ksantypa is an e-recruitment system developed by Poznan University of Technology. It is designed to simplify recruitment process at the university. In this year third version of the system is developed. The Ksantypa3 is designed to serve all departments at the university and provides tools for automatic rank list generation with the regards to applicants marks and preferences in global manner. The only step which is performed in traditional way is a provision of required documents by accepted applicants. Therefore, candidates handle the data by themselves and must appear at the university only once, to finalize recruitment process. System can be seen as two cooperating parts: candidates web portal and recruitment administration module. In the following section administration module is considered and will be referred as K3 system.

Administration module supports dean office employees, recruitment committees members and system administrator. It provides functions for: defining a recruitment for given semester for all departments and types of studies, examination handling, validating application documents, ranking applicants and qualifying students. To finalize students qualification cooperation with other university system is required. In addition cooperation with banking systems is required to handle students fees. Apart from above, multiple non-functional requirements were specified. The most important concern changeability, security, performance and usability issues.

Architecture Discussion

To describe architecture of K3 architectural description model proposed in this paper was used. Following considerations deal with the intermediate version of specification. To simplify discussion, only part of design decision space is presented. K3 consist of two main modules and was written in Java. XanUI is written with the use of GWT. This module is responsible for handling user interaction. XanServ consist of several modules which communication is based on OSGi specification [START_REF] Alliance | Osgi Service Platform, Core Specification Release 4[END_REF]. The design decision space is described in diagram 3. At this point we need to mention that this is not a proposal of notation. Both part of diagram was generated with Graphviz tool to illustrate relations existing in model. In the a) part interrelation between requirements (only non-functional requirements are shown for diagram simplification) and design decisions are presented. Requirements are represented with the green boxes. The full arrows represents is consequence of relations. The is refinement of is introduced with empty arrow. This relation is used between decisions D 03 and D 05.

The D 03 deals with the communication between XanServ modules.

D 03 -communication between modules is based on OSGi specification.

Problem. N 25 components must exchangeable without the need of restarting the production server.

Rationale. OSGi was designed to handle dynamic exchange of modules. In addition components can be loosely coupled and communicate with the use only specified interfaces (OSGi secure visibility of module content in the environment).

Decision type -behavioral.

Alternatives. As an alternative implementation of self hosted dynamic module loading was considered. However this solution is not compatible with D 04 (use of Springframework as a middleware layer). Decision D 05 is a refinement of D 03 and describes the usage of Spring Dynamic Modules as an OSGi implementation. It is also a consequence of usage Springframework library in the system. D 19 (usage of VPD mechanism) was taken to secure data access on the database level. However D 21 concerns usage of shared database space for Ksantypa administration module and candidates web portal. As portal was not designed for the uses of VPD mechanism integration risk was discovered which was recorded on discussed relation's axis.

In this section case study for model usage was described. Although description of K3 architecture is not complete some characteristics of the knowledge repository model can be observed. Model enable designer to use both view and decision descriptions. This methods are complementary especially when architectural frame is taken into account. With the use of AF additional relations between requirements can be observed. Therefore additional risks may be discovered.

Conclusions

Architecture is a result of multiple decision being taken. However, it is shaped by the requirements stated for the system. With the use of our model the binding between requirements and architecture is maintained. Requirements are addressed with the use of design decisions which are first class entities in our approach.

The second important part of the model is architectural frame (AF). It provides overall view on a component structure in built system. Additionally, AF provides a space which interrelates design decisions. The analysis of those indirect dependencies allow to find additional risks, trade-offs and conflicts in decisions space. AF has the composite structure, which facilitates an incremental knowledge refinement. Therefore, designers can focus on key problems specifying in detail some modules. It can be done without description consistency loss.

Design decisions can be interdependent as well as bound with the requirements. The analysis of these dependencies simplifies the change risk and impact evaluation. In addition, decisions are documented with a number of attributes. With the use of dependencies and attributes, decisions space can be explored in multiple dimensions. With simple filtering technical decisions space is available. Adding another criteria technical decisions concerning performance issues are identified. Moreover, we belief that historical knowledge mining can provide solutions to current problems.

To conclude, with the use of presented model the architectural knowledge artifacts can be captured. Their interrelations empower multidimensional knowledge exploration and traceability.

As the repository which uses this model is under development the future work includes finalization of the project and its industrial validation. In addition, the filed of integration multimedia data from architectural meeting with existing knowledge will be explored. Another challenge is extension of the model to support product lines. The introduction of formal methods for consistency management in our model is also a problem awaiting answers.

Fig. 1 .

 1 Fig.1. Decisions mapped on architectural frame. In the top layer boxes represent requirements and ellipses design decisions. In the bottom architectural components are presented using UML components notation.

Fig. 2 .

 2 Fig. 2. Architectural knowledge repository model. Relation between requirements, design decisions and architectural frame.

Fig. 3 .

 3 Fig. 3. Ksantypa design decision dependencies. Diagram a) decision space, b) decisions relations with the use of architectural frame.