A Survey on Time-aware Business Process Modeling
---
paper_title: Formal verification of business processes with temporal and resource constraints

paper_content:

The correctness of business process models is critical for IT system development. The properties of business processes need to be analyzed when they are designed. In particular, business processes usually have various constraints on time and resources, which may cause serious problems like bottlenecks and deadlocks. In this paper, we propose an approach based on the model checking technique for verifying business process models with temporal and resource constraints. First, we extend Business Process Modeling Notation (BPMN) to handle these constraints. Then, we provide a mapping of the business process models described with this extended BPMN onto timed automata that can be verified by the UPPAAL model checker. This approach helps to eliminate various problems with time and resources in the early phase of development, and enables the quality assurance of business process models.
---
paper_title: Representation, Verification, and Computation of Timed Properties in Web

paper_content:

In this paper we address the problem of qualitative and quantitative analysis of timing aspects of Web service compositions defined as a set of BPEL4WS processes. We introduce a formalism, called Web Service Timed State Transition Systems (WSTTS), to capture the timed behavior of the composite web services. We also exploit an interval temporal logic to express complex timed assumptions and requirements on the system’s behavior. Building on top of this formalization, we provide techniques and tools for modelchecking BPEL4WS compositions against time-related requirements. We also present a symbolic algorithm that can be used to compute duration bounds of behavioral intervals that satisfy such requirements. We perform a preliminary experimental evaluation of our approach and tools with the help of an e-Government case study.
---
paper_title: A Survey on Web Services Composition

paper_content:

Due to the web services' heterogeneous nature, which stems from the definition of several XML-based standards to overcome platform and language dependence, web services have become an emerging and promising technology to design and build complex inter-enterprise business applications out of single web-based software components. To establish the existence of a global component market, in order to enforce extensive software reuse, service composition experienced increasing interest in doing a lot of research effort. This paper discusses the urgent need for service composition, the required technologies to perform service composition. It also presents several different composition strategies, based on some currently existing composition platforms and frameworks, re-presenting first implementations of state-of the-art technologies, and gives an outlook to essential future research work.
---
paper_title: Dynamic Checking and Solution to Temporal Violations in Concurrent Workflow Processes

paper_content:

Current methods that deal with concurrent workflow temporal violations only focus on checking whether there are any temporal violations. They are not able to point out the path where the temporal violation happens and thus cannot provide specific solutions. This paper presents an approach based on a sprouting graph to find out the temporal violation paths in concurrent workflow processes as well as possible solutions to resolve the temporal violations. First, we model concurrent workflow processes with time workflow net and a sprouting graph. Second, we update the sprouting graph at the checking point. Finally, we find out the temporal violation paths and provide solutions. We apply the approach in a real business scenario to illustrate its advantages: 1) It can dynamically check temporal constraints of multiple concurrent workflow processes with resource constraints; 2) it can give the path information in the workflow processes where the temporal violation happens; and 3) it can provide solution to the temporal violation based on the analysis.
---
paper_title: Conceptual Modeling of Temporal Clinical Workflows

paper_content:

The diffusion of clinical guidelines to describe the proper way to deal with patients' situations is spreading out and opens new issues in the context of modeling and managing (temporal) information about medical activities. Guidelines can be seen as processes describing the sequence of activities to be executed, and thus approaches proposed in the business context can be used to model them. In this paper, we propose a general conceptual workflow model, considering both activities and their temporal properties, and focus on the representation of clinical guidelines by the proposed model.
---
paper_title: Formal verification of business processes with temporal and resource constraints

paper_content:

The correctness of business process models is critical for IT system development. The properties of business processes need to be analyzed when they are designed. In particular, business processes usually have various constraints on time and resources, which may cause serious problems like bottlenecks and deadlocks. In this paper, we propose an approach based on the model checking technique for verifying business process models with temporal and resource constraints. First, we extend Business Process Modeling Notation (BPMN) to handle these constraints. Then, we provide a mapping of the business process models described with this extended BPMN onto timed automata that can be verified by the UPPAAL model checker. This approach helps to eliminate various problems with time and resources in the early phase of development, and enables the quality assurance of business process models.
---
paper_title: Time Petri nets for workflow modelling and analysis

paper_content:

Time management in workflow processes is crucial in determining and controlling the life cycle of business activities. In our model, a temporal interval as an execution duration is assigned to every workflow task. While the real time taken by the task is nondeterministic and unpredictable, it may be between the bounds thus specified. We extend workflow nets (WF-nets) with time intervals and call the new nets Time WF-nets (TWF-nets). Extending our previous results on timed Petri nets, we show that certain behavioural properties of workflow processes modelled in TWF-nets can be verified. Using a clinical health care process as a case study, we also illustrate the modelling of shared resources available at different times.
---
paper_title: Towards Trustworthy Composite Service Through Business Process Model Verification

paper_content:

The Business Process Modeling Notation (BPMN) is a standard for modeling business processes in the early phases of systems development. Model verification is an important means to guarantee the trustiness of composite services. The verification of model, especially the model with strict time constraints, is a challenge in the field of trust composite services. Whether a model is trustworthy depends not only on the model structure but also on quantitative properties such as time properties. In this paper, we propose a mapping from BPMN to time Petri nets, and use the verification techniques on the basis. The algorithm we present can be used to check the model structure and the time choreography.
---
paper_title: Controllability in Temporal Conceptual Workflow Schemata

paper_content:

Workflow technology has emerged as one of the leading technologies in modelling, redesigning, and executing business processes. Currently available workflow management systems (WfMS ) and research prototypes offer a very limited support for the definition, detection, and management of temporal constraints over business processes. In this paper, we propose a new advanced workflow conceptual model for expressing time constraints in business processes and, in particular, we introduce and discuss the concept of controllability for workflow schemata and its evaluation at process design time. Controllability refers to the capability of executing a workflow for any possible duration of tasks. Since in several situations durations of tasks cannot be decided by WfMSs , even tough the minimum and the maximum durations for each task are known, checking controllability is stronger than verifying the consistency of the workflow temporal constraints.
---
paper_title: A relative timed semantics for BPMN

paper_content:

We describe a relative-timed semantic model for Business Process Modelling Notation (BPMN). We define the semantics in the language of Communicating Sequential Processes (CSP). This model augments our untimed model by introducing the notion of relative time in the form of delays chosen non-deterministically from a range. We illustrate the application by an example. We also show some properties relating the timed semantics and BPMN's untimed process semantics by exploiting CSP refinement. Our timed semantics allows behavioural properties of BPMN diagrams to be mechanically verified via automatic model-checking as provided by the FDR tool.
---
paper_title: The tool TINA – Construction of abstract state spaces for petri nets and time petri nets

paper_content:

In addition to the graphic-editing facilities, the software tool Tina proposes the construction of a number of representations for the behaviour of Petri nets or Time Petri nets. Various techniques are used to extract views of the behaviour of nets, preserving certain classes of properties of their state spaces. For Petri nets, these abstractions help prevent combinatorial explosion, relying on so-called partial order techniques such as covering steps and/or persistent sets. For Time Petri nets, which have, in general, infinite state spaces, they provide a finite symbolic representation of their behaviour in terms of state classes.
---
paper_title: Timed modelling and analysis in Web service compositions

paper_content:

In this paper we present an approach for modelling and analyzing time-related properties of Web service compositions defined as a set of BPEL4WS processes. We introduce a formalism, called Web service timed state transition systems (WSTTS), to capture the timed behavior of the composite Web services. We also exploit an interval temporal logic to express complex timed assumptions and requirements on the system's behavior. Building upon of this formalization, we provide techniques and tools for model checking BPEL4WS compositions against time-related requirements. We perform a preliminary experimental evaluation of our approach and tools with the help of the e-government case study.
---
paper_title: On Temporal Abstractions of Web Service Protocols

paper_content:

Web services are increasingly gaining acceptance as a framework for facilitatingapplication-to-application interactions within and across enterprises. They pro-videabstractionsandtechnologiesforexposingenterpriseapplicationsasservicesand make them accessible programmatically through standardized interfaces.However, tools supporting service development today provide little support forhigh level modeling and analysis of abstractions at higher level of services stack,and in particular there is little support for protocol modeling and management.We believe that indeed protocol modeling and management will be key in sup-porting Web service development and interaction, and that developing formalmodels and a protocolalgebra will have a positive impact similar to the one thatthe relational model and the relational algebra had in database technology.Whendeveloping ourframeworkfor serviceprotocolsmodeling, analysis,andmanagement [1,2], we identiﬁed the need for representing temporal abstractionsin protocol descriptions. In particular, our analysis of the characteristics and re-quirements of service protocols in terms of description languages, we found that,inadditiontomessagechoreographyconstraints,protocolspeciﬁcationlanguagesneed to cater for time-sensitive conversations(i.e., conversationsthat arecharac-terized by temporal constraints on when an operation must or can be invoked).For example, a protocolmay specify thatapurchase ordermessageis acceptedonly if it is received within 24 hours after a quotation has been received. In thispaper, we discuss the augmentation of business protocols with speciﬁcations oftemporal abstractions (called timed protocols). Then we motivate, through ex-amples, a need for analyzing timed protocol speciﬁcations, and speciﬁcally foridentifying if and under what conditions two services, characterized by certaintimed protocols, can interact. Technical details are given in an extended versionof this paper [3] where a formal timed business protocol model is presented andoperators that enable characterizing compatibility and replaceability classes fortimed protocols are described.
---
paper_title: Analysis and management of Web Service protocols

paper_content:

In the area of Web services and service-oriented architectures, business protocols are rapidly gaining importance and mindshare as a necessary part of Web service descriptions. Their immediate benefit is that they provide developers with information on how to write clients that can correctly interact with a given service or with a set of services. In addition, once protocols become an accepted practice and service descriptions become endowed with protocol information, the middleware can be significantly extended to better support service development, binding, and execution in a number of ways, considerably simplifying the whole service life-cycle. This paper discusses the different ways in which the middleware can leverage protocol descriptions, and focuses in particular on the notions of protocol compatibility, equivalence, and replace-ability. They characterise whether two services can interact based on their protocol definition, whether a service can replace another in general or when interacting with specific clients, and which are the set of possible interactions among two services.
---
paper_title: Representation, Verification, and Computation of Timed Properties in Web

paper_content:

In this paper we address the problem of qualitative and quantitative analysis of timing aspects of Web service compositions defined as a set of BPEL4WS processes. We introduce a formalism, called Web Service Timed State Transition Systems (WSTTS), to capture the timed behavior of the composite web services. We also exploit an interval temporal logic to express complex timed assumptions and requirements on the system’s behavior. Building on top of this formalization, we provide techniques and tools for modelchecking BPEL4WS compositions against time-related requirements. We also present a symbolic algorithm that can be used to compute duration bounds of behavioral intervals that satisfy such requirements. We perform a preliminary experimental evaluation of our approach and tools with the help of an e-Government case study.
---
paper_title: Specifying and Monitoring Temporal Properties in Web Services Compositions

paper_content:

Current Web service composition approaches and languages such as WS-BPEL do not allow to define temporal constraints in a declarative and separate way. Also it is not possible to verify if there are contradictions between the temporal constraints implemented in the composition. These limitations lead to maintainability and correctness problems. In this paper, we tackle these problems through a novel approach to temporal constraints in Web service compositions, which combines formal methods and aspect-oriented programming. In this approach, we use a powerful and expressive formal language, called XTUS-Automata, for specifying time-related properties and we introduce specification patterns that ease the definition of such constraints. The formal specifications are translated automatically into AO4BPEL aspects, which ensure the runtime monitoring of the temporal constraints. Our approach enables a declarative, separate, and verifiable specification of temporal properties and it generates automatically modular enforcement code for those properties.
---
paper_title: Towards Timed Requirement Verification for Service Choreographies

paper_content:

In this paper, we propose an approach for analyzing and validating a composition of services with respect to real time properties. We consider services defined using an extension of the Business Process Execution Language (BPEL) where timing constraints can be associated to the execution of an activity or define delays between events. The goal is to check whether a choreography of timed services satisfies given complex real time requirements. Our approach is based on a formal interpretation of timed choreographies in the Fiacre verification language that defines a precise model for the behavior of services and their timed interactions. We also rely on a logic-based language for property definition to formalize complex real-time requirements and on specific tooling for model-checking Fiacre specifications.
---
paper_title: Negotiating Deadline Constraints in Inter-organizational Logistic Systems: A Healthcare Case Study

paper_content:

Current logistics methods are more focused on strategic goals and do not deal with short term objectives, such as, reactivity and real-time constraints. Automated logistics management systems tend to facilitate information sharing between companies, in order to support cooperative strategies, improve productivity, control service quality and reduce administrative costs. In this paper, we discuss the application of Inter-Organizational Workflows (IOW) for automating logistic procedures in a collaborative context. A case study of healthcare process is presented, and focuses on the negotiations aspects of temporal constraints in critical situations. We show how our proposed temporal extension of the CoopFlow approach, brings advantages to automating logistics operational procedures, by providing real-time data knowledge and decision routing for the case of emergency healthcare.
---
paper_title: Temporal Consistency of View Based Interorganizational Workflows

paper_content:

Interorganizational workflows are a major step in automating B2B electronic commerce and to support collaborations of organizations on the technical level. Process views are an important conceptual modelling approach for interorganizational workflows as they allow interaction and communication while internal and private parts of the process can be hidden. However, it is essential to guarantee that an interorganizational workflow is free of conflicts and the overall quality assurances of the whole workflow can be achieved. This paper proposes an approach for checking temporal consistency of interorganizational workflows crossing boundaries of organizations.
---
paper_title: Temporal Conformance of Federated Choreographies

paper_content:

Web service composition is a new way for implementing business processes. In particular, a choreography supports modeling and enactment of interorganizational business processes consisting of autonomous organizations. Temporal constraints are important quality criteria. We propose a technique for modeling temporal constraints in choreographies and orchestrations, checking whether the orchestrations satisfy the temporal constraints of a choreography and compute internal deadlines for the activities in an interorganizational workflow.
---
paper_title: Satisfaction and coherence of deadline constraints in inter-organizational workflows

paper_content:

The integration of time constraints in Inter-Organizational Workflows (IOWs) is an important issue in the workflow research field. Since each partner exposes a limited version of his business process, some information is kept hidden and not visible to all partners. The inter-enterprise business process, however, is obtained by joining all activities and control flows that have relevant roles within the context of the global operation. It should be noted that this composition process does not intrinsically guarantee the satisfaction of any critical deadline constraints that may be imposed by the partners. Obviously, expressing and satisfying time deadlines is important for modern business processes that need to be optimized for efficiency and extreme competitiveness. In this paper, we propose a temporal extension to CoopFlow, an existing approach for designing and modeling IOW, based on Time Petri Net models. A method for expressing and publishing sensible time deadlines, by the partners, is given. We also give a systematic method assuring the verification and the consistency of the published time constraints within the context of the global business process, while maintaining the core advantage of CoopFlow, that each partner can keep the critical part of his business process private.
---
paper_title: Dynamic Checking and Solution to Temporal Violations in Concurrent Workflow Processes

paper_content:

Current methods that deal with concurrent workflow temporal violations only focus on checking whether there are any temporal violations. They are not able to point out the path where the temporal violation happens and thus cannot provide specific solutions. This paper presents an approach based on a sprouting graph to find out the temporal violation paths in concurrent workflow processes as well as possible solutions to resolve the temporal violations. First, we model concurrent workflow processes with time workflow net and a sprouting graph. Second, we update the sprouting graph at the checking point. Finally, we find out the temporal violation paths and provide solutions. We apply the approach in a real business scenario to illustrate its advantages: 1) It can dynamically check temporal constraints of multiple concurrent workflow processes with resource constraints; 2) it can give the path information in the workflow processes where the temporal violation happens; and 3) it can provide solution to the temporal violation based on the analysis.
---
paper_title: Negotiating Deadline Constraints in Inter-organizational Logistic Systems: A Healthcare Case Study

paper_content:

Current logistics methods are more focused on strategic goals and do not deal with short term objectives, such as, reactivity and real-time constraints. Automated logistics management systems tend to facilitate information sharing between companies, in order to support cooperative strategies, improve productivity, control service quality and reduce administrative costs. In this paper, we discuss the application of Inter-Organizational Workflows (IOW) for automating logistic procedures in a collaborative context. A case study of healthcare process is presented, and focuses on the negotiations aspects of temporal constraints in critical situations. We show how our proposed temporal extension of the CoopFlow approach, brings advantages to automating logistics operational procedures, by providing real-time data knowledge and decision routing for the case of emergency healthcare.
---
paper_title: Temporal Consistency of View Based Interorganizational Workflows

paper_content:

Interorganizational workflows are a major step in automating B2B electronic commerce and to support collaborations of organizations on the technical level. Process views are an important conceptual modelling approach for interorganizational workflows as they allow interaction and communication while internal and private parts of the process can be hidden. However, it is essential to guarantee that an interorganizational workflow is free of conflicts and the overall quality assurances of the whole workflow can be achieved. This paper proposes an approach for checking temporal consistency of interorganizational workflows crossing boundaries of organizations.
---
paper_title: Conceptual Modeling of Temporal Clinical Workflows

paper_content:

The diffusion of clinical guidelines to describe the proper way to deal with patients' situations is spreading out and opens new issues in the context of modeling and managing (temporal) information about medical activities. Guidelines can be seen as processes describing the sequence of activities to be executed, and thus approaches proposed in the business context can be used to model them. In this paper, we propose a general conceptual workflow model, considering both activities and their temporal properties, and focus on the representation of clinical guidelines by the proposed model.
---
paper_title: Formal verification of business processes with temporal and resource constraints

paper_content:

The correctness of business process models is critical for IT system development. The properties of business processes need to be analyzed when they are designed. In particular, business processes usually have various constraints on time and resources, which may cause serious problems like bottlenecks and deadlocks. In this paper, we propose an approach based on the model checking technique for verifying business process models with temporal and resource constraints. First, we extend Business Process Modeling Notation (BPMN) to handle these constraints. Then, we provide a mapping of the business process models described with this extended BPMN onto timed automata that can be verified by the UPPAAL model checker. This approach helps to eliminate various problems with time and resources in the early phase of development, and enables the quality assurance of business process models.
---
paper_title: Temporal Conformance of Federated Choreographies

paper_content:

Web service composition is a new way for implementing business processes. In particular, a choreography supports modeling and enactment of interorganizational business processes consisting of autonomous organizations. Temporal constraints are important quality criteria. We propose a technique for modeling temporal constraints in choreographies and orchestrations, checking whether the orchestrations satisfy the temporal constraints of a choreography and compute internal deadlines for the activities in an interorganizational workflow.
---
paper_title: Towards Trustworthy Composite Service Through Business Process Model Verification

paper_content:

The Business Process Modeling Notation (BPMN) is a standard for modeling business processes in the early phases of systems development. Model verification is an important means to guarantee the trustiness of composite services. The verification of model, especially the model with strict time constraints, is a challenge in the field of trust composite services. Whether a model is trustworthy depends not only on the model structure but also on quantitative properties such as time properties. In this paper, we propose a mapping from BPMN to time Petri nets, and use the verification techniques on the basis. The algorithm we present can be used to check the model structure and the time choreography.
---
paper_title: Representation, Verification, and Computation of Timed Properties in Web

paper_content:

In this paper we address the problem of qualitative and quantitative analysis of timing aspects of Web service compositions defined as a set of BPEL4WS processes. We introduce a formalism, called Web Service Timed State Transition Systems (WSTTS), to capture the timed behavior of the composite web services. We also exploit an interval temporal logic to express complex timed assumptions and requirements on the system’s behavior. Building on top of this formalization, we provide techniques and tools for modelchecking BPEL4WS compositions against time-related requirements. We also present a symbolic algorithm that can be used to compute duration bounds of behavioral intervals that satisfy such requirements. We perform a preliminary experimental evaluation of our approach and tools with the help of an e-Government case study.
---
paper_title: Specifying and Monitoring Temporal Properties in Web Services Compositions

paper_content:

Current Web service composition approaches and languages such as WS-BPEL do not allow to define temporal constraints in a declarative and separate way. Also it is not possible to verify if there are contradictions between the temporal constraints implemented in the composition. These limitations lead to maintainability and correctness problems. In this paper, we tackle these problems through a novel approach to temporal constraints in Web service compositions, which combines formal methods and aspect-oriented programming. In this approach, we use a powerful and expressive formal language, called XTUS-Automata, for specifying time-related properties and we introduce specification patterns that ease the definition of such constraints. The formal specifications are translated automatically into AO4BPEL aspects, which ensure the runtime monitoring of the temporal constraints. Our approach enables a declarative, separate, and verifiable specification of temporal properties and it generates automatically modular enforcement code for those properties.
---
paper_title: Satisfaction and coherence of deadline constraints in inter-organizational workflows

paper_content:

The integration of time constraints in Inter-Organizational Workflows (IOWs) is an important issue in the workflow research field. Since each partner exposes a limited version of his business process, some information is kept hidden and not visible to all partners. The inter-enterprise business process, however, is obtained by joining all activities and control flows that have relevant roles within the context of the global operation. It should be noted that this composition process does not intrinsically guarantee the satisfaction of any critical deadline constraints that may be imposed by the partners. Obviously, expressing and satisfying time deadlines is important for modern business processes that need to be optimized for efficiency and extreme competitiveness. In this paper, we propose a temporal extension to CoopFlow, an existing approach for designing and modeling IOW, based on Time Petri Net models. A method for expressing and publishing sensible time deadlines, by the partners, is given. We also give a systematic method assuring the verification and the consistency of the published time constraints within the context of the global business process, while maintaining the core advantage of CoopFlow, that each partner can keep the critical part of his business process private.
---
paper_title: Towards Timed Requirement Verification for Service Choreographies

paper_content:

In this paper, we propose an approach for analyzing and validating a composition of services with respect to real time properties. We consider services defined using an extension of the Business Process Execution Language (BPEL) where timing constraints can be associated to the execution of an activity or define delays between events. The goal is to check whether a choreography of timed services satisfies given complex real time requirements. Our approach is based on a formal interpretation of timed choreographies in the Fiacre verification language that defines a precise model for the behavior of services and their timed interactions. We also rely on a logic-based language for property definition to formalize complex real-time requirements and on specific tooling for model-checking Fiacre specifications.
---
paper_title: Constraint-based workflow models: Change made easy

paper_content:

The degree of flexibility of workflow management systems heavily influences the way business processes are executed. Constraint-based models are considered to be more flexible than traditional models because of their semantics: everything that does not violate constraints is allowed. Although constraint-based models are flexible, changes to process definitions might be needed to comply with evolving business domains and exceptional situations. Flexibility can be increased by run-time support for dynamic changes - transferring instances to a new model - and ad-hoc changes - changing the process definition for one instance. In this paper we propose a general framework for a constraint-based process modeling language and its implementation. Our approach supports both ad-hoc and dynamic change, and the transfer of instances can be done easier than in traditional approaches.
---
paper_title: Controllability in Temporal Conceptual Workflow Schemata

paper_content:

Workflow technology has emerged as one of the leading technologies in modelling, redesigning, and executing business processes. Currently available workflow management systems (WfMS ) and research prototypes offer a very limited support for the definition, detection, and management of temporal constraints over business processes. In this paper, we propose a new advanced workflow conceptual model for expressing time constraints in business processes and, in particular, we introduce and discuss the concept of controllability for workflow schemata and its evaluation at process design time. Controllability refers to the capability of executing a workflow for any possible duration of tasks. Since in several situations durations of tasks cannot be decided by WfMSs , even tough the minimum and the maximum durations for each task are known, checking controllability is stronger than verifying the consistency of the workflow temporal constraints.
---
paper_title: A relative timed semantics for BPMN

paper_content:

We describe a relative-timed semantic model for Business Process Modelling Notation (BPMN). We define the semantics in the language of Communicating Sequential Processes (CSP). This model augments our untimed model by introducing the notion of relative time in the form of delays chosen non-deterministically from a range. We illustrate the application by an example. We also show some properties relating the timed semantics and BPMN's untimed process semantics by exploiting CSP refinement. Our timed semantics allows behavioural properties of BPMN diagrams to be mechanically verified via automatic model-checking as provided by the FDR tool.
---

Title: A Survey on Time-aware Business Process Modeling

Section 1: INTRODUCTION
Description 1: Provide an introduction to the context of business process modeling, the importance of addressing temporal constraints in inter-organisational business processes, and the goals of this paper.

Section 2: OVERVIEW ON THE EXISTING TEMPORAL CONSTRAINTS SPECIFICATION METHODS
Description 2: Offer a classification of the existing models for specifying temporal constraints in business processes, including workflows, web service composition, and inter-organisational domain.

Section 3: Temporal constraints in the workflow research area
Description 3: Detail the approaches to specifying and verifying temporal constraints within the workflow research area, including notable methods and their limitations.

Section 4: Temporal constraints in web service composition research field
Description 4: Discuss the methods for temporal constraint specification and verification in the web service composition research field, highlighting key approaches and their strengths and limitations.

Section 5: Temporal constraints in the inter-organisational research field
Description 5: Explain the efforts and methods used to specify and verify temporal constraints in inter-organisational business processes, addressing challenges and limitations.

Section 6: EVALUATION AND DISCUSSION
Description 6: Provide an evaluation of the surveyed methods, highlight the effectiveness of different approaches, and discuss observed strengths, weaknesses, and gaps in current research.

Section 7: RESEARCH CHALLENGES AND CONCLUSION
Description 7: Summarize the key findings and insights from the survey, outline the major research challenges that need to be addressed, and conclude with remarks on future directions in time-aware business process modeling.