The RALph miner for automated discovery and verification of resource-aware processmodels

Software and Systems Modeling (2020) 19:1415–1441 https://doi.org/10.1007/s10270-020-00820-7 SPECIAL SECTION PAPER The RALph miner for automated discovery and verification of resource-aware process models Cristina Cabanillas1,2 ·Lars Ackermann3·Stefan Schönig4·Christian Sturm3·Jan Mendling2 Received: 14 December 2018 / Revised: 14 July 2020 / Accepted: 22 July 2020 / Published online: 8 August 2020 © The Author(s) 2020 Abstract Automated process discovery is a technique that extracts models of executed processes from event logs. Logs typically include information about the activities performed, their timestamps and the resources that were involved in their execution. Recent approaches to process discovery put a special emphasis on (human) resources, aiming at constructing resource-aware process models that contain the inferred resource assignment constraints. Such constraints can be complex and process discovery approaches so far have missed the opportunity to represent expressive resource assignments graphically together with process models. A subsequent verification of the extracted resource-aware process models is required in order to check the proper utilisation of resources according to the resource assignments. So far, research on discovering resource-aware process models has assumed that models can be put into operation without modification and checking. Integrating resource mining and resource-aware process model verification faces the challenge that different types of resource assignment languages are used for each task. In this paper, we present an integrated solution that comprises (i) a resource mining technique that builds upon a highly expressive graphical notation for defining resource assignments; and (ii) automated model-checking support to validate the discovered resource-aware process models. All the concepts reported in this paper have been implemented and evaluated in terms of feasibility and performance. Keywords Model checking ·Organisational mining ·Process mining ·Process verification ·RALph ·Resource assignment · Resource mining Communicated by Rainer Schmidt and Jens Gulden. This work was funded by the Austrian Science Fund (FWF)—Grant V 569-N31 (PRAIS); and by MCI/AEI/FEDER, UE—Grant RTI2018-100763-J-100 (CONFLEX). BCristina Cabanillas [email protected] Lars Ackermann [email protected] Stefan Schönig [email protected] Christian Sturm [email protected] Jan Mendling [email protected] 1University of Seville, Seville, Spain 2Vienna University of Economics and Business, Vienna, Austria 3University of Bayreuth, Bayreuth, Germany 1 Introduction Process mining extracts relevant information on executed business processes from historical data stored in event logs and analyses it for different purposes [59]. Process discovery organises the information extracted in the form of a process model. The richer the data in the event logs, the more facets of the underlying processes that can be discovered. Such event data typically refers to the executed activities, their timestamps and the human resources (for short resources) that were involved. The functional (activities), behavioural (control flow) and organisational (resources) perspectives of business processes can thus be discovered [24]. Most of the recent process mining techniques focus on the two former perspectives and generate textual as well as graphical representations of the discovered processes [23,45]. The target of those approaches have been both routine (or procedural) processes, which are usually modelled with imperative notations 4University of Regensburg, Regensburg, Germany 123 1416 C. Cabanillas et al. (e.g., Business Process Model and Notation (BPMN) [39]); and flexible processes, for which declarative notations are preferred (e.g., Declare [58]). A key challenge of approaches that yield rules, such as Declare constraints, based on support thresholds can produce rule sets that are inconsistent. For this reason, the constructed process models require an additional check in order to avoid or fix conflicting constraints [21]. To this end, model checking addresses the automatic verification of properties of a model. Regarding activities and control flow, a number of approaches to check process soundness [42] have been developed (e.g., [14,33]). As far as the organisational perspective is concerned, resource mining aims at discovering resource assignment constraints (or rules) specifying who is allowed to execute the process activities depending on the roles, skills and a number of properties defined in organisational models. Such constraints range from simple role-based assignments to complex constraints over several activities, like separation of duties [46,54]. The resulting resource-aware process models ideally contain expressive resource assignments including simple as well as complex constraints. First, the expressive power of the generated model depends on the resource assignment language used. Most of the existing resource assignment languages target either imperative or declarative process model notations with differing expressiveness, and so far only textual representations of the output resource assignment constraints have been provided. While benefits of graphical notations have been acknowledged [32,37,44], an approach capable of generating expressive graphical resource-aware process models has been missing. Second, resource-aware model checking aims at analysing properties of business process models related to resources. For example, it checks whether all resource assignment constraints can be satisfied with the available resources, or identifies resources that are critical for process completion. An initial set of analysis operations have been defined [17] but comprehensive support for their automated resolution is missing. Finally, the existing resource mining and resource-aware model-checking approaches have been separately developed relying on different types of resource assignment languages. Hence, support for the automated verification of automatically discovered graphical resource-aware process models is an important research gap. In this paper, we present the RALph Miner as an integrated solution with a two-fold contribution. First, we define a technique to discover resource-aware process models. It mines the constraints from event logs and represents the resulting resource-aware process models using RALph [16]. RALph is an expressive graphical notation for defining resource assignments, which is independent of the process modelling notation. Second, we introduce a novel model-checking approach that allows for the verification of RALph-aware process models in conjunction with the recent extension of the Declare language for defining multi-perspective process models (MP-Declare [12]). For this purpose, we rely on the Alloy framework [29]. We show how previously defined analysis operations are supported. To validate our solution, the RALph Miner has been implemented and the two techniques have been tested with a real use case from the university domain. This paper builds on previous work [20] that introduced the RALph Miner as a novel way of mining resource-aware graphical imperative process models together with BPMN. We have developed automated resource-aware process verification capabilities. The RALph Miner is meant to be interactively used by process analysts. To assure an appropriate response time, the performance of the verification technique has been tested in experiments based on example models. The performance of the resource mining approach was assessed in [20]. We have followed the Design Science Research Methodology (DSRM) [40] to develop and evaluate our approach. The problem identification and motivation phase is covered by Sect. 2, which exemplifies the research problems addressed. The objective of the solution phase is tackled by Sect. 3, which describes the pursued requirements as well as the existing support for them. The design and development phase involves Sects. 4–6, which first provide an overview and then explain the different components of our approach, the RALph Miner. Finally, the demonstration and evaluation phases are included in Sect. 7, which shows the evaluations conducted with details of the implementations, applications and performance tests. The paper finishes with the conclusions drawn from the work and a discussion of limitations and directions for future work in Sect. 8. 2 Background: resource-aware process discovery and verification Process participants are responsible for the correct operation of the business processes of an organisation. The specification of who must do what is known as resource assignment and is usually done based on organisational information. Organisational data include organisational units, positions, roles and characteristics of the people, such as skills. For instance, the research group (organisational unit) depicted in Fig. 1is structured as a hierarchy of positions. The group is led by a professor (SJ) accountable for the work of two secretaries (KH, RR) and three researchers (BR, SS, CC). It would be reasonable to assign resources to process activities based on their positions, for example. One of the most frequent activities related to scientific research is the management of trips for attending conferences or giving invited research talks. In a typical business trip management process, a researcher first applies for a business 123 The RALph miner for automated discovery and verification of resource-aware process models 1417 Fig. 1 Hierarchy of positions within a research group trip, which must be approved by their immediate superior. Once the trip request is approved, the applicant is in charge of booking the accommodation required and of buying the respective transport tickets. Finally, all the documentation is stored by one of the secretaries in order to preserve it for potential future needs (e.g., internal audits). This process description indicates that the process must be always executed in a similar way (procedural process). This kind of process definition is usually specified with imperative process modelling notations like BPMN [39] or Event-driven Process Chains (EPCs) [35]. A more flexible specification of the same process could be in place in another organisational unit, in which the process is described as follows: if a work trip application is approved, the respective trip request has to have been placed eventually before. The approval has to be done by a Professor. When the accommodation has been booked, the documentation is eventually stored in the system. This description, based on rules, leaves room for variation in the execution of the process (flexible process). For example, it is not specified when the transport tickets must be bought or whether they have to be bought at all. Similarly, it could be the case that other activities are performed between the application for the trip and its approval, and between the booking of the accommodation and the documentation storage, respectively. Flexibility also concerns the organisational perspective, in this case. Flexible process definitions are better specified with declarative process modelling notations like Declare [58], DCR Graphs [26] or Declarative Process Intermediate Language (DPIL) [64]. Process executions are stored in event logs (i.e., machinerecorded files that report on the execution of tasks during the enactment of the instances of a given process). In an event log, every process instance corresponds to a sequence (trace) of recorded entries, namely, events.The trace length corresponds to the number of events the trace consists of. Each event is defined by a set of attributes. These attributes typically involve an explicit reference to the enacted task and to the operating resource [59]. For instance, the following excerpt of a business trip event log encoded using the XES format [60] shows the recorded information of the completion event of an instance of the activity Apply for trip performed by the resource SS. <event> <string key="org:resource" value="SS"/> <date key="time:timestamp" value="2017-08-06T14:58:00.000+01:00"/> <string key="concept:name" value="Apply for trip"/> <string key="lifecycle:transition" value="complete"/> </event> As different activity instances could be executed by different resources, it is necessary to infer the actual resource assignment rules from the event log data. The organisational information is crucial for that purpose. Following up on the previous example, we observed five instances of the activity executed by SS, three by CC and three by BR.The analysis of such data along with the organisational model depicted in Fig. 1reveals that the activity Apply for trip is performed by a resource with the position Researcher.The output resource assignment rules should be specified together with the functional and behavioural perspectives of the process in the resulting process model, being it imperative or declarative. Furthermore, the discovery of both simple as well as complex resource assignment rules should be supported. Resource mining addresses the automated discovery of resource-aware process models whose expressive power greatly depends on the language used to define the resource assignment constraints. Verifying the correctness of the output model is crucial in order to avoid inconsistencies at run time. Imagine that resource mining over the event log of our running scenario discovered a binding of duties constraint between activities Apply for trip and Approve application. This constraint specifies that the two activities must be performed by the same 123 1418 C. Cabanillas et al. resource. However, this can never hold true if the former activity is executed by a researcher and the latter by a professor because these sets of resources are disjoint (cf. Fig. 1). Indeed, rule sets that are mined from process executions can be inconsistent if a support threshold below 100% is chosen [21]. Rule sets can also be modified by process analysts before they are put into operation. With the help of model checking [22] we can detect inconsistencies and apply the required adjustments or recovery actions. 3 Problem scope and state of the art In this section, we first define functional and non-functional requirements that we pursue and which have already been used in similar contexts. Afterwards, we analyse the state of the art with respect to such requirements. 3.1 Resource mining and resource-aware model checking requirements We aim at discovering expressive resource-aware process models, which implies that we have to use an expressive notation for defining resource assignment constraints. The expressiveness of a resource assignment language is often related to the workflow resource patterns called creation patterns [46], which describe various ways in which resources can be distributed in process activities. The more patterns a mining approach can discover, the higher expressive power it has. Therefore, providing support for discovering the creation patterns leads to requirements for an expressive resource mining (RM) approach, specifically: (RM1) Automated discovery of Direct Assignments (Dir), i.e., activities assigned to a specific resource. (RM2) Automated discovery of Role-Based Assignments (Rb), i.e., activities assigned to a specific organisational role. (RM3) Automated discovery of Capability-Based Assignments (Cb), i.e., activities assigned to a specific capability. (RM4) Automated discovery of Organisational Assignments (Org), i.e., activities assigned to a resource based on their organisational position and their organisational relationship with other resources. (RM5) Automated discovery of Separation of Duties (SoD), i.e., the obligation of allocating two tasks to different resources in a given process instance. (RM6) Automated discovery of Case Handling (CH), i.e., the allocation of all the activity instances within a given process instance to the same resource. (RM7) Automated discovery of Retain Familiar or Binding of Duties (BoD), i.e., the obligation of allocating an activity instance to the same resource that performed a preceding activity instance within a given process instance. (RM8) Automated discovery of History-Based Assignments (Hb), i.e., activity instances assigned to resources based on their execution history. Note that a requirement for the creation pattern Deferred Assignment was not included because this pattern is related to run time and cannot be inferred from the log data. Furthermore, the Authorisation and Automatic Execution patterns were disregarded because they are unrelated to the definition of resource assignment constraints. Note also that the separation of duties and binding of duties patterns are discussed in research on access-control constraints, too [54]. Graphical notations have the advantage of grouping together all the information that is used. They also support a number of perceptual inferences that may be easier to understand for humans than textual specifications [32]. We pursue the graphical representation of the discovered resource assignment constraints and the capability of dealing with procedural as well as flexible processes: (RM9) Graphical representation of the discovered resource assignments (Gr): the resource assignments can be graphically specified together with the process control flow. (RM10) Independence of the process modelling notation (Ind): the resource assignments can be defined over imperative as well as declarative process models. The second group of requirements aim to develop a modelchecking technique that allows for the verification of different properties of the output resource-aware process models. Analysis operations to check resource-aware processes have been defined in the Role-Based Access Control (RBAC) and workflow management literature [8,17,54,55,61]. The goal of the model-checking technique is to provide automated design-time support for the largest possible set of operations in order to cover a variety of needs. Providing support for the eight analysis operations that we have found formally defined in the literature (which are more technically described in Sect. 4.3) constitute the model-checking (MC) requirements in this work, in particular: (MC1) Support for the Potential Participants (PP) operation, which infers the resources that can participate in a process activity given the resource assignments in the process model. (MC2) Support for the Potential Activities (PA) operation, which infers the activities that can be allocated to a specific resource given a resource-aware process model. 123 The RALph miner for automated discovery and verification of resource-aware process models 1419 (MC3) Support for the Non-potential Activities (NPA) operation, which infers the activities that can never be allocated to a specific resource given a resourceaware process model. (MC4) Support for the Non-participants (NP) operation, which infers the resources that can never participate in the a process activity given the resource assignments in the process model. (MC5) Support for the Satisfiability (SF) operation, which checks whether the available resources can complete a workflow given its resource-aware process model. (MC6) Support for the Consistency Checking (CC) operation, which checks whether it is always possible to complete a workflow given its resource-aware process model. (MC7) Support for the Critical Participants (CP) operation, which infers the resources that are necessary to be able to execute a business process. (MC8) Support for the Critical Activities (CA) operation, which infers the activities of the process that can cause a deadlock because only one specific resource can execute them. Finally, we aim to address two non-functional (NF) requirements. The former pursues the development of an integrated approach. Having individual solutions for specific requirements can be beneficial in certain situations (e.g., when it can be assured that only procedural processes will have to be discovered or the analysis functionalities are not needed) but it limits their application under different circumstances. The need of integration has already been described in the literature [15]. The latter non-functional requirement relates to the end users of the approach, specifically, to the need of caring about performance aspects to prevent excessive response times. They are defined as follows: (NF1) Integrated support for the analysis of the discovered resource-aware process models, i.e., all analysis operations should operate on the graphical and expressive resource-aware process models automatically discovered from event logs of procedural as well as flexible processes. (NF2) Support for user interaction, i.e., the system must ensure that the end users (process analysts) get the results within a reasonable amount of time (ranging from maximum 1 to 2 seconds). 3.2 Related work In the last years, a number of techniques for mining the organisational perspective of a process have been developed [11]. Using input data from process event logs, several methods focus on extracting the organisational model or a social network [53] behind a business process, which show the characteristics and relationships among the process participants. There is also increasing interest in analysing resource behaviour and productivity [41] as well as the influence of resources on process performance [27,38,62]. The approaches that are most closely related to our resource mining research problem are those addressing the discovery of creation patterns [46] to enrich process models with resource assignments [65]. Table 1a collects them along with the support provided with respect to the resource mining requirements. Among them, the so-called staff assignment mining approach [43] is able to extract several types of assignment rules based on decision tree learning. The identification of separation and binding of duties, among others, is not addressed. The output is an imperative process model (a Petri net, an EPC or a Heuristic net) and textual resource assignments written as Staff Assignment Rules (SAR). The approaches classified as role mining [7,13,30] share a focus on organisational roles. Some of them address the pure identification of roles by analysing only the data in the event logs [30]. In this case, resource assignment is not an objective. Others aim at building an RBAC model [5] that includes the discovery of information about roles and permissions as well as role-based assignments associated with the activities [7]. In this case, the assignments are defined within the RBAC model and thus decoupled from the process model. An explicit link to the process model is present in the approach introduced in [13], which uses the Handover of Roles (HooR) principle to enrich a given control-flow model with roles that cluster the process activities under the assumption that each resource has exactly one role. BPMN and its swimlanes [39] are used to show the outcome. This as well as some of the aforementioned methods have been integrated into the ProM tool suite.1 None of the previous approaches covers the whole set of creation patterns (RM1–RM8). The DPILMiner was developed to narrow that gap [49]. It implements a three-step framework that can mine not only most of the creation patterns but also patterns that consider the control flow and the resources together. The output is a declarative process model with textual resource assignments defined with DPIL [64]. The History-based Assignment pattern (RM8) is not covered because DPIL does not support the definition of the respective resource assignments. Business process verification has usually been addressed with model checking techniques [63], which assess the internal correctness of a process model including the satisfaction of a given formula by a model (e.g., binding of duties) [34]. Focusing on resource-aware process verification, the existing support for automatically executing the operations that constitute our model-checking requirements (MC1–MC8) 1http://www.promtools.org/. 123 1420 C. Cabanillas et al. Table 1 State of the art on resource-aware process discovery and verification:  supported; (–) partly supported; – not supported; n/a not applicable Approach Resource mining requirements RM1 RM2 RM3 RM4 RM5 RM6 RM7 RM8 RM9 RM10 Dir Rb Cb Org SoD CH BoD Hb Gr Ind (a) Support for resource mining [43]–––––– [7,30]–––––––n/an/a [13]–––––––– [49]––– RALph Miner – Approach Resource-aware model checking requirements MC1 MC2 MC3 MC4 MC5 MC6 MC7 MC8 PP PA NPA NP SF CC CP CA (b) Support for resource-aware process verification [8,54,55]––––– [17] RALph Miner (−) is limited mostly to the Potential Participants, Satisfiability and Consistency Checking operations [8,54,55] (MC1, MC5 and MC6), as depicted in Table 1b. Still, as shown in the table, the eight operations have been implemented in [17]. The implementation uses description logics [6] on a textual resource assignment language called RAL. While this shows the feasibility of description logics to automatically execute some of the operations, description logics apply the so-called open-world assumption, assuming that the information in the knowledge base may be incomplete and hence, the absence of a property assertion does not imply the fact being false but unknown. As we are not working with incomplete information, we have to ensure that the data in the knowledge base always be complete, which hinders the implementation. Regarding the non-functional requirements, the disjoint sets of approaches in the two tables show the lack of an integrated solution targeting both resource mining and the subsequent analysis of the output resource-aware process models (NF1). The DPILMiner has demonstrated a performance that meets NF2 [49]. The existing implementation of the analysis operations has not been tested for performance [17]. Therefore, from the study of the state of the art we draw the following conclusions: (i) the discovery of expressive resource-aware declarative process models is covered by the DPILMiner. The definition of the resource assignments relies on DPIL, a textual declarative process modelling notation that supports several process perspectives, including the organisational perspective. Such assignments are inherently related to DPIL and cannot be used with other notations—hence, RM9 and RM10 remain uncovered; (ii) the automated verification of resource-aware process models has been addressed with description logics for process models annotated with RAL resource assignments despite the difficulties caused by the open-world assumption; and (iii) there is not an integrated approach that enables the automated verification of the expressive resource-aware process models discovered with resource mining because process discovery and verification have been separately addressed. Our goal in this work is to develop a solution that fills the existing gaps. 4 Overview of the RALph miner To address the pursued requirements, we conceptualise and integrate different techniques to provide full support for integrated resource mining and model checking functionality (NF1) within the so-called RALph Miner. An overview of the approach is depicted in Fig. 2. The baseline is a graphical notation for resource assignment called RALph [16], which is briefly described in Sect. 4.1. On top of it is RALph’s semantics, which we have defined in Linear Temporal Logic over finite traces (LTL f)[36]. LTL fconstitutes the underlying formalism for the two main functionalities developed, namely, resource mining and resource-aware process verification. Basics of LTL fare described in Sect. 4.2. As shown in the figure, to develop the required functionalities, our work builds upon two separate technologies and research streams: SQL and Alloy. While any of the two techniques could have been used to address the resource mining and model checking requirements, each of them has specific strengths that make it more suitable for a specific purpose. Following this rationale, we rely on SQL and Alloy for dif- 123 The RALph miner for automated discovery and verification of resource-aware process models 1421 Fig. 2 Overview of the integrated approach ferent purposes in order to best exploit their capabilities, as will be explained next. Specifically, SQL is used for mining process models (as explained in detail in Sect. 5) and Alloy for checking process models (as described in Sect. 6). The left hand side of the figure tackles resource mining and thus provides support for requirements RM1–RM10. As aforementioned, we rely on SQL for mining expressive RALph resource assignments from event logs. Our choice is propelled by previous findings that show that the semantics of the resource assignment patterns can be expressed through SQL queries in an efficient way [51]. Furthermore, process event logs can be easily represented or transformed to relational database tables [50,51]. In contrast, encoding complete event logs in Alloy models would not be practical and browsing the extensive search space of event logs with Alloy has proven to be inadequately slow [4]. The right hand side of the figure is concerned with the model-checking approach to address the analysis operations involved in requirements MC1–MC8. Model checking requires both a possibility to represent process models with RALph assignments and a possibility to analyse model characteristics. To the best of our knowledge, an approach to encode resource-aware process models in relational databases or SQL queries has not yet been devised. On the contrary, metamodels for encoding process models in Alloy have been presented in the literature [3,4]. Here, Alloy has been used to generate traces from a given declarative process model. Therefore, we use Alloy as a basis for automatically checking RALph-aware process models. Once RALph-aware process models have been discovered, the resulting model can be checked and varied for consistency with the RALph-aware process model checking approach. The essential concepts to understand the RALph Miner’s functionalities, including RALph, multi-perspective process mining, and resource-aware process verification in terms of the model-checking requirements, are described next. 4.1 Target resource assignment language: RALph RALph is a graphical notation for the definition of resource assignment constraints. It is expressive in terms of the creation patterns described in Sect. 3.1 (cf. [16]), and it has been designed independently of any process modelling notation so it can be combined with both imperative and declarative process models. So far it has been integrated with BPMN [16,20]. RALph assumes an organisational model representing a hierarchy of positions compatible with the metamodel depicted in Fig. 3, similar to other approaches such as [46]. This kind of organisational model includes concepts like position, role, capability and organisational unit, besides person.2The RALph notation consists of entities and connectors that enable the graphical modelling of resource assignments in relation to process models. Some of the creation patterns are directly supported with explicit constructs (e.g., Direct, Role-based and Capability-based Distribution) and others implicitly through constructs that aggregate several types of constraints (e.g., RALph history connectors enable the specification of binding and separation of duties within the same or different process instances). 2While there is not a consensus on the most common structure of organisational models [28], the organisation ontology defined by the W3C shares many concepts with RALph’s metamodel (https://www. w3.org/TR/vocab-org/). 123 1422 C. Cabanillas et al. Fig. 3 Organisational metamodel used by RALph (taken from [46]) (a) Position-based (b) Hierarchy-based (c) Binding of duties Fig. 4 Examples of RALph assignments with BPMN Figure 4a illustrates some prominent concepts of RALph. APosition entity is connected to an activity to indicate that a person with the position Researcher has to apply for a trip. In Fig. 4b, a RALph hierarchy connector is used to specify that the approval of the application must be done by someone who can delegate work to researchers (i.e., a researcher’s superior). Finally, Fig. 4c depicts a binding of duties between two activities, meaning that activity Book accommodation has to be executed by the same person who performed activity Apply for trip in that process instance. Note that if we had several assignment rules associated with one activity, the intersection of all of them (AND) would be used to find suitable resources. For more flexibility, RALph provides an alternative connector that enables the union of the resource assignment rules (OR). A more detailed description of the RALph notation can be found in [16]. 4.2 Multi-perspective process mining To do process mining, a declarative approach is typically used based on the definition of constraint templates. Constraint templates define parametrised classes of properties, and constraints are their concrete instantiations. Constraint templates are used for querying the provided event log to find solutions for the placeholders. A solution (also known as constraint candidate), is any combination of concrete values for the placeholders that yields a concrete rule that is satisfied in the event log. This approach has its roots in declarative process modelling notations, most notably in Declare [58]. For instance, a response constraint indicates that if activity A occurs, activity Bmust eventually follow. A template for this constraint parametrises the variable elements of the rule, in this case A and B. By replacing these placeholders with specific activities found in traces of an event log, pairs of activities that fulfil the constraint can be automatically identified. For example, the response constraint is satisfied in traces such as t1=A,A,B,C,t2=B,B,C,D, and t3=A,B,C,B, but not in t4=A,B,A,C.Inthis case, the second occurrence of Ais not eventually followed by B.Int2, it is actually vacuously satisfied [31] (i.e., in a trivial way, because Anever occurs). The semantics of the constraints and the templates can be formalised using formal logics, such as LTL f[36]. Declare has traditionally focused on the functional and behavioural perspectives. Hence, the operators that have been used include: –TheF,X,G, and ULTL ffuture operators: Fψ1means that ψ1holds sometime in the future, Xψ1that ψ1holds in the next position, Gψ1that ψ1holds forever in the future, and ψ1Uψ2that sometime in the future ψ2will hold and until that moment ψ1holds (with ψ1and ψ2 LTL fformulas). 123 The RALph miner for automated discovery and verification of resource-aware process models 1423 –TheO,Yand SLTL fpast operators: Oψ1means that ψ1held sometime in the past, Yψ1that ψ1held in the previous position, and ψ1Sψ2that ψ1has held sometime in the past and since that moment ψ2holds. The aforementioned response constraint is defined with LTL fas G(A→FB). An activation activity of a constraint in a trace is an activity whose execution imposes, because of that constraint, some obligations on the execution of other activities (target activities) in the same trace. For example, in the response constraint Ais an activation activity and Bis a target activity, since the execution of Aforces Bto be executed. An activation of a constraint leads to a fulfilment or to a violation. Consider again G(A→FB). In trace t1, the constraint is activated and fulfilled twice, whereas in trace t3it is activated and fulfilled only once. Referring to the formal specification of constraints in LTL f,activation φais the sub-formula that lies on the left-hand side of the implication operator →, whereas target φtis the formula that lies on its right-hand side. The importance of multi-perspective dependencies led to the definition of a multi-perspective version of Declare (MP-Declare) [12]. This version is of interest to us since we aim at defining templates for constraints that relate to the process organisational perspective. Its semantics builds on the notion of payload of an event, which is the set of attributes that define it. e( activity )identifies the occurrence of an event in order to distinguish it from the activity name. At the time of a certain event e, its attributes x1,...,xm have certain values. pe activity =(valx1,...,valxn)represents its payload. To denote the projection of the payload pe A=(x1,...,xn)over attributes x1,...,xmwith m≤n, the shorthand notation pe A[x1,...,xm]is used. For instance, pe ApplyForTrip[Resource]=SS is the projection of the attribute Resource in the event description shown in Sect. 2. Furthermore, the n-ples of attributes xiare represented as x. Therefore, the templates in MP-Declare extend standard Declare with additional conditions on event attributes. Specifically, given the events e(A)and e(B)with payloads pe A=(x1,...,xn)and pe B=(y1,...,yn),theactivation condition ϕa,thecorrelation condition ϕc, and the target condition ϕtare defined. The activation condition is part of the activation φa, whilst the correlation and target conditions are part of the target φt, according to their respective time of evaluation. The activation condition is a statement that must be valid when the activation occurs. In the case of the response template, the activation condition has the form ϕa(x1,...,xn), meaning that the proposition ϕaover (x1,...,xn)must hold true. The correlation condition is a statement that must be valid when the target occurs, and it relates the values of the attributes in the payloads of the activation and the target event. It has the form ϕc(x1,...,xm,y1,...,ym)with m≤n, where ϕcis a propositional formula on the variables of both the payload of e(A)and the payload of e(B).Target conditions exert limitations on the values of the attributes that are registered at the moment wherein the target activity occurs. They have the form ϕt(y1,...,ym)with m≤n, where ϕtis a propositional formula involving variables in the payload of e(B). 4.3 Resource-aware process verification The design-time analysis of the organisational perspective of business process models aims to ensure a correct utilisation of resources in the processes. Detected potential problems can be overcome by re-defining the processes and/or organisational data before the processes are under execution. Our approach assumes that it is always a single person responsible for the task execution. This is in line with classical workflow concepts. Note that collaborative mining [48] and collaborative resource assignment [18] have also been discussed in the literature. In the following, we describe the analysis operations underlying our model-checking requirements (cf. Sect. 3.1) in terms of their inputs and outputs as defined in the literature. Their applicability is also outlined: 1. Potential participants (PP): It takes an activity and a responsibility and returns the people who are candidates to hold that specific responsibility for the activity specified [17]. Thus, at design time, a person is a potential participant of an activity for a specific responsibility if there is some process instance in which they can be an actual holder of that responsibility. This operation serves for studying whether people are involved in specific types of activities as well as for detecting security problems derived from an incorrect assignment of permissions in terms of activity execution. It is also useful to detect activities that can be assigned to the same resources and hence, may be aggregated when creating an executable process model [24]. 2. Potential activities (PA): It lists the activities that may be allocated to one resource with regard to a specific responsibility during a process instance execution. It takes the identity of a specific person and the responsibility to be checked, and it returns the activities that can be potentially allocated to this person for that responsibility [17]. This operation is useful to provide people with a personalised list of all the activities they may be involved in or to identify the requirements for someone who is going to substitute a certain person. It also detects the degree of involvement of a person in a process in terms of the number of activities in which they can take part. 3. Non-potential activities (NPA): It takes a person and a responsibility and calculates the activities in which they cannot hold that responsibility, if any [17]. 123 1430 C. Cabanillas et al. the imported signature AssociatedElement can be used as a type of the field assoEl. This way, it is possible to declare instances of organisational metamodel signatures (Listing 3) as parts of a TaskEvent’s payload, too. The fact block adds two constraints that form an event chain (i.e., it determines the positioning of each event within the process execution trace). Without this block, instances of traceMM were unordered sets of events rather than an ordered sequence. Based on the two metamodels from Listings 3and 4the next section shows how to map RALph’s assignment templates to Alloy. 6.3 Transformation of RALph’s resource assignment templates to alloy Based on the metamodel transformation discussed in the previous section it is now possible to transform RALph’s resource assignment templates (cf. Table 2) into Alloy, too. As described in Sect. 6.1, Alloy provides two alternatives to declare reusable code fragments: predicates and functions. Since predicates are parametrisable and (unlike functions) always have Boolean results, they are suitable for representing templates. Parametrisation is important since all of the resource assignment templates can be parametrised, too. The Boolean result type of Alloy predicates reflects the binary property of instances of resource assignment templates that state that they can be either fulfilled or not. Each template from Table 2forms one Alloy predicate as shown in Listing 5. Therein, the predicates have the same ordering and naming as the templates in Table 2. Before describing the predicates it has to be mentioned that there is a slight deviation in the payload definitions between Table 2and the Alloy implementation given in Listing 3.In Table 2all elements of the organisational metamodel given in Fig. 3can be part of the payload of an event. In order to keep the Alloy code concise and readable, we decided to only allow for the person/resource element to be part of the event payload. Since it is possible to reach all other payload information by means of the transitive closure, it does not limit the expressiveness of the chosen implementation. pred directAssignment(t:Task , p:Person) { all e:HumanTaskEvent |#(t & e.assoEl) >0 implies #(p & e.assoEl) >0 } pred roleBasedAssignment(t:Task , r:Role) { all e:HumanTaskEvent |#(t & e.assoEl) >0 implies #((e.assoEl & Person).occupies. participatesIn & r) >0 } pred posBasedAssignment(t:Task , p :Position) { all e:HumanTaskEvent |#(t & e.assoEl) >0 implies #((e.assoEl & Person).occupies & p) >0 } pred capBasedAssignment(t:Task , c:Capability) { all e:HumanTaskEvent |#(t & e.assoEl) >0 implies #((e.assoEl & Person). hasCapability & c) >0 } pred unitBasedAssignment(t:Task , u : OrganisationalUnit) { all e:HumanTaskEvent |#(t & e.assoEl) >0 implies #((e.assoEl & Person).occupies. isMemberOf & u) >0 } pred negUnitBasedAssignment(t:Task , u : OrganisationalUnit) { all e:HumanTaskEvent |#(t & e.assoEl) >0 implies #((e.assoEl & Person).occupies. isMemberOf & u) =0 } pred bindingOfDuties(t1, t2:Task) { all e,f:HumanTaskEvent |#(t1 & e.assoEl) > 0and #(t2 & f.assoEl) >0implies #(e. assoEl & f.assoEl & Person) >0 } pred separationOfDuties(t1, t2:Task) { all e,f HumanTaskEvent |#(t1 & e.assoEl) >0 and #(t2 & f.assoEl) >0implies #(e. assoEl & f.assoEl & Person) =0 } pred hierarchyBasedAssignmentDelegate(t:Task , p:Position) { all e:HumanTaskEvent |#(e.assoEl & t) >0 implies #((e.assoEl & Person).occupies. canDelegateWorkTo & p) >0 } pred hierarchyBasedAssignmentReport(t:Task , p: Position) { all e:HumanTaskEvent |#(e.assoEl & t) >0 implies #((e.assoEl & Person).occupies. reportsTo & p) >0 } pred caseHandling(p:Person) { all e:HumanTaskEvent |(e.assoEl & Person) = p } Listing 5 RALph’s assignment rules in Alloy All predicates restrict the events that occur in a trace, where an event is already described by the trace metamodel from Listing 4. The current concept of the metamodel only supports events that describe the execution of activities by human resources. However, because of the payload abstraction via the common signature AssociatedElement it is possible to extend the metamodel with a custom module for, e.g., non-human resources. The subsequent implications (implies) always restrict rule applications to events that describe the execution of the task(s) provided as rule parameter (left part of the implication). All rule templates then use the set operator &(a.k.a. intersection) to check different properties of the Persons that are assigned to those events. For instance, the rule template unitBasedAssignment uses the term #((e.assoEl &Person).occupies.isMemberOf &u) >0 to restrict the performer of the task tto a Person that occupies a position which belongs to the provided OrganisationalUnit u. 123 The RALph miner for automated discovery and verification of resource-aware process models 1431 (a) Trace #1 (b) Trace #2 Fig. 5 Two exemplary process execution traces 6.4 Alloy-based representation of process models and execution traces Based on the representation of RALph’s resource assignment templates in Alloy (Sect. 6.3) it is possible to represent RALph-aware MP-Declare models in Alloy, too. This is necessary in order to use Alloy for checking those models with respect to the analysis operations defined in Sect. 3.1. // (a) RALph -aware MP-Declare model one sig Aextends Task{} one sig Bextends Task{} one sig John extends Person{} one sig Sarah extends Person{} fact { separationOfDuties[A,B] } // (b) Given process execution trace fact { #(atPos[A,add[integer/min ,0]] #(atPos[B,add[integer/min ,1]] } Listing 6 Representing process execution traces in Alloy Listing 6shows the Alloy representation of (a) a process model and (b) a (maybe partial) trace of its execution. The process model consists of the two activities Aand Bas well as the two persons John and Sarah. In the first fact block, RALph’s resource assignment template separation of duties (Table 2) is instantiated and configured with the two activities Aand B. This means that if the two activities are executed within the same process instance, the performers have to be different. Additionally, the approach can be configured with an empty, partial or complete process execution trace. This allows running all analysis operations (cf. Sect. 3.1)tobe evaluated either for an initial or a particular execution state of the process. More concretely, this means it enables the user to specify a sequence of fixed events forming a trace which describes the progress of a process instance. This process instance can be completed but does not have to. If it is not completed, the trace is referred to as partial. The given trace in Listing 6comprises two events and is encoded in an Alloy fact block. The first event is restricted in a way that it has to cover information that says that some activity Ahas been performed first. In contrast, the second event describes the execution of some activity B. No resource assignments are specified within the trace. A potential use case could be to check the effect of the separation of duties for the two given activities. Alloy is able to create examples that are valid regarding the given model. An exemplary6result is shown in Fig. 5. Figure 5shows two process execution traces that are visualised by means of the graphical representation capabilities of Alloy’s analysis engine. Both of the traces show two Human- TaskEvents, respectively, where one describes the execution of activity Aand the second describes an execution of activity B. The only difference is that in Fig. 5aSarah executed activity Awhile John was responsible for activity Bwhereas in Fig. 5b it is the other way round. The Alloy analysis engine exhaustively searches for examples that fulfil the given model and, for the example given in Listing 6, the results given in Fig. 5are complete. This shows the effect of the separation of duties since there is no example where both activities A and Bare executed by the same resource. Though the approach discussed in [4] does not use RALph, the included principle already describes how MP-Declare models as well as process execution traces can be encoded in Alloy. Although the given examples only show resource assignments, both MP-Declare as well as the trace metamodel allow for specifying more aspects of an event’s payload. However, they are not discussed in the paper at hand for the sake of conciseness. Instead, the authors refer to 6This example assumes a trace length of two. Since the current paper focuses on model checking rather than example generation the details for the latter are skipped. 123 1432 C. Cabanillas et al. examples in [4] that show the involvement of, for instance, the data perspective. 6.5 RALph-aware MP-declare process model checking with alloy In general, Alloy provides flexibility regarding the model properties that are desired to be checked. The remainder of this section discusses how properties of RALph-aware MP- Declare process models can be checked. For the current paper the model checking approach comprises the design-time execution of the analysis operations that constitute our process verification requirements. In order to enable Alloy to check RALph-aware MP- Declare process models the desired analysis operations have to be encoded in Alloy, too. Hence, the model checking approach is based upon two main building blocks—(i) a set of Alloy predicates that represent analysis operations and (ii) an Alloy command configuration. Alloy predicates are reusable pieces of code that become active either by using them in a fact block or in combination with an Alloy command (cf. Sect. 6.1). The predicates for analysis operations formulate (in general) a contradiction to what the particular analysis operation should compute. Using the Alloy check command these contradictory statements are refuted by showing counter examples that contain the results of the particular analysis operations. For instance, for determining Potential Participants for a given activity, the predicate states that the activity is never executed by any resource. By applying Alloy’s check command this statement is refuted by showing exemplary executions (a.k.a. HumanTaskEvents) where a valid resource participates. Since Alloy provides a scope-complete analysis,7those examples in sum show all potential participants. The necessary building blocks (i.e. the predicates and the configuration of the check command) are explained in detail in the remainder of this section. Alloy predicates for the analysis operations. The analysis operations are generally represented as predicates, which makes them (i) parametrisable and (ii) usable with the Alloy commands. Listing 7shows an Alloy representation for several analysis operations described in Sect. 4.3. // Potential participants (Requirement MC1) pred PP(t:Task) { all e:HumanTaskEvent |#(e.assoEl & t)>0 implies #(Person & e.assoEl)=0 } // Potential activities (Requirement MC2) pred PA(p:Person) { 7Scope-complete here means that Alloy is able to compute all examples that refute the discussed statement that are within the defined maximum trace length. all e:HumanTaskEvent |#(e.assoEl & Task)>0 implies #(p & e.assoEl)=0 } // Non-potential activities (Requirement MC3) : Not encoded as a predicate // Non-Potential participants (Requirement MC4) : Not encoded as a predicate // Critical Participants (Requirement MC7) pred CP() { all p:Person |pin HumanTaskEvent.assoEl } // Critical activities (Requirement MC8) pred CAhelper(t:Task , p:Person) { all e:HumanTaskEvent |#(e.assoEl & t) >0 implies #(p & e.assoEl) =1 } pred CA(p:Person) { no t:(HumanTaskEvent.assoEl & Task) | CAhelper[t,p] } Listing 7 RALph analysis operations in Alloy The predicate for retrieving Potential Participants (PP) formulates a statement that each execution of a given task t occurs in absence of any resource (a.k.a. Person). Potential activities (PA) are identified similarly through a statement that each time a given resource pis involved in any execution this execution is not associated with any activity. The operations Non-participants (NP) for an activity tand Nonpotential Activities (NPA) for a resource pdo not have to be encoded in Alloy, since NP is the relative complement of all resources and all potential participants for t(NP = Person - PP[t]) and NPA is the relative complement of all activities and the potential activities for p(NPA = Task - PA[p]). Consistency Checking (CC)(MC6) cannot be solved with the proposed Alloy-based approach. The reason is that Alloy is based on instance search (i.e. it solves satisfiability issues by computing examples—if existent—that prove satisfiability). However, for CC computing examples of satisfiable cases does not answer the question whether the process model is always consistent. One way to achieve this is to search for the opposite, which means searching for inconsistent examples. Consequently, the CC analysis operation would have to search for examples that violate the given specification. Inconsistent here means that it has to compute examples where a resource assignment is not possible. However, due to the constraint that each HumanTaskEvent has exactly one associated resource it is not possible to generate those examples. Nevertheless, a relaxed interpretation of this analysis operation can be the general satisfiability of the process model (MC5). This is the most native usage scenario of Alloy and can be solved by applying Alloy’s run command instead of the check command. If this application leads to one or more examples the model is proven to be satisfiable since it is possible to identify one or more examples that fulfil the model. 123 The RALph miner for automated discovery and verification of resource-aware process models 1433 Critical Participants (CP) are computed by a statement that all resources are always involved in the process. The result of applying the check command would contain all resources that do not necessarily have to be involved in the process and, thus, the result of the analysis operation is the relative complement of all resources and those that are contained in the results of applying the check command for CP. Finally, Critical Activities (CA) was split into two predicates for readability reasons. The predicate CAhelper forms a statement that each time a given activity tis executed, a given resource pmust participate in this execution. The second predicate—CA—forms a statement that for a given person p there is no task execution for which CAhelper is true. Applying the check command refutes the statement contained in CA providing counter examples containing activities that can be executed by a resource other than the given resource p. Consequently, the critical activities are all activities not contained in these counter examples (i.e., the relative complement of all activities and those contained in the counter example). Besides these analysis operations, Alloy is able to support additional operations, too. Three examples are given in Listing 8.8 // Is p in PP (pPP) pred pPP(p:Person , t:Task) { no e:HumanTaskEvent |#(e.assoEl & t)>0and #(p & e.assoEl)=1 } // Is a specific role/position/capability required for the execution of the process? pred RPC(rpc:(Position + Role + Capability)) { rpc in ((HumanTaskEvent.assoEl & Person). occupies + (HumanTaskEvent.assoEl & Person ).hasCapability + (HumanTaskEvent.assoEl & Person).occupies.participatesIn) } // Which roles are not involved in the process? pred NP { all po:Position |not RPC[po] } Listing 8 Additional analysis operations in Alloy The predicate pPP can be used to ascertain whether a given resource pis one of the potential participants of a given activity t. Therefore, it formulates a statement that no execution of tinvolves p. The second exemplary predicate (RPC) determines whether a given role, position or capability rpc is required for the execution of the process. It contains a statement that checks whether rpc is involved in any execution of any activity. If the analysis result provides counter examples this means that rpc is not required in order to execute the process. Finally, the third example (NP) computes all positions that are not involved in the process.9For that reason it reuses the predicate RPC and evaluates this predicate for all positions in the model. Hence, applying the check command 8A formal definition of these analysis operations is omitted since they are designed for illustrating our approach’s extensibility. 9The statements for roles and capabilities are analogous. retrieves all positions that can be involved in the process and, consequently, the final result is the relative complement of all positions and those contained in the analysis result. Command configuration. All questions mentioned above can be answered via Alloy’s language and analysis features. However, each answer is only valid for a given scope which describes the size of the solution space. To be more concrete, a general answer for the questions above is not possible. This is because first-order logic is in general undecidable. For that reason, Alloy requires to limit the size of the solution space by means of a scope restriction. Hence, the remainder of this section describes what that scope represents for the current approach and how it is used to configure Alloy’s check command. In Alloy, all signatures that do not have an explicit multiplicity must be restricted regarding the number of times an instance of each of them may occur in a solution produced by Alloy’s analysis engine. The example given in Listing 9shows three signatures. The abstract signature Person is already known from the organisational metamodel given in Listing 3. In Alloy, an abstract signature is used for inheritance of fields and signature facts which means that they are usually extended by other signatures. However, if no signature extends this abstract signature, Alloy instantiates the abstract signature instead. Thus, in a model without any involved resources (a.k.a. Persons), it is necessary to restrict the scope for Person explicitly. In Listing 9,Max and Mary are two signatures that extend the abstract signature Person. Consequently, a scope restriction for Person would be superfluous. However, in contrast to Mary,Max is a signature without an explicitly defined multiplicity and hence, it has to be restricted via the scope, too. Mary is a signature with a multiplicity of exactly one, so it does not require any scope restriction. As a result, the same exemplary model without the signature Max does not require any scope restriction for the signature Person since it is already restricted by Mary. In short, scope restrictions are necessary for those signatures without any explicit multiplicity. abstract sig Person extends AssociatedElement{... } sig Max extends Person{} one sig Mary extends Person{} Listing 9 RALph analysis operations in Alloy Considering the metamodel given in Listing 4, a scope restriction is always necessary for the signature TaskEvent. This scope restriction represents the maximum process execution trace length and, consequently, the number of events that the trace may consist of. Additionally, it is necessary to restrict the scope of all signatures in the RALph’s metamodel provided in Listing 3if no other signature extends them having an explicit multiplicity. However, if those signatures are extended the corresponding extending signatures 123 1434 C. Cabanillas et al. should have the multiplicity one, since capabilities, person names, etcetera, can be assumed to be clearly distinguishable. In order to give an example (cf. Listing 10 for its Alloy representation), we assume a RALph-aware MP-Declare model consisting of two activities Aand B, two resources John (who occupies position CEO) and Sarah (who occupies position CIO) and two assignment rules: •The two activities have to be executed by different resources (separationOfDuties[A,B]). •The resource that is responsible for Amust occupy the position CEO (posBasedAssignment[A,CEO]). A possible analysis operation that might be executed for the given model could be the retrieval of potential participants for activity A. This can be achieved by creating an assertion which states that the predicate PP (cf. Listing 7) holds for the given argument A. Applying the check command to this assertion causes Alloy’s analysis engine to create counter examples that falsify this assertion if possible—for the given scope. one sig Aextends Task{} one sig Bextends Task{} one sig John extends Person{}{occupies =CEO } one sig Sarah extends Person{}{occupies =CIO } one sig CEO extends Position{} one sig CIO extends Position{} fact { separationOfDuties[A,B] posBasedAssignment[A,CEO] } assert opPP { PP[A] } check opPP for 2 TaskEvent , 0 Role , 0 Capability , 1 OrganisationalUnit Listing 10 Exemplary scope restriction Alloy’s check command can be configured regarding the number of times an instance of a particular signature may occur in potential results of executing the analysis operations. This is what is already mentioned as scope restriction. Listing 10 shows an exemplary scope restriction to two for the metamodel signature TaskEvent (cf. Listing 4). This means that, independently from any other constraint or restriction, all analysis operations are performed for process execution traces consisting of two events at most. Listing 10 contains extensions for the metamodel signatures Person and Position (cf. Listing 3). For the remaining signatures of RALph’s metamodel a scope restriction is necessary. Thus, the call of Alloy’s check command is accompanied by scope restrictions for all those signatures. Since the exemplary RALph-aware MP-Declare model does not mention anything about roles or capabilities, we can set the expected number of instances of those signatures to zero. In contrast, OrganisationalUnit must be set to at least one since RALph’s metamodel (Listing 3) requires that a Position is member of exactly one OrganisationalUnit. Though this necessary background knowledge seems to be an uncomfortable limitation of the proposed approach, we rather suggest an automation procedure as future work. This is valid since this internal knowledge about the metamodel is static and therefore, can be reflected by likewise static rules. Figure 6shows a partial result for the analysis operation for retrieving potential participants for activity A. It is a partial result because it contains only one potential participant while the full set of potential participants can be retrieved by iterating over all examples. The visualisation in Fig. 6shows a process execution trace consisting of two events. However, the analysis operation asks for specific event details, namely, the performers of activity A. This specific detail is marked with $PP_e; the performer in the marked event is one potential participant for activity A. Since Alloy searches exhaustively for examples (counter examples in this case) with respect to the given scope, the resulting set of potential participants is complete with respect to the given scope, too. This dependency to the scope and further implications are discussed in the subsequent paragraph. Implications of the necessity of a scope restriction. There are two major implications that result from the necessity to artificially configure the size of the solution space in terms of a scope restriction: (i) scope-boundedness of results and (ii) necessity of background knowledge. Scope-boundedness of results means that the result of each analysis operation is only valid for the given scope restriction and, consequently, it is not possible to answer any analysis question in general. This requires the follow-up conclusion that the results of the analysis operations might differ depending on the configured scope. If, for instance, the scope for TaskEvent is too low, running the analysis operation PP for activity Amight produce an empty set—just because the TaskEvent scope does not allow an event where Ais executed (e.g., because of control-flow restrictions) and not because there is no resource that could execute this activity. However, always configuring a “huge” scope significantly lowers the performance [3,4] and thus, leads to an issue from a pragmatic point of view. Hence, an efficient scope—denoting a scope that is both able to produce valuable analysis results while being still performant—heavily depends on the respective model and the analysis question. A second implication—the necessity of backgroundknowledge—results from the scope-boundedness. More concretely, the approach currently requires background knowledge about the given process model in terms of the required size of analysis results. This is necessary in order to choose an efficient scope restriction. For the current state of the proposed approach this is a manual task. Thus, the current state of 123 The RALph miner for automated discovery and verification of resource-aware process models 1435 Fig. 6 Example result after invoking the check command from Listing 10 the approach assumes that sufficient background knowledge about the process model is available. However, since the proposed approach focuses on design-time checking the target user group are modelling experts that are in charge of developing the process model. Consequently, the assumption of background knowledge is consistent with the intended application environment. 7 Implementation and evaluation In this section, we provide details and examples of the RALph Miner implementation and evaluate its components. In particular, we show the feasibility of the resource mining and resource-aware process verification approaches (cf. Sect. 7.1) as well as the performance of the latter (cf. Sect. 7.2). The performance of the SQL-based resource mining approach with RALph was already assessed in [20]. We also briefly report how the system requirements defined in Sect. 3.1 are supported (cf. Sect. 7.3). 7.1 RALph miner The RALph mining approach has been implemented as a web-based process mining tool. The implemented architecture and used toolset are illustrated in Fig. 7.Weaimat discovering RALph-aware process models and hence, two main elements must be discovered, namely, the definition of the process itself (i.e., the functional and behavioural perspectives) and the resource assignment rules for the process activities (i.e., the organisational perspective). As mentioned in Sect. 1, there is a number of approaches for discovering a business process. Implementations for many of them are available as plug-ins in the ProM framework.10 We use the BPMN Miner tool with a XES event log to extract a resourceunaware BPMN model. Afterwards, the resulting BPMN model is exported as an XML file according to the BPMNXML specification [39]. We use the SQL mining approach 10 http://www.promtools.org/doku.php. described in Sect. 5.3 for extracting RALph assignment rules. Since this approach builds on the relational RXES event log representation, we first have to import the XES event log to relational database tables in RXES format as well as make the organisational information available as tables as explained in Sect. 5.3. We can then run the set of SQL queries required to extract RALph resource assignment rules. The resulting assignment rules are attached in the previous BPMN-XML file to the respective activity as specific resource tags. Here, we match activities from the given BPMN model and the extracted assignment rules based on activity identifiers given in the event log. The RALph-aware BPMN model is then visualised in the graphical BPMN diagram editor bpmn.io,11 which has been extended with the RALph symbols. For automatically arranging and layouting the RALph assignment symbols in the process diagram, we used a Java Script based implementation of the Sugiyama graph layout algorithm [25]. Additionally, the underlying formal RAL expressions can be imported and edited in BPMN editors like Signavio.12 A plug-in is available to automatically analyse such RAL assignments so that the RAL-aware process model can be automatically executed [19]. As a proof of concept, we applied the described toolset to an event log of a university business trip management system. The log contains 2104 events of eight different activities related to the application and the approval of university business trips as well as the management of accommodations and transfers (e.g., booking accommodations and transport tickets). The system has been used for six months by eleven employees of a research institute. The organisational model of the institute comprises two organisational units: Administration, with two employees; and Research Group, divided into three positions that include one professor, six researchers and two secretaries as depicted in Fig. 1. On the given event log, we were able to execute all RALph resource assignment queries (cf. Table 2) in less than one second. The resulting BPMN model with the extracted RALph assignment rules 11 BPMN Viewer and Editor, https://bpmn.io. 12 https://www.signavio.com. 123 1436 C. Cabanillas et al. Fig. 7 Implementation architecture and mining procedure Fig. 8 User interface of RALphMiner with extracted assignment rules is shown in Fig. 8. The screenshot also shows the extended bpmn.io modelling toolbox on the left-hand side. Note that the model has not been pruned as described in Sect. 5.4 since the implementation of that post-processing feature is still pending work. Therefore, the model contains some assignment rules that are irrelevant (e.g., the direct assignment of entity SJ to Approve Application or the binding of duties rule between Book accommodation and Buy transport tickets). As a second part of our proof of concept the discovered process model (Fig. 8) was translated into Alloy.13 Since RALph is independent from a particular modelling language for the definition of the control flow, the subsequent explanations focus on the resource perspective and skip the behavioural aspect. 13 The full example is available online: https://github.com/ stefanschoenig/mpdeclaremining. 123 The RALph miner for automated discovery and verification of resource-aware process models 1437 one sig Admin1 extends Person{}{ occupies = AdminPosition } one sig Admin2 extends Person{}{ occupies = AdminPosition } one sig Secretary1 extends Person{}{ occupies = Secretary } one sig Secretary2 extends Person{}{ occupies = Secretary } one sig Researcher1 extends Person{}{ occupies =Researcher } one sig Researcher2 extends Person{}{ occupies =Researcher } one sig Researcher3 extends Person{}{ occupies =Researcher } one sig Researcher4 extends Person{}{ occupies =Researcher } one sig Researcher5 extends Person{}{ occupies =Researcher } one sig Researcher6 extends Person{}{ occupies =Researcher } one sig SJ extends Person{}{ occupies = Professor } one sig Researcher extends Position{}{ #participatesIn =0 isMemberOf =ResearchGroup #canDelegateWorkTo =0 #reportsTo =0 } one sig Secretary extends Position{}{ #participatesIn =0 isMemberOf =ResearchGroup #canDelegateWorkTo =0 #reportsTo =0 } one sig Professor extends Position{}{ #participatesIn =0 isMemberOf =ResearchGroup canDelegateWorkTo =Researcher #reportsTo =0 } one sig AdminPosition extends Position{}{ #participatesIn =0 isMemberOf =Administration #canDelegateWorkTo =0 #reportsTo =0 } one sig Administration extends OrganisationalUnit{} one sig ResearchGroup extends OrganisationalUnit{} Listing 11 Exemplary organisational model in Alloy Listing 11 shows the representation of the organisational model. The first block of signatures represents the eleven employees that are distributed over three explicitly mentioned positions. An additional position was introduced (AdminPosition) since RALph’s metamodel given in Fig. 3 prescribes that resources are assigned to organisational units via their positions (cf. relation isMemberOf in Position). The last two signatures describe the two organisational units. fact { // RALph resource assignment rules bindingOfDuties[ApplyForTrip , BookFlight] bindingOfDuties[ApplyForTrip , BookAccommodation] bindingOfDuties[ApplyForTrip , BuyTransportTickets] bindingOfDuties[BookAccommodation , BookFlight] bindingOfDuties[BookAccommodation , BuyTransportTickets] bindingOfDuties[BookFlight , BuyTransportTickets] posBasedAssignment[ApplyForTrip , Researcher ] posBasedAssignment[EditResponse , Secretary] posBasedAssignment[ArchiveTripDocuments , Secretary] directAssignment[ApproveApplication , SJ] hierarchyBasedAssignmentDelegate[ ApproveApplication , Researcher] unitBasedAssignment[CheckApplication , Administration] assert testPP { PP[BookFlight] } check testPP for 8 TaskEvent , 0 Role , 0 Capability , 2 OrganisationalUnit , 4 Position } Listing 12 Exemplary assignment rules Alloy Listing 12 shows the Alloy representation of the assignment rules depicted in Fig. 8. The potential participants of an activity can be retrieved by means of the PP predicate. In the example it is applied to the activity BookFlight.The corresponding check command is configured for the maximum number of events that may occur within one process instance—which is equal to the number of activities since each activity has to be executed exactly once. The remaining scope parameters are depending on the organisational model which contains no roles and no capabilities but two organisational units and four positions. Alloy’s analysis engine interprets the check command and generates examples of potential participants. Collecting all of them shows that this comprises all resources occupying the position Researcher. This is because a rule bindingOf- Duties was applied for the two tasks ApplyForTrip and BookFlight. However, if we encode a partial trace with a single event that associates Researcher2 with ApplyForTrip,the retrieved potential participants for BookFlight are reduced to Researcher2 which conforms to the sequence of bindingOf- Duties constraints. 7.2 Performance of RALph-aware MP-declare model checking In this section, we describe the evaluation of our resourceaware model checking approach regarding performance measurements. In particular, we measure the time that Alloy’s analysis engine needs to determine one single solution for a given maximum number of events n. Within a RALph model checking setting, this represents the time Alloy needs for calculating one specific execution instance of the given RALph-aware MP-Declare process model of trace length n. For measuring the execution time of the approach, we use a RALph-aware MP-Declare process model that consists of the following entities: (i) three activities A, B and C; (ii) three MP-Declare constraints covering the control-flow per- 123 1438 C. Cabanillas et al. Fig. 9 Performance evaluation of RALph-aware model checking spective; and (iii) BindingOfDuties(A,B) and Separationof- Duties(B,C) representing RALph assignment constraints. The organisational model consists of two different roles, capabilities and organisational units each. For the given model we measured the runtime performance for a maximum trace length of n=20. Already existing performance measurements showed the trace length’s strong influence on the computation time [3,4]. Since the current paper focuses on resource assignment, we keep the trace length fixed and pick the constant arbitrarily. Consequently, the experimental setup varies the number of positions and resources in the range from 0 to 100. The measurements visualised in Fig. 9have been performed on a Dell Latitude E6430 (Core i7-3720QM, 8 x 2.6GHz, 16 GB RAM, SSD drive and Win 8 64 Bit). Our experimental setup applies the analysis operation for retrieving potential participants for activity B. This means that the collected performance data represents the computation times for one potential participant for the corresponding variation of the number of resources and positions. Consequently, the computation time for retrieving all potential participants can be calculated by multiplying a particular computation time from Fig. 9with the number of resources at its worst. We say “at most” since the actual computation time will usually be smaller because only a subset of all resources will be potential participants of B. The results (i.e. the time measured for retrieving one potential participant) show that the calculation of one single solution of the given RALph-aware MP-Declare process model is performed in less than 1 second in most of the cases. The figure additionally shows that the execution time is mainly influenced by the number of positions and not by the number of resources. This is caused by the fact that Alloy needs to check all variations of possible resource-to-position mappings, which results in a potentially huge number of possibilities. The calculation run time scales linearly (i.e., calculating two possible solutions will double the given runtime values). 7.3 Discussion Table 1includes the support provided by our integrated solution, the RALph Miner, for the functional and non-functional requirements that frame this work. Almost all the creation patterns can be mined and represented with the output resource assignment notation, RALph. The only exception is History-based Assignment (RM8). History-based assignments can be defined with RALph constructs. However, our mining approach currently does not consider data from past process instances to infer resource assignment constraints. RM9 and RM10 are supported thanks to RALph’s design. The resource-aware process verification component of the RALph Miner provides automated support for the execution of seven of the eight analysis operations behind the modelchecking requirements. MC6 (Consistency Checking) cannot be implemented in a comprehensive and smart way. A bruteforce solution could be defined but this requires to implement the brute force strategy outside of Alloy. The reason for that is the necessity to encode all potential execution states of the process by means of a trace in Alloy. However, since the current metamodel is limited to a representation of the execution state of exactly one process instance it is necessary to generate asetinstead of one Alloy model, one for each potential execution state. As depicted in Fig. 2, the RALph Miner constitutes an integrated solution for resource mining and resource-aware process verification, satisfying non-functional requirement NF1. Note that three different modelling languages are used: BPMN as a graphical process modelling language, MP- Declare with its strong logical foundation, and RALph, which is the connection point of the proposed tools and thus, serves as an integration base. RALph is independent from any particular process modelling language but in order to make it usable with existing process modelling languages and tools, it is integrated with BPMN for the process mining task and with MP-Declare for model verification. Both BPMN and MP- Declare here serve as host languages for enabling the control flow perspective of processes, too. This shows RALph’s flexibility on the one hand side and adapts existing approaches on the other hand side, allowing us to concentrate on the integration based on RALph’s logical foundation instead of reinventing process mining and verification techniques. Furthermore, since RALph’s formal semantics is defined independently from any process modelling language but is implemented in both BPMN and MP-Declare in an additive way, it is straightforward to map a RALph assignment rule discovered by an BPMN-based process mining technique to MP-Declare. Lastly, the performance evaluations of the resource mining and the resource-aware process verification components (cf. [20] and Sect. 7.2, respectively) conclude that NF2 is also supported. 123 The RALph miner for automated discovery and verification of resource-aware process models 1439 8 Conclusions and future work In this work we have focused on the organisational perspective of business processes and we have developed the RALph Miner, an integrated solution that allows for the automated discovery of expressive graphical resource-aware process models and their automated verification. We have used the RALph notation for defining the resource assignments in the discovered resource-aware process models. RALph’s semantics has been defined using LTL fas a common semantic foundation to give support to the resource mining and modelchecking approaches. We have shown how the RALph Miner provides full support for eighteen of the twenty system requirements identified from studies of the literature involved with resource management in different domains. Nevertheless, our work also has some limitations that we aim to tackle in future efforts. Regarding the resource mining approach, the implementation of the pruning step after the discovery of the RALph-aware process models is the next task to be performed. As for resource-aware process model checking, the transformation of RALph templates to Alloy code needs to be done manually at the moment. In addition to the described usability issues, we will also try to further improve the performance of the introduced model-checking approach with a smarter configuration of the Alloy’s analysis engine. As far as the scope is concerned, the two requirements not supported or partly supported at the moment will be further addressed. Finally, since use cases might differ in terms of the resource specialisation, we plan to investigate the impact that that may have on the RALph Miner by testing it on more use cases. Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecomm ons.org/licenses/by/4.0/. References 1. Abrial, J.R.: Specification language. On the Construction of Programs (1980) 2. Abrial, J.R., Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005) 3. Ackermann, L., Schönig, S., Jablonski, S.: Simulation of multiperspective declarative process models. In: Business Process Management Workshops, pp. 61–73. Springer, Berlin (2016) 4. Ackermann, L., Schönig, S., Petter, S., Schützenmeier, N., Jablonski, S.: Execution of multi-perspective declarative process models, pp. 154–172 (2018). https://doi.org/10.1007/978-3-030-02671- 4_9 5. American National Standards Institute, I.: Role-based access control. ANSI INCITS 359-2004 (2004). http://csrc.nist.gov/rbac 6. Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel- Schneider, P.F.: The Description Logics Handbook: Theory, Implementations, and Applications. Cambridge University Press, Cambridge (2003) 7. Baumgrass, A.: Deriving current state RBAC models from event logs. In: Int. Conf. on Availability, Reliability and Security, pp. 667–672 (2011) 8. Bertino, E., Ferrari, E.: Data security. In: COMPSAC, pp. 228–239 (1998) 9. Bertino, E., Ferrari, E., Atluri, V.: The specification and enforcement of authorization constraints in workflow management systems. ACM Trans. Inf. Syst. Secur. 2, 65–104 (1999) 10. Bjorner, D., Jones, CB, et al.: The Vienna development method: the meta-language (1978) 11. Bose, J.C., Maggi, F.M., van der Aalst, W.: Enhancing declare maps based on event correlations. BPM 8094, 97–112 (2013) 12. Burattin, A., Maggi, F.M., Sperduti, A.: Conformance checking based on multi-perspective declarative process models. Expert Syst. Appl. 65, 194–211 (2016) 13. Burattin, A., Sperduti, A., Veluscek, M.: Business models enhancement through discovery of roles. In: IEEE CIDM, pp. 103–110 (2013) 14. Caballero, H.S.G., Westenberg, M.A., Verbeek, H.M.W., van der Aalst, W.M.P.: Visual analytics for soundness verification of process models. Bus. Process Manag. Workshops 308, 744–756 (2017). https://doi.org/10.1007/978-3-319-74030-0_59 15. Cabanillas, C.: Process- and resource-aware information systems. In: Int. Conf. on Enterprise Distributed Object Computing (EDOC), pp. 1–10 (2016) 16. Cabanillas, C., Knuplesch, D., Resinas, M., Reichert, M., Mendling, J., Ruiz-Cortés, A.: RALph: A graphical notation for resource assignments in business processes. In: CAiSE, vol. 9097, pp. 53–68. Springer, Berlin (2015) 17. Cabanillas, C., Resinas, M., del Río-Ortega, A., Ruiz-Cortés, A.: Specification and automated design-time analysis of the business process human resource perspective. Inf. Syst. 52, 55–82 (2015) 18. Cabanillas, C., Resinas, M., Ruiz-Cortés, A.: A template-based approach for responsibility management in executable business processes. Enterp. Inf. Syst. 12(5), 550–586 (2018). https://doi. org/10.1080/17517575.2017.1390166 19. Cabanillas, C., del Río-Ortega, A., Resinas, M., Cortés, A.R.: CRISTAL: collection of resource-centrIc supporting tools and languages. In: BPM (Demos), pp. 51–56. CEUR-WS.org (2012) 20. Cabanillas, C., Schönig, S., Sturm, C., Mendling, J.: Mining expressive and executable resource-aware imperative process models. In: Int. Conf. on Enterprise, Business-Process and Information Systems Modeling (BPMDS), vol. 318, pp. 3–18 (2018) 21. Ciccio, C.D., Maggi, F.M., Montali, M., Mendling, J.: Resolving inconsistencies and redundancies in declarative process models. Inf. Syst. 64, 425–446 (2017). https://doi.org/10.1016/j.is.2016. 09.005 22. Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Berlin (2000) 23. Di Ciccio, C., Mecella, M.: On the discovery of declarative control flows for Artful processes. ACM Trans. Manag. Inf. Syst. 5(4), 241–2437 (2015) 24. Dumas, M., Rosa, M.L., Mendling, J., Reijers, H.A.: Fundamentals of Business Process Management, 2nd edn. Springer, Berlin (2018) 123