Stefan Dziwok

Christian Heinzemann
email: [stefan.dziwok|christian.heinzemann]@uni-paderborn.de

Matthias Tichy
email: tichy@chalmers.se

Real-Time Coordination Patterns for Advanced Mechatronic Systems

Keywords: Advanced Mechatronic Systems, Patterns, Coordination, Communication, Real-Time, MechatronicUML

Innovation in today's mechanical systems is often only possible due to the embedded software. Particularly, the software connects previously isolated systems resulting in, so-called, advanced mechatronic systems. Mechatronic systems are often employed in a safety-critical context, where hazards that are caused by faults in the software have to be prevented. Preferably, this is achieved by already avoiding these faults during development. A major source of faults is the complex coordination between the connected mechatronic systems. In this paper, we present Real-Time Coordination Patterns for advanced mechatronic systems. These patterns formalize proven communication protocols for the coordination between mechatronic systems as reusable entities. Furthermore, our approach exploits the patterns in the decomposition of the system to enable a scalable formal verification for the detection of faults. We illustrate the patterns with examples from different case studies.

Introduction

Mechanical engineering has a long tradition in sustained development of innovation, e.g., innovation in cars in the last century. However, in the last decades, software is the driving force for innovation in mechanical engineering as, e.g., in the automotive domain [START_REF] Scharnhorst | Autosar -challenges and achievements[END_REF]. Modern mechanical systems are developed by experts from several engineering disciplines: mechanical engineering, electrical engineering, control engineering, and software engineering. These systems are called mechatronic systems. Mechatronic systems often operate in a safety-critical context where failures can lead to death or serious injury to people.

Furthermore, previously isolated systems increasingly form systems of systems where each autonomous part communicate with each other by means of complex message exchange protocols [START_REF] Schäfer | The Challenges of Building Advanced Mechatronic Systems[END_REF] in an ad-hoc manner. This results in very complex systems. These trends make the development of advanced mechatronic systems a big challenge. Thus, appropriate development approaches have to be utilized and rigorously followed. Particularly, the software has to be subject of rigorous verification and validation activities.

Figure 1 shows three advanced mechatronic systems developed at the University of Paderborn in the last couple of years. On the left, two autonomous shuttles of the RailCab systems are shown. RailCab shuttles are autonomous railway vehicles which combine the flexibility of individual transport with the energy efficiency of public transport systems. They save energy by forming convoys which reduce the air resistance. In the middle, two miniature robots called BeBots are shown. BeBots form ad-hoc networks in order to jointly execute tasks. The robots can collectively agree on taking different roles to achieve the common task. On the right, two cooperating robots are shown which play pingpong. They do so without any external global camera system but instead rely on the timely exchange of position, velocity, and trajectory of the batted ball.

In all three advanced mechatronic systems, coordination plays an important role because they consist of independent, communicating actors (e.g., autonomous mechatronic systems), who join their efforts towards mutually defined goals (cf. [START_REF]A report by NSF-IRIS review panel for research on coordination theory and technology[END_REF]). For example, the communication actors decide on a common strategy (e.g., activating the convoy) or they decide on a master who delegates tasks to the slaves. These coordination aspects require sophisticated coordination protocols.

We developed the coordination protocols for these systems based on the patterns presented in [START_REF] Gamma | Design Patterns: Elements of Reusable Object-Oriented Software[END_REF][START_REF] Buschmann | Pattern-Oriented Software Architecture[END_REF][START_REF] Douglass | Doing hard time: developing real-time systems with UML, objects, frameworks, and patterns[END_REF][START_REF] Douglass | Real-Time Design Patterns: Robust Scalable Architecture for Real-Time Systems[END_REF] in order to exploit the vast amount of existing experience. The patterns listed in these approaches proved to be very helpful in developing our systems. However, they lack a formal description which may lead to the introduction of errors in the application to new systems. As we focus on safety-critical mechatronic systems, a pattern approach which avoids this introduction of errors in the first place is beneficial in order to guarantee the safety of the system.

Based on that experience, we developed Real-Time Coordination Patterns which formalize coordination protocols for mechatronic systems with a particular focus on safety properties and hard real-time constraints. Furthermore, protocols that are based on these patterns enable to decompose the mechatronic system in such a way that a scalable formal verification using model checking can be employed. This is possible because of our previous work on compositional verification [START_REF] Giese | Towards the compositional verification of real-time uml designs[END_REF]. In contrast to the pattern formalism of [START_REF] Giese | Towards the compositional verification of real-time uml designs[END_REF], we further abstract from application-specific details for a better reusability, define a description format for the patterns, and have build up a catalog of patterns.

In summary, the contribution of this paper is as follows: (1) we present Real-Time Coordination Patterns as formal representation of reusable coordination protocols, (2) we present formal refinement steps which define how these patterns are applied and refined, and (3) we report on a case study in which the approach was applied to the aforementioned cooperating robots example.

Section 2 presents MechatronicUML, which is the foundation for our approach. In Section 3, we introduce Real-Time Coordination Patterns that are patterns for Real-Time Coordination Protocols. We show how these patterns are applied to new systems in Section 4. Thereafter, we present the cooperating robots case study in Section 5. Next, we distinguish our results from related work in Section 6. Finally, we conclude with an outlook on future work in Section 7.

MechatronicUML

MechatronicUML [START_REF] Becker | The Mechatron-icUML method -process, syntax, and semantics[END_REF] is a language for the model-driven design of software of advanced mechatronic systems. It follows the component-based approach where each component encapsulates a part of the software. In advanced mechatronic systems, the components that constitute the software do not work in isolation, but they have to coordinate their actions using communication for achieving the intended functionality of the system. Therefore, each component defines a set of external interaction points, which we call ports. Components can communicate via their ports if a connector connects them.

A connection between two components implies that they are able to communicate correctly. The protocol definition formally defines the message exchange and the timing constraints that the message exchange needs to adhere to. In MechatronicUML, a protocol is defined by a pair of communicating roles and a connector. We call it a Real-Time Coordination Protocol. We describe the behavior of each role with a Real-Time Statechart.

Real-Time Statecharts are an extension of UPPAAL timed automata [START_REF] Bengtsson | Timed automata: Semantics, algorithms and tools[END_REF] to support, e.g., modeling of worst-case execution times and deadlines for actions. Real-Time Statecharts especially support the specification of asynchronous messages as well as real-time constraints. In addition, Real-Time Statecharts may define variables and operations that are required for the communication. Their semantics is defined by a mapping to UPPAAL timed automata [START_REF] Giese | Real-time statechart semantics[END_REF]. Figure 2 shows an example of a Real- The protocol definition in MechatronicUML explicitly considers that a transmission of a message from sender to receiver takes time. Therefore, the connectors may receive a transmission delay. In our example, we assume a transmission delay of up to 200ms.

In many cases, the communication of the components is safety-critical, i.e., a malfunctioning communication may cause severe damage to property or human lives. For example in case of the convoy coordination, RailCabs may collide if the RailCab driving behind assumes to be in convoy mode while the RailCab driving in front does not. In convoy mode, the RailCab driving in front must notify its follower before braking. If the RailCab driving in front is not in convoy mode, it will not send the notification. Thus, we must ensure that the RailCab driving behind, i.e., the rear role of the protocol, only enters the state Convoy if the front role is in state Convoy as well. We formalize such properties using the Timed Computation Tree Logic (TCTL) [START_REF] Alur | Model-checking in dense real-time[END_REF]. Thus, the aforementioned property is formalized as AG rear.Convoy implies f ront.Convoy.

The properties are formally verified using timed model checkers like UP-PAAL [START_REF] Behrmann | A tutorial on uppaal[END_REF]. In our verification, we explicitly consider the delay of the connector as well as the case that messages may be lost, e.g., when using an unreliable transmission medium. In addition, we assume that messages are not reordered during the transmission and that they are stored in a FIFO-queue allowing only access to the first element. The protocol introduced in this section remains safe w.r.t. the specified property and free of deadlocks.

The behavior of a component constitutes from the Real-Time Statecharts of the ports. In addition, the component may provide additional internal behavior, e.g., for resolving conflicts between different ports or for providing additional operations as discussed in Section 4.

In most cases, the system under construction cannot be verified as a whole using model checking because of the state space explosion problem (the number of reachable states is often exponential in the size of the specification). To achieve a scalable formal verification, we use the compositional verification approach of [START_REF] Giese | Towards the compositional verification of real-time uml designs[END_REF]. Here, we verify each Real-Time Coordination Protocol separately before verifying each component. This is enabled by clearly separating component internal behavior and communication behavior using Real-Time Coordination Protocols.

Patterns for Real-Time Coordination Protocols

In MechatronicUML, connectors are first class entities. Therefore, the focus within the first process steps is to design the coordination and communication behavior. Based on given requirements, the developer has to specify one Real-Time Coordination Protocol per connector. While doing so, he has to ensure that it is free of faults despite hard real-time constraints, message delay and the possibility of message loss. Although the developer is able to identify faults regarding the behavior description using model checkers, removing the faults is a non trivial task. In general, specifying a Real-Time Coordination Protocol is very complex and thus, very time-consuming and error-prone. Moreover, the intention of an already existing protocol is often hard to grasp.

While modeling Real-Time Coordination Protocols for different advanced mechatronic systems, we identified that the coordination is based on recurring use-cases. This applies for the coordination between autonomous systems, but also for the coordination between components within one system. Therefore, we define general, reusable solutions for these recurring use cases (we call them Real-Time Coordination Patterns). These patterns support the developer by offering solutions that contain formal models and a comprehensive documentation. By doing so, our goal is to increase the quality of the resulting Real-Time Coordination Protocols as well as the efficiency of their development.

Real-Time Coordination Patterns

In general, a pattern within software design "provides a scheme for refining the subsystems or components of a software system, or the relationships between them. It describes a commonly recurring structure of communicating components that solves a general design problem within a particular context" [START_REF] Buschmann | Pattern-Oriented Software Architecture[END_REF].

A Real-Time Coordination Pattern describes a well-proven, reusable, and formal solution to a commonly occurring coordination problem within the domain of advanced mechatronic systems. These systems communicate under hard real-time constraints in a safety-critical environment. Hence, Real-Time Coordination Patterns are a special kind of software patterns and support inexperienced developers in specifying Real-Time Coordination Protocols. A Real-Time Coordination Pattern is defined such that it respects certain safety properties, which can be formally verified using model checkers. Moreover, if a developer defines coordination protocols based on our patterns, the system under construction can be fully verified based on our compositional verification approach [START_REF] Giese | Towards the compositional verification of real-time uml designs[END_REF].

A Real-Time Coordination Pattern abstracts from application-specific details to be reusable in different scenarios. For example, time parameters are defined instead of concrete time values. However, the correctness of a protocol depends on real-time constraints and properties of the connector (e.g., reliability) and is therefore not automatically correct for all possible time parameters and all connectors. Thus, we define the steps a developer has to execute for each pattern to get a correct protocol (see Section 4).

The Real-Time Coordination Patterns that we identified so far are collected and described within a pattern catalog [START_REF] Dziwok | A catalog for Real-Time Coordination Patterns of advanced mechatronic systems[END_REF]. Currently, the catalog consists of eight patterns. A briefly overview of those follows:

Synchronized Collaboration synchronizes the activation and deactivation of a collaboration of two roles. The pattern assumes that a safety-critical situation appears if the role, which initialized the activation, is in collaboration mode and the other role is not in collaboration mode. Therefore, the pattern ensures that this situation never happens.

Fail-Safe Delegation realizes a delegation of a task from a master role to a slave role. The slave executes the task in a certain time and answers regarding success or failure. If the execution fails, no other task may be delegated until the master ensures that the failure has been corrected. Moreover, only one delegation at a time is allowed.

Fail-Operational Delegation realizes a delegation of a task from a master role to a slave role. The slave executes the task in a certain time and answers regarding success or failure. The pattern assumes that a failure is not safetycritical, though only one delegation at a time is allowed.

Master-Slave-Assignment is used if two systems can dynamically change between one state in which they have equal rights and another state in which one is the master and the other one is the slave.

Periodic Transmission can be used to periodically transmit information from a sender to a receiver. If the receiver does not get the information within a certain time, a specified behavior must be activated to prevent a safety-critical situation.

Producer-Consumer is used when two roles shall access a safety-critical section alternately. For example, one produces goods, the other consumes them. The pattern guarantees that only one is in the critical section at the same time.

Block Execution coordinates a blocking of actions, e.g., due to safetycritical reasons.

Limit Observation is used to communicate if a certain value violates a defined limit or not.

Description Format of our Patterns

For describing our patterns, we defined a uniform description format such that a developer can understand, compare, and use our patterns more easily.

Several popular description formats for software patterns already exist [START_REF] Buschmann | Pattern-Oriented Software Architecture[END_REF][START_REF] Gamma | Design Patterns: Elements of Reusable Object-Oriented Software[END_REF]. We analyzed how well they fit to our patterns and, hence, decided to choose the format of Buschmann et al. [START_REF] Buschmann | Pattern-Oriented Software Architecture[END_REF] and adapt it to our needs.

We use all attributes of their description format except of implementation and example resolved because we propose to use code generators and resolve our example already within the other attributes. Furthermore, we divide the attribute see also into the two attributes alternative patterns and combinability because these are two different contents, which are easier to find and understand for the developer if they are separated from each other. At last, we add the attribute verification properties to explain the verification properties that must hold for the pattern.

To conclude, Real-Time Coordination Patterns are described with the following attributes: name (including a short summary), context, problem, solution, structure, behavior, verification properties, consequences, examples, variants, alternative patterns, and combinability.

Example: Synchronized Collaboration

The Real-Time Coordination Protocol Convoy Coordination (Fig. 2) is a good solution when two communicating actors have to synchronize the (de-) activation of a concrete collaboration. Therefore, we abstracted it from all its application specific details and defined the Real-Time Coordination Pattern Synchronized Collaboration (Fig. 3). We will now give a short description for this pattern. We omitted the attributes variants, alternative patterns, and combinability because of the limited space of the paper. The full description can be found within our pattern catalog [START_REF] Dziwok | A catalog for Real-Time Coordination Patterns of advanced mechatronic systems[END_REF].

Name: Synchronized Collaboration (also known as: Strategy Coordination)

This pattern synchronizes the activation and deactivation of a collaboration of two systems. The pattern assumes that a safety-critical situation appears if the system that initialized the activation is in collaboration mode and the other system is not in collaboration mode. Therefore, the pattern ensures that this situation never happens. Problem: Switching between collaboration and no collaboration adds hazards.

It may be the case that one system assumes they are working together while the other one does not think so. This must be avoided. The possibility for this problem occurrence increases, if the communication is asynchronous and the communication channel is unreliable. This patterns assumes that the safety-critical situation only occurs, if system s1 assumes they are working together and system s2 does not think so. The other way round is considered as not safety-critical.

Solution: Define a coordination protocol that enables to activate and deactivate the collaboration while it considers the given problems. The systems act with different roles: System s1 is the master and system s2 is the slave. The master initiates the activation and the deactivation. The activation is a proposal so that the slave can decide whether the collaboration is possible and useful. The deactivation is a direct command so that the master can deactivate the collaboration as soon as it is no longer useful.

Structure:

The pattern consists of the two roles master and slave and a connector (Fig. 3). The master may send the messages activationProposal and deactivation to the slave. The slave may send the messages activationAccepted and activationRejected to the master. The time parameter of the master role is $timeout, the time parameter of slave role is $eval-time. The connector may lose messages. The delay for sending a message is defined by the time parameters $delay-min and $delay-max.

Behavior: The Real-Time Statecharts of both roles are shown in Fig. 3. A short description is as follows: First, the collaboration is in both roles inactive. The slave is passive and has to wait for the master to decide to send a proposal for activating the collaboration. In this case, the slave has a certain time to answer if he accepts or rejects the proposal. If the slave rejects, the collaboration will remain inactive. If the slave accepts, he activates the collaboration and informs the master so that he also activates the collaboration. If the master receives no answer in a certain time (e.g. because the answer of the slave got lost), he cancels its waiting and may send a new proposal. Only the master can decide to deactivate the collaboration. He informs the slave so that he also deactivates it.

Verification Properties: There will never be a deadlock within the protocol: AG not deadlock. If the master is in state CollaborationActive, then the slave must always be in state CollaborationActive: AG master.CollaborationActive implies slave.CollaborationActive.

Consequences: Both roles must have a pre-defined behavior when the collaboration is active or inactive. At run-time, the behavior must be adapted accordingly, because master and slave decide on this defined behavior to activate or deactivate the collaboration. Moreover, the slave cannot deactivate the collaboration.

Examples: Two RailCabs are driving on the same track. The rear RailCab wants to create a convoy to take advantage of the slipstream. However, it has to drive with a small gap to the front RailCab. Therefore, the rear RailCab cannot avoid a collision, if the front RailCab brakes hard without informing the rear RailCab. Synchronized Collaboration enables to build a secure convoy if the rear RailCab acts as the master and the front RailCab acts as the slave and the rear RailCab only drives with a small gap as long as the convoy collaboration is active.

Developing Advanced Mechatronic Systems using Real-Time Coordination Patterns

In this section, we illustrate how a developer may use the provided Real-Time Coordination Patterns during the development of a concrete system. The general process for each pattern is depicted in Fig. 4. The developer starts with the requirements for the coordination protocol. Based on these requirements, the developer selects a Real-Time Coordination Pattern which suites the requirements in Step 1. In Step 2, the developer may adapt the Real-Time Coordination Pattern to the concrete domain of the system under development. We call this an application-specific adaptation which we describe in detail in Section 4.1. At the end of Step 2, we perform model checking to ensure that all verification properties are met. The result is a Real-Time Coordination Protocol. In Step 3, this protocol is applied to the components of the system to specify their communication. That requires an implementation-specific refinement which we introduce in Section 4.2. The correctness of the refinement is ensured by a refinement check. Finally, the result is a MechatronicUML model of the system under construction.

Application-specific Adaptation

Real-Time Coordination Patterns are intended to be reused in different applications that operate in different domains. Consequently, they abstract from all application-specific details, e.g., concrete timing information, and use generic names for states and messages. The Real-Time Coordination Pattern Synchronized Collaboration in Fig. 3 gives an example. When applying a Real-Time Coordination Pattern to an application of a specific domain, the developer needs to specify concrete values for all time parameters and the properties of the connector. That includes message delay, consideration of message loss, and the concrete implementation variant of a buffer.

Besides the mandatory steps described above, the developer may adapt the Real-Time Coordination Pattern to the application. This adaptation includes:

(1) renaming elements (protocol, roles, states, messages, clocks, variables, operations) to concretize their application-specific meaning, (2) adding new message parameters, (3) changing the state hierarchy (increasing or flattening), ( 4) adding variables and clocks, and ( 5) splitting transitions into several transitions with intermediate states. Further adaptations, e.g., adding entirely new states, transitions, and messages, change the solution provided by the pattern significantly. Then, it cannot be assured that the verification properties are still meaningful and sufficient for guaranteeing the safety of the resulting protocol.

After executing all adaptation steps, we obtain a Real-Time Coordination Protocol for the specific application. Given the essential timing information, we can perform model checking on the Real-Time Coordination Protocol to ensure that it satisfies all verification properties specified in the pattern definition. The model checking task is carried out by a timed model checker, e.g., UPPAAL [START_REF] Behrmann | A tutorial on uppaal[END_REF].

Implementation-specific Refinement

In this step, we assign the resulting Real-Time Coordination Protocols to the components of the system under construction to define their communication. The assignment of a Real-Time Coordination Protocol to a component requires to integrate it with the internal behavior of the component and to resolve conflicts or dependencies between several protocols. As an example for such dependencies, consider the RailCab system. A RailCab may only enter the convoy mode if it is correctly registered at a track side control unit. The registration is performed by another Real-Time Coordination Protocol.

The assignment of a protocol to a concrete component might also require the implementation of component-specific operations. In our example, the front role of the convoy coordination protocol needs to be extended by an implementation that determines whether a convoy is useful or not. The changes which are applied to a Real-Time Coordination Protocol must not invalidate the verified safety and liveness properties which is achieved by a refinement.

The changes which we allow for the implementation-specific refinement are so-called lightweight changes only. The lightweight changes that we support are:

(1) adding deadlines to transitions, (2) adding actions to states and transitions, (3) adding synchronizations, and (4) splitting transitions into a sequence of states and transitions. We allow to add invariants to the states and time guards to the transition that originate from splitting transitions.

After applying the lightweight changes, we need to verify that they have been applied correctly. Model checking the whole Real-Time Coordination Protocol, again, is costly and not necessary in this case. Instead, we only need to verify that each role of the Real-Time Coordination Protocol has been refined correctly. That requires the refined role to be checked against the role obtained after application-specific adaptation. If the refinement has been done correctly, the Real-Time Coordination Protocol with the refined role fulfills all verified properties. In [START_REF] Heinzemann | Reusing dynamic communication protocols in selfadaptive embedded component architectures[END_REF], we have shown that checking for correct refinement of a single role is more efficient than a repetition of the verification of the whole Real-Time Coordination Protocol. Formal definitions for refinements of timed automata have been introduced in [START_REF] Tripakis | Analysis of timed systems using time-abstracting bisimulations[END_REF] and [START_REF] Heinzemann | Reusing dynamic communication protocols in selfadaptive embedded component architectures[END_REF].

Case Study: Cooperating Robots

After we collected a set of eight Real-Time Coordination Patterns, we started a case study to answer the following questions: (1) Are our patterns reusable? (2) Is our pattern catalog including our pattern description format helpful? (3) Is our proposed process after selecting a pattern appropriate?

Our new case study were the cooperating robots (Fig. 1 (iii)) that have to play ping-pong using different squash balls without needing a camera to trace the ball. Instead, the two fully independent robots use contact sensors to trace the ball and use communication to inform each other. Among others, the following requirements were defined: (1) Initially, one of both robots receives the ball. ( 2) Balls with different properties should be supported. [START_REF] Becker | The Mechatron-icUML method -process, syntax, and semantics[END_REF] The robot that initially receives the ball, first has to juggle it alone to identify the ball properties. [START_REF] Behrmann | A tutorial on uppaal[END_REF] The game is restricted to a maximum of 30s. [START_REF] Bengtsson | Timed automata: Semantics, algorithms and tools[END_REF] The robot that initially receives the ball has to ensure that the other robot must be ready and knows the ball properties before the ball is hit to it. Otherwise, the other robot cannot hit the squash ball correctly or will not perform a hit at all. Both problems lead to an unwanted behavior.

A computer science student, who has basic knowledge regarding model-driven development, carried out the design of the MechatronicUML model and especially the modeling of the coordination and communication. We gave him a detailed introduction of MechatronicUML, our existing case studies including the documentation and our pattern catalog. Afterward, we defined the requirements of the application. The student worked primarily on his own except some questions of him regarding the given documents. As a result, the student defined four Real-Time Coordination Protocols to realize the robot-to-robot communication. Two are based on Real-Time Coordination Patterns, namely: Master-Slave-Assignment, and Synchronized Collaboration. One of the two non pattern-based protocols is a good solution for an alternating transmission. Thus, we want to abstract it to a new pattern. Regarding the internal communication within each robot, the student used just three protocols to define all 13 internal connectors. Two of them were patterns and the third is a good candidate for a new pattern.

For example, the student selected the pattern Synchronized Collaboration to synchronize the start and the end of the game between the robots while ensuring that the robot that initially receives the ball may only start the game if the other robot is aware of that and does know the ball properties. He adapted the pattern to the Real-Time Coordination Protocol Game Coordination (Fig. 5), e.g., he defined the time variables, renamed some elements, and added a new invariant for state Gaming of statechart ping to restrict the length of the game. The model checker did not found any errors within the resulting protocol. Therefore, the student assigned the protocol to a connector and refined it by synchronization channels to integrate it with the internal behavior of the connected components.

Concluding, the student successfully reused our Real-Time Coordination Patterns, adapted them to Real-Time Coordination Protocols, and reused these protocols, but with different refinement-variants. Regarding the pattern catalog, the student found the description and its format fitting and on the correct level of abstraction. The student was able to carry out the steps of our proposed process, which defined the application-specific adaptation and the implementationspecific refinement, in an efficient manner.

Patterns regarding the coordination and communication between classes, components, and systems already exist and were a great help for defining our own patterns. However, most of them only illustrate the communication informally using sequence diagrams. If at all, they only define simple timing behavior. Examples for these are the patterns Chain of Responsibility, Command, and Observer by Gamma et al. [START_REF] Gamma | Design Patterns: Elements of Reusable Object-Oriented Software[END_REF] and the patterns Master-Slave, Forwarder-Receiver, Client-Dispatcher-Server, and Publisher-Subscriber by Buschmann et al [START_REF] Buschmann | Pattern-Oriented Software Architecture[END_REF]. In contrast to these pattern systems, we formally specify the coordination using Real-Time Statecharts. Using them, the messages a communication participant may receive and send depend on its current state and on additional real-time constraints.

Real-Time Coordination Patterns are protocol patterns for the domain of advanced mechatronic systems. Other domains-specific languages also defined patterns for communication, e.g., in the domain of multi-agent-system. For example, AgentUML is a modeling language to specify agent interaction protocols [START_REF] Bauer | Agent uml: A formalism for specifying multiagent interaction[END_REF]. For such protocols the Foundation of Intelligent Physical Agents defined socalled protocol templates, e.g., the Propose Interaction Protocol, which proposes an interaction that can be accepted or rejected. Agent interaction protocols combine sequence diagrams with the notion of state diagrams, though they do not support real-time constraints that are mandatory in our domain of advanced mechatronic systems. Douglass [START_REF] Douglass | Doing hard time: developing real-time systems with UML, objects, frameworks, and patterns[END_REF][START_REF] Douglass | Real-Time Design Patterns: Robust Scalable Architecture for Real-Time Systems[END_REF] defined real-time design patterns for the collaboration between components, e.g., Watchdog. The behavior is described by UML state machines including useful real-time constraints and message exchanges. However, our behavior is described using Real-Time Statecharts, which are more expressive (e.g., they can define how long a state may be active). Furthermore, Douglass does not define how a developer may adapt this pattern for his application.

We define our patterns in a formal way and describe the process of their subsequent adaptation and refinement. Taibi et al. [START_REF]Design Patterns Formalization Techniques[END_REF] describe several approaches regarding the formalization of patterns and their subsequent refinement, but they do not focus on coordination protocols of advanced mechatronic systems.

In contrast to the mentioned related work, our patterns consider safetycritical situations (in the domain of advanced mechatronic systems) that must not happen. They offer a solution which ensures that these situations never appear. Furthermore, we define a process that preserves these characteristics during the application of the pattern.

Conclusions and Future Work

In this paper, we proposed patterns for Real-Time Coordination Protocols, which we call Real-Time Coordination Patterns. They describe safety-critical problems that appear when a developer designs the coordination through communication between advanced mechatronic systems. Furthermore, our patterns suggest a solution that is reusable in different applications and specifies the behavior in such a way that it can be proven regarding safety-critical requirements. We used a real application example to explain the need of our patterns. Moreover, we defined how developers should develop the coordination when they use our patterns. We identified eight patterns through several case studies and were able to reuse them in a new case study. We mainly differ from existing pattern systems, because we specify safety-critical requirements that our patterns ensure.

Our patterns may help developers to increase the quality of coordination protocols for advanced mechatronic systems and to improve the efficiency developing them.

Several topics require further investigations: [START_REF] Alur | Model-checking in dense real-time[END_REF] We have to carry out a comprehensive evaluation to confirm our results. [START_REF] Bauer | Agent uml: A formalism for specifying multiagent interaction[END_REF] We want to examine more case studies for advanced mechatronic systems to identify additional Real-Time Coordination Patterns. [START_REF] Becker | The Mechatron-icUML method -process, syntax, and semantics[END_REF] In this paper we only introduced patterns for a one-to-one communication. However, Real-Time Coordination Protocols for one-to-many and many-to-many communication also exist. Therefore, we want to extend our catalog with such patterns. (4) To enable a developer to improve the search for an appropriate pattern, we are currently designing an ontology to store our patterns within the Semantic Web as suggested in [START_REF] Henninger | Software pattern communities: Current practices and challenges[END_REF]. Afterward, we want to enable the developer to search after patterns within our MechatronicUML modeling tool Fujaba Real-Time Tool Suite. (5) Our patterns have many variants. Therefore, we want to define a feature model for each pattern so that a developer may select a feature configuration and the system automatically constructs the corresponding structure, behavior model, and verification properties.

Fig. 1 .

 1 Fig. 1. Examples for advanced mechatronic systems

Fig. 3 .

 3 Fig. 3. Structure and behavior of Real-Time Coordination Pattern Synchronized Collaboration

Fig. 4 .

 4 Fig. 4. Process for Developing with Design Patterns

Fig. 5 .

 5 Fig. 5. Real-Time Coordination Protocol Game Coordination that is adapted and refined for the coordination of the cooperating robots

  Time Coordination Protocol namedConvoy Coordination which is used for coordinating a convoy of RailCabs. The behavior is as follows: Initially, both Real-Time Statecharts are in the states NoConvoy/Default. Then, the rear RailCab, i.e., the RailCab driving behind, may switch to state Waiting by sending an asynchronous message convoyProposal to the front RailCab to initiate the convoy build-up. The front RailCab receives this message and switches to EvaluateProposal. In this state, the front RailCab decides RailCabs share the same route. For this reason, the rear RailCab sends the ID of its destination as a parameter of the convoyProposal. Within 599ms, either the front RailCab rejects the proposal by sending convoyProposalRejected or it accepts by sending startConvoy. In the first case, both Real-Time Statecharts return to the Default states. In the second case, both Real-Time Statecharts switch to state convoy. For avoiding a deadlock in the rear RailCab, it specifies a time out in state Waiting which causes it to return to Default after 1000ms. The transition, however, has lowest priority (indicated by 1) such that a message will be considered if it has been received. While being in state Convoy, the rear RailCab may propose to break the convoy by sending breakConvoy, which causes both to return to the NoConvoy/Default state. The transition from Convoy to EvaluateProposal is needed to prevent deadlocks in case of message loss.

		r2:RailCab			rear	front	r1:RailCab
	rear	var: int destinationID; cl: c_wait;	front		var: int destinationID; cl: c_eval;
		NoConvoy					NoConvoy
		[c_wait ≥ 1000ms]					/ convoyProposalRejected()
		convoyProposalRejected() /	2	1			1
	Default	/ convoyProposal (destinationID)	Waiting c_wait ≤ 1000ms entry / {reset:c_wait}	Default	convoyProposal (destinationID) /	EvaluateProposal c_eval ≤ 599ms entry / {reset:c_eval}
				3				2
				startConvoy() /			/ startConvoy()
		/ breakConvoy()		Convoy		breakConvoy() /	1	Convoy	2	convoyProposal (destinationID) /
	Fig. 2. Real-Time Statecharts of Real-Time Coordination Protocol Convoy Coordina-
	tion
	whether a convoy is useful or not. The decision depends, among others, on how
	long both

Acknowledgment We thank Marcel Sander for being the test person of our case study cooperating robots. This work was developed in the project "EN-TIME: Entwurfstechnik Intelligente Mechatronik" (Design Methods for Intelligent Mechatronic Systems). The project ENTIME is funded by the state of North Rhine-Westphalia (NRW), Germany and the EUROPEAN UNION, European Regional Development Fund, "Investing in your future". This work was developed in the course of the Special Research Initiative 614 -Self-optimizing Concepts and Structures in Mechanical Engineering -University of Paderborn, and was published on its behalf and funded by the Deutsche Forschungsgemeinschaft. Christian Heinzemann is supported by the International Graduate School Dynamic Intelligent Systems.


Roberto Bruni

Carla Ferreira

Anne Kersten Kauer

First-Order Dynamic Logic for Compensable Processes

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

Introduction

Recent years have witnessed a massive distribution of data and computation, especially in the case of emerging paradigms like service-oriented computing and cloud computing. This has led to a breakthrough in the design of modern distributed applications, which need to integrate heterogeneous and loosely coupled components or services. When passing from coarse grain design to fine grain implementation, it is often the case that certain groups of activities must be performed in a transactional (all-or-nothing) fashion. However, many such transactions are long-lasting (weeks or even months), which prevents classical lock mechanisms from ACID transactions to be applicable in this setting. Instead, compensable long-running transactions seem to offer a more convenient approach, that deals well with distribution and heterogeneity: each activity is assigned a compensation; if the activity succeeds, then the compensation is installed; if the transaction ends successfully, then the installed compensations are discarded; if a fault occurs within the run of the transaction, then the installed compensations are executed (in the reverse order of installation) to compensate the fault and restore the system to a consistent state. While traditional perfect roll-back mechanisms guarantee that the initial state is exactly restored after a fault occurs, in compensable long-running transactions this is not realistic: if a message has been sent it cannot just be held back and maybe another message has to be sent for compensation. For example, late canceling of a booking may require some fees to be paid.

Compensable workflows enjoy an intuitive and expressive graphical representation that has become widely popular in areas such as business process modeling and service orchestration. However, analysis and verification techniques require more work to be done in the area of formal foundation and modeling of programs-with-compensations.

Starting from StAC [START_REF] Butler | A Process Compensation Language[END_REF] a number of other formalisms emerged, especially in the area of process calculi, and some of them have been applied as semantic frameworks of widely adopted standard technologies [21,[START_REF] Lucchi | A pi-calculus based semantics for WS-BPEL[END_REF][START_REF] Eisentraut | Fault, compensation and termination in WS-BPEL 2.0 -A comparative analysis[END_REF]. Such formalisms often employ basic activities abstract in nature [START_REF] Bruni | Theoretical foundations for compensations in flow composition languages[END_REF][START_REF] Butler | A Trace Semantics for Long-Running Transactions[END_REF][START_REF] Bravetti | On the expressive power of process interruption and compensation[END_REF] (i.e. taken over an alphabet of labels) or are based on message passing approaches for interaction [START_REF] Vaz | Dynamic Recovering of Long Running Transactions[END_REF][START_REF] Mazzara | Towards a Unifying Theory for Web Services Composition[END_REF][START_REF] Bruni | Nested Commits for Mobile Calculi: Extending Join[END_REF][START_REF] Vries | Communicating Transactions -(Extended Abstract)[END_REF]. Other approaches focus only on a basic notion of reversibility [START_REF] Danos | Reversible Communicating Systems[END_REF][START_REF] Lanese | Reversing higher-order pi[END_REF]. Moreover, although some recent proposals addressed the problem of compensation correctness [START_REF] Vaz | Towards compensation correctness in interactive systems[END_REF][START_REF] Caires | A process calculus analysis of compensations[END_REF], they miss a wellestablished logic counterpart, to be used by analysts, designers and programmers to prove some basic consistency properties of faulty systems after a compensation.

In this paper, we improve over existing literature on compensable workflows by proposing a rigorously formalised concurrent programming language with compensations and developing a logical framework based on dynamic logic to investigate program properties. The choice of extending dynamic logic is not incidental: we have been inspired by the interesting literature using deontic logic for error handling [START_REF] Broersen | A fixed-point characterization of a deontic logic of regular action[END_REF][START_REF] Castro | Deontic action logic, atomic boolean algebras and fault-tolerance[END_REF]. The main novelties with respect to previous approaches is that we study concurrent programs based on compensation pairs. At the semantic level, instead of interpreting programs over pairs of states (initial and final), we take traces and make explicit the presence of possible faults. A more detailed discussion of related work is given in Sections 2.1 and 2.2. The main result establishes some sufficient conditions under which a compensable program is guaranteed to always restore a correct state after a fault.

Structure of the paper. In Section 2 we overview some background on logical formalism for error handling, and more specifically about first-order dynamic logic that we shall extend twice: in Section 3 to deal with concurrent programs and in Section 4 to deal with compensable (concurrent) programs. Our framework is detailed over a toy running example. Some concluding remarks are discussed in Section 5 together with related work and future directions of research.

First Order Dynamic Logic

In this section we recap the basic concepts of first order dynamic logic [START_REF] Harel | First order dynamic logic[END_REF]. It was introduced to reason directly about programs, using classical first order predicate logic and modal logics combined with the algebra of regular events. In the second part we shall briefly overview related work on the two main concepts for our extension of dynamic logic, namely deontic formalisms for error handling and concurrency.

Let Σ = {f, g, . . . , p, q . . .} be a finite first-order vocabulary where f, g range over Σ-function symbols and p, q over Σ-predicates. Each element of Σ has a fixed arity, and we denote by Σ n the subset of symbols with arity n > 0. Moreover let V = {x 0 , x 1 , . . .} be a countable set of variables. Let Trm(V ) = {t 1 , . . . , t n , . . .} be the set of terms over the signature Σ with variables in V .

Definition 1 (Activities

). Let x 1 , • • • , x n ∈ V and t 1 , • • • , t n ∈ Trm(V ). A basic activity a ∈ Act(V ) is a multiple assignment x 1 , • • • , x n := t 1 , • • • , t n .
As special cases, we write a single assignment as x := t ∈ Act(V ) (with x ∈ V and t ∈ Trm(V )) and the empty assignment for the inaction skip.

Example 1. We take an e-Store as our first example (see Fig. 1 for the complete presentation). Activity acceptOrder ∈ Act(V ) is defined as a multiple assignment to variables stock and card such that acceptOrder stock , card := stock -1, unknown. This activity decreases the items in stock by one (the item being sold is no longer available), and resets the current state of the credit card to unknown.

Basic activities can be combined in different ways. While it is possible to consider while programs (with sequential composition, conditional statements and while loops), we rely on the more common approach based on the so-called regular programs.

Definition 2 (Programs).

A program α is any term generated by the grammar:

α, β ::= a | α ; β | α β | α *
A program is either: a basic activity a ∈ Act(V ); the sequential composition α ; β; the nondeterministic choice α β; or the iteration α * for programs α and β.

To define the semantics of programs we introduce a computational domain.

Definition 3 (Computational Domain).

Let Σ be a first-order vocabulary. A firstorder structure D = (D, I) is called the domain of computation such that: D is a non-empty set, called the carrier, and I is a mapping assigning:

to every n-ary function symbol f ∈ Σ a function f I : D n → D; to every n-ary predicate p ∈ Σ a predicate p I : D n → Bool .

A state is a function s : V → D that assigns to each variable an element of D. The set of all states is denoted by State(V ). As usual, we denote by s[x → v] the state s such that s (x) = v and s (y) = s(y) for y = x. Now we can extend the interpretation to terms in a given state.

Definition 4 (Term Valuation

). The valuation val of a term t ∈ Trm(V ) in a state s ∈ State(V ) is defined by:

val (s, x) s(x) if x ∈ V ; val (s, f (t 1 , . . . , t n )) f I (val (s, t 1 ), . . . , val (s, t n )).
Basic activities (and thus programs) are interpreted as relations on states. For basic activities this means evaluating the assignments in the current state replacing the old values of the variables.

Definition 5 (Interpretation of Activities). The valuation ρ ∈ 2 State(V )×State(V ) of an activity a ∈ Act(V ) is defined by:

ρ(a) {(s, s ) | s = s[x 1 → val (s, t 1 ), • • • , x n → val (s, t n )]} if activity a is defined by a multiple assignment x 1 , • • • , x n := t 1 , • • • , t n .
Definition 6 (Interpretation of Programs). We extend the interpretation ρ of basic activities to programs in the following manner:

ρ(α ; β) {(s, r) | (s, w) ∈ ρ(α) ∧ (w, r) ∈ ρ(β)} ρ(α β) ρ(α) ∪ ρ(β) ρ(α * ) ρ(α) *
Sequential composition is defined using the composition of relations. The union is used for nondeterministic choice. The iteration is defined as the choice of executing a program zero or more times.

To reason about program correctness, first order dynamic logic relies on the following syntax for logical formulas.

Definition 7 (Formulas). The set of formulas Fml (V ) is defined by the following grammar:

ϕ, ψ ::= p(t 1 , • • • , t n ) | | ⊥ | ¬ϕ | ϕ ∧ ψ | ϕ ∨ ψ | ϕ → ψ | ∀x.ϕ | ∃x.ϕ | α ϕ | [α]ϕ for p ∈ Σ n a predicate, t 1 , • • • t n ∈ Trm(V ), x ∈ V and α ∈ Prog(V ).
The notion of satisfaction for logic formulas is straightforward for first order operators. The program possibility α ϕ states that it is possible that after executing program α, ϕ is true. The necessity operator is dual to the possibility. It is defined as A valid formula for Ex. 1 would be stock > 0 → [acceptOrder ]stock ≥ 0 (assuming that the computational domain are the natural numbers). Below we show how in previous approaches dynamic logic is either extended with deontic formalisms or concurrency. Most of these approaches use propositional dynamic logic [START_REF] Harel | Dynamic logic[END_REF]. It is more abstract than first order dynamic logic. The interpretation of basic activities is an abstract relation on states, often Kripke frames are used. Thus there is no need for the valuation of terms and the computational domain. However it does not allow for quantification in formulas.

[α]ϕ ¬ α

Deontic Formalisms for Error Handling

In this section we overview previous approaches that combine dynamic logic with deontic logic [START_REF] Wright | I. deontic logic[END_REF] by introducing operators for permission, obligation and prohibition. While the original deontic logic reasons on predicates, in combination with dynamic logic these operators are applied to actions.

Meyer [START_REF] Meyer | A different approach to deontic logic: Deontic logic viewed as a variant of dynamic logic[END_REF] proposed the use of a violation condition V that describes an undesirable situation, so that the violation condition corresponds to validity of proposition V . The prohibition operator is defined such that s |= F α iff s |= [α]V , i.e., it is forbidden to do α in s iff all executions of α terminate in a violation. Obligation and permission are defined based on prohibition. The main problem with Meyer's work is that dependency between permission and prohibition raises paradoxes. Paradoxes of deontic logics are valid logical formulas that go against common sense, e.g., Ross' paradox states if a letter ought to be sent, then a letter ought to be sent or burnt.

While Meyer focused on permission of states, Meyden [START_REF] Van Der Meyden | The dynamic logic of permission[END_REF] defined permission on the possible executions of an action. He extended models for dynamic logic with a relation P on states. An execution of an action α is permitted if every (internal) state transition of α is in P . This implies that if an execution of an action is permitted also each of its subactions must be permitted. This avoids, for example, Ross' paradox. Meyden's definition of violation is however not very different from Meyer's. As shown in [START_REF] Broersen | Modal Action Logics for Reasoning about Reactive Systems[END_REF] there is a correspondence between the two definitions.

In [START_REF] Broersen | A fixed-point characterization of a deontic logic of regular action[END_REF] Broersen et al. define permission of an action as a proposition over states and actions. Each model contains a valuation function that maps permission propositions over atomic actions to sets of states. Contrary to the previous approaches permission is in fact based on the action itself. For compound actions permission is defined in terms of possible traces and its subactions. Broersen extends this approach in [START_REF] Broersen | Modal Action Logics for Reasoning about Reactive Systems[END_REF] including also concurrency.

Castro and Maibaum [10] refine Broersen's approach. Their definition of violation is very similar, however actions can be combined differently. While previous approaches focused on free choice and sequence for the combination of atomic actions, the authors define the domain of actions as an atomic boolean algebra. Actions can be combined using choice, intersection (i.e. concurrency) and a locally restricted form of complement. This allows them to show not only that their logic is sound and complete, but moreover it is decidable and compact.

Concurrency

There are only a few approaches adding concurrency to dynamic logic. The first, concurrent dynamic logic [START_REF] Peleg | Concurrent dynamic logic[END_REF], interpretes programs as a collection of reachability pairs, such that for each initial state it assigns a set of final states. In case of parallel composition the sets of final states are joined, while for choice the reachability pairs are joined. In this approach the formula α ϕ holds in states s such that a reachability pair (s, U ) for the interpretation of α exists and each state s ∈ U satisfies ϕ. In particular, the axiom α ∩ β ϕ ↔ α ϕ ∧ β ϕ is valid, i.e., actions are independent of each other.

For Broersen [START_REF] Broersen | Modal Action Logics for Reasoning about Reactive Systems[END_REF] this is an undesirable property. He considers only true concurrency, i.e. executing actions in parallel has a different effect than interleaving them. The interpretation uses the intersection for concurrency. Moreover he considers an open concurrency interpretation, which is not applicable to first order dynamic logic (that follows a closed action interpretation).

In [START_REF] Benevides | A propositional dynamic logic for CCS programs[END_REF] the authors define a dynamic logic for CCS where the interpretation of concurrency is based on the labelled transition system of CCS. Thus concurrency is either interpreted as interleaving or the so-called handshake of CCS. This is the first article applying dynamic logic to a process calculus.

As we have seen, concurrency in dynamic logic is often interpreted as a simultaneous execution. This interpretation is not suited for the kind of systems we want to model, where concurrent programs describe activities that can be executed concurrently, or even in parallel, but do not have to happen simultaneously. A possible approach would be to only allow parallel composition of independent processes, i.e., processes that do not interfere with each other. This requirement is quite strong and excludes most long running transactional systems. In the area of transactional concurrency control, extensive work has been done on the correctness criterion for the execution of parallel transactions. Proposed criteria include, linearizability [START_REF] Herlihy | Linearizability: a correctness condition for concurrent objects[END_REF], serializability [START_REF] Papadimitriou | The serializability of concurrent database updates[END_REF], etc. These criteria are more realistic, since they allow some interference between concurrent transactions. Therefore, for our interpretation of concurrency we used a notion of serializability (less restrictive than linearizability), stating that: the only acceptable interleaved executions of activities from different transactions, are those that are equivalent to some sequential execution. Serializability is presented formally in Def. 17.

Concurrent Programs

We will consider an extension of first-order dynamic logic. We keep the definitions for the term algebra and variables from Section 2. Our definition of basic activities is extended to take into account a validity formula.

Definition 9 (Basic Activities).

A basic activity a ∈ Act(V ) is a multiple assignment together with a quantifier and program-free formula E(a) ∈ Fml (V ) that specifies the conditions under which activity a leads to an error state.

Formula E(a) can be seen as a precondition of activity a: if formula E(a) holds on state s, executing a will cause an error. We exploit E(a) to classify state transitions as successful or failed, depending on whether the precondition holds or not on a given state. We could use instead for each activity a an explicit set of error transitions or error states, but those sets (either of error transitions or states) can be obtained from formula E(a). Another point worth discussing is the use of E(a) as a precondition or postcondition for activity a. Using E(a) as a precondition of a ensures erroneous state transitions do not occur, leaving the system in a correct state (the last correct state before the error). Whereas using E(a) as a postcondition of a, the state transition has to occur to determine if E(a) holds. Note that the empty assignment skip is always successful. Consider once more activity acceptOrder from Ex. 1. A possible error condition could be E(acceptOrder ) stock ≤ 0, that checks if there are any items in stock.

The definition of concurrent programs uses standard dynamic operators, including parallel composition and a test operator for a quantifier-free formula ϕ.

Definition 10 (Concurrent Programs). The set Prog(V ) of programs is defined by the following grammar:

α, β ::= a | ϕ? | α ; β | α β | α β | α *
Let the computational domain be as in Def. 3, as well as the valuation of terms as in Def. 4. The interpretation of basic activities (and thus programs) differs from the usual interpretation of dynamic logic. First we distinguish between activities that succeed or fail. Second we use traces instead of the relation on states. This is due to the combination of possible failing executions and nondeterminism. We will explain this further when introducing the interpretation of concurrent programs.

Definition 11 (Traces).

A trace τ is defined as a sequence of sets of triples

[[ ]] where ∈ {a, -a, ϕ?} (a ∈ Act(V ) a multiple assignment x 1 , • • • , x n := t 1 , • • • , t n , ϕ ∈ Fml (V ) a quantifier-free formula) and [[a]] {s a s | s = s[x 1 → val (s, t 1 ), • • • , x n → val (s, t n )] ∧ s |= ¬E(a)} [[-a]] {s a s | s |= E(a)} [[ϕ?]] {s ϕ? s | s |= ϕ}.

We will use [[]]

for the singleton containing the empty (but defined) trace; when combined with another trace it acts like the identity. Moreover we use the notation

[[ .τ ]] = [[ ]][[τ ]] for traces with length ≥ 1. Note that if [[ ]] = ∅ the trace is not defined.
When composing traces there is no restriction whether adjoining states have to match or not. The system is in general considered to be open, i.e., even within one trace between two actions there might be something happening in parallel changing the state. When we build the closure of the system traces that do not match are discarded.

A closed trace is a trace where adjoining states match. We define a predicate closed on traces such that closed (s s ) = and closed (s s .τ ) = closed (τ ) ∧ (s = first(τ )). For closed traces we can define functions first and last that return the first and the last state of the trace.

Definition 12 (Interpretation of Basic Activities). The valuation ρ of an activity a ∈ Act(V ) is defined by:

ρ(a) [[a]] ∪ [[-a]]
With this semantic model an activity a may have "good" (committed) or "bad" (failed) traces, depending on whether the initial state satisfies E(a) or not. As it is clear from the interpretation of basic activities, a precondition violation forbids the execution of an activity. Therefore failed transitions do not cause a state change.

Example 2. Take activity acceptOrder from Ex. 1 and its error formula E(acceptOrder ). In this setting, we have that

[[acceptOrder ]] {s acceptOrder s | s = s[stock → s(stock )-1, card → unknwn] ∧ s |= stock > 0} [[-acceptOrder ]] {s acceptOrder s | s |= stock ≤ 0}
As we mentioned for basic activities, we use traces instead of a state relation for the interpretation of programs. To illustrate this decision consider the behaviour of a compensable program. If it is successful the complete program will be executed. If it fails the program is aborted and the installed compensations will be executed. Thus we need to distinguish between successful and failing executions. Hence we need to extend the error formula E. But extending E to programs does not suffice as programs introduce nondeterminism, i.e., a program with choice may both succeed and fail in the same state. Using E for programs would however only tell us that the program might fail, not which execution actually does fail. For a trace we can state whether this execution fails or not.

Definition 13 (Error Formulas of Traces). We lift error formulas from activities to traces τ by letting E(τ ) being inductively defined as:

E([[]]) ⊥ E([[a]]τ ) E(τ ) E([[ϕ?]]τ ) E(τ ) E([[-a]]τ )
We exploit error formulas for defining the sequential composition • of traces. If the first trace raises an error, the execution is aborted and thus not combined with the second trace. If the first trace succeeds sequential composition is defined as usual, i.e. we append the second trace to the first trace.

τ α • τ β τ α if E(τ α ) τ α τ β if ¬E(τ α )
Abusing the notation we use the same symbol • to compose sets of traces.

Next, to build the trace for parallel composition of two basic programs we would consider the interleaving of any combination of traces:

[[]] τ 2 {τ 2 } [[ 1 ]]τ 1 [[ 2 ]]τ 2 {[[ 1 ]]τ | τ ∈ (τ 1 [[ 2 ]]τ 2 )} τ 1 [[]] {τ 1 } ∪ {[[ 2 ]]τ | τ ∈ ([[ 1 ]]τ 1 τ 2 )}
Now we can define the interpretation of concurrent programs:

Definition 14 (Interpretation of Concurrent Programs). We extend the interpretation ρ from basic activities to concurrent programs in the following manner:

ρ(ϕ?) [[ϕ?]] ρ(α ; β) {τ α • τ β | τ α ∈ ρ(α) ∧ τ β ∈ ρ(β)} ρ(α β) ρ(α) ∪ ρ(β) ρ(α β) {τ | τ α ∈ ρ(α) ∧ τ β ∈ ρ(β) ∧ τ ∈ τ α τ β } ρ(α * ) [[]] ∪ ρ(α) • ρ(α * )
Test ϕ? is interpreted as the identity trace for the states that satisfy formula ϕ. The interpretation of sequential programs is the sequential composition of traces. Failed transitions are preserved in the resulting set as executions of α that have reached an erroneous state and cannot evolve. Choice is interpreted as the union of trace sets of programs α and β. The interpretation of parallel composition is the set of all possible interleavings of the traces for both branches. Iteration is defined recursively (by taking the least fixpoint). To build the closure of the system, i.e., a program α, we define the set of all closed traces for α such that closure(α) {τ | τ ∈ ρ(α) ∧ closed (τ )}.

Next we show in an example the application of Definition 14. Take program eStore defined as in Fig. 1. Note that we abbreviate activities using initials, e.g., we write aO for acceptOrder . This program describes a simple online shop and it starts with an activity that removes from the stock the ordered items. Since for most orders the credit cards are not rejected, and to decrease the delivery time, the client's card processing and courier booking can be done in parallel. In this example, the activities running in parallel may interfere with each other as bookCourier will fail once the card is rejected. As the order of the execution for the parallel composition is not fixed after rejecting the credit card we issue a throw (defined as the empty assignment that always fails). In the interpretation of program eStore we can first distinguish the traces where acceptOrder succeeds and where it fails. In the latter case no other action is executable. In the successful case the parallel composition is executed where both branches may succeed or fail and we include any possible interleaving. Note that the traces

| s = s[stock → s(stock ) -1, card → unkown] ∧ r = s [card → accepted ] ∧s = r[courier → booked ] ∧ s |= stock > 0 ∧ r |= ¬card = rejected )
For formulas we include two modal operators related to program success where success of a program is interpreted as not reaching an erroneous state. The modal operator success S(α) states that every way of executing α is successful, so program α must never reach an erroneous state. The modal operator weak success S W (α) states that some way of executing α is successful. The failure modal operator F(α) is a derived operator, F(α) = ¬S W (α), and states that every way of executing α fails. Notice that both weak success and program possibility ensure program termination, while success and program necessity do not.

Definition 15 (Formulas). The set of formulas Fml (V ) is defined by the grammar:

ϕ, ψ ::= p(t 1 , • • • , t n ) | | ⊥ | ¬ϕ | ϕ ∧ ψ | ϕ ∨ ψ | ϕ → ψ | ∀x.ϕ | ∃x.ϕ | α ϕ | [α]ϕ | S(α) | S W (α) | F(α) for p ∈ Σ n a predicate, t 1 , • • • t n ∈ Trm(V ), x ∈ V and α ∈ Prog(V ).
Definition 16 (Formula Validity). The validity of a formula ϕ in a state s ∈ State(V ) of a computational domain D = (D, I) is defined by:

s |= p(t 1 , . . . , t n ) iff p I (val (s, t 1 ), . . . , val (s, t n )) s |= for all s ∈ S s |= ¬ϕ iff not s |= ϕ s |= ϕ ∧ ψ iff s |= ϕ and s |= ψ s |= ∀x.ϕ iff s[x → d] |= ϕ for all d ∈ D s |= α ϕ iff ∃ τ ∈ closure(α) such that first(τ ) = s ∧ last(τ ) |= ϕ s |= S(α) iff for all τ ∈ closure(α), first(τ ) = s implies ¬E(τ ) s |= S W (α) iff ∃ τ ∈ closure(α) such that first(τ ) = s and ¬E(τ ) s |= F(α) iff s |= ¬S W (α)
The new modal operators for success and failure are defined according to the description given above. Considering Fig. 1 a possible formula would be F(acceptOrder ), that is only satisfiable in some states. However stock ≤ 0 → F(acceptOrder ) is a valid formula for any state.

As it was discussed in Section 2, we want an interpretation of concurrency where concurrent activities do not have to happen simultaneously. For example, packing the items in a client's order and booking a courier to deliver that same order are independent activities that can be run in parallel. If, contrary to the example just mentioned, parallel activities are not independent then concurrency becomes more complex: as activities may interfere with each other, this may lead to unexpected results. In this work parallel composition is not restricted to independent programs (such that the set of variables updated and read by those programs is disjoint), however without any restriction the logic is too liberal to state any properties. Instead we use a notion of serializability (Def. 17). We will use the abbreviation τ τ for traces τ and τ denoting

τ τ closed (τ ) ∧ closed (τ ) ∧ first(τ ) = first(τ ) ∧ last(τ ) = last(τ )
Definition 17 (Serializable Concurrent Programs). Processes α and β are serializable if for every trace τ ∈ closure(α β) there exist ν ∈ ρ(α) and µ ∈ ρ(β) such that either τ (νµ) or τ (µν).

Note that serializability is defined as an implication, as the equivalence cannot be ensured. The fact that activities may be executed independently does not ensure, in the presence of interference, that those activities may be executed concurrently. We show some useful logical equivalences involving the novel modal operators. We are particularly considering their interplay with parallel composition. Proposition 1. Let α, β be two serializable programs. The following are valid formulas in the presented dynamic logic:

α β ϕ ∨ β α ϕ ↔ α β ϕ S(α ; β β ; α) ↔ S(α β) S W (α ; β) ∨ S W (β ; α) ↔ S W (α β) F(α ; β) ∧ F(β ; α) ↔ F(α β)

Compensable Programs

This section defines compensable programs, where the basic building block is the compensation pair. A compensation pair a ÷ a is composed by two activities, such that if the execution of the first activity is successful, compensation a is stored. Otherwise, if activity a fails, no compensation is stored. Compensation pairs can be composed using similar operators as for basic programs. The transaction operator {[•]} converts a compensable program into a basic program by discarding stored compensations for successful executions and running compensations for failed executions.

Definition 18 (Compensable Programs). The set Cmp(V ) of compensable programs is defined by the following grammar (for a, a ∈ Act(V )):

α ::= . . . | {[δ]} δ, γ ::= a ÷ a | δ ; γ | δ γ | δ γ | δ *
In order to ensure the overall correctness of a compensable program, the backward program of a compensation pair a ÷ a must satisfy a condition: a must successfully revert all forward actions of activity a. In the following we do not require that a exactly undoes all assignments of a and thus revert the state to the exact initial state of a. Instead, we require that it performs some compensation actions that lead to a "sufficiently" similar state. The way to determine if two states are similar depends on the system under modeling, so we do not enforce any rigid definition. Still, we propose a concrete notion that may characterize a widely applicable criterion of correctness (but other proposals may be valid as well).

The notion we give is parametric w.r.t. a set of variables whose content we wish to monitor.

Definition 19. Let X be a set of integer variables. We call s\ X s the distance over X between two states, i.e., the set of changes occurred over the variables in X, when moving from s to s . Formally, we define (s\ X s )(x) = s (x) -s(x) for any x ∈ X (and let (s\ X s )(x) = 0 otherwise).

For an empty trace the distance is null, the same holds for s\ X s.

Definition 20 (Correct Compensation Pair). Let X be a set of integer variables. Activity a ∈ Act(V ) is a correct compensation over X of a iff for all traces s a s ∈ ρ(a) with s |= ¬E(a), then for all t a t ∈ ρ(a) we have t |= ¬E(a) and s\ X s = t\ X t . Example 3. For most hotels the cancellation of a booking requires the payment of a cancellation fee. This can be modeled by a compensation pair bookHotel ÷cancelHotel , where forward activity bookHotel books a room and sets the amount to be paid, while the compensation cancelHotel cancels the reservation and charges the cancellation fee. bookHotel rooms, price, fee := rooms -1, 140$, 20$ cancelHotel rooms, price, fee := rooms + 1, fee, 0$

In this example cancelHotel does not completely revert all of bookHotel actions, and in fact it is likely that room cancelation imposes some fees. However, if we are only interested in the consistency of the overall number of available rooms, we can take X = {rooms} and consider s\ X s as a measure of distance. The idea is that a correct compensation should restore as available the rooms that were booked but later canceled.

In Definition 21 each compensable program is interpreted as a set of pairs of traces, where the first element is a trace of the forward program, while the second element is a trace that compensates the actions of its forward program. Compensation pairs are interpreted as the union of two sets. The first set represents the successful traces of forward activity a, paired with the traces of compensation activity a. The second set represents the failed traces, paired with the empty trace as its compensation. Sequential composition of compensable programs δ ; γ is interpreted by two sets, one where the successful termination of δ allows the execution of γ, the other where δ fails and therefore γ cannot be executed. As for the compensations of a sequential program, their traces are composed in the reverse order of their forward programs.

The interpretation of a transaction includes two sets: the first set discards compensable traces for all successful traces; while the second set deals with failed traces by composing the correspondent compensation trace with each failed trace. Notice that for this trace composition to be defined, it is necessary to clear any faulty activities in the failed forward trace. Therefore, in defining the interpretation of a transaction {[δ]}, we exploit a function cl that clears failing activities from a run:

cl ([[]]) [[]] cl ([[ ]]τ ) [[E(a)?]] cl (τ ) if = -a [[ ]] cl (τ ) otherwise
where E(a)? is the test for the error formula of activity a. It is always defined in s as activity a only aborts if s |= E(a), thus it is in general like a skip. In fact, if τ is faulty but successfully compensated by τ , then we want to exhibit an overall non faulty run, so that we cannot just take τ • τ (if E(τ ) then obviously E(τ • τ )). The following lemma states that cl does not alter the first nor the last state of a trace:

Lemma 1. For any τ : ¬E(cl (τ )), first(τ ) = first(cl (τ )) and last(τ ) = last(cl (τ )).

Definition 21 (Interpretation of Compensable Programs). Now we can define the interpretation ρ c of compensable programs in the following manner:

ρ c (a ÷ a) {(τ, τ ) | τ ∈ ρ(a) ∧ τ ∈ ρ(a) ∧ ¬E(τ )} ∪ {(τ, [[]]) | τ ∈ ρ(a) ∧ E(τ )} ρ c (δ γ) ρ c (δ) ∪ ρ c (γ) ρ c (δ ; γ) {(τ • ν, ν • τ ) | (τ, τ ) ∈ ρ c (δ) ∧ (ν, ν) ∈ ρ c (γ) ∧ ¬E(τ )} ∪ {(τ, τ ) | (τ, τ ) ∈ ρ c (δ) ∧ E(τ )} ρ c (δ γ) {(τ, τ ) | (ν, ν) ∈ ρ c (δ) ∧ (µ, µ) ∈ ρ c (γ) ∧ τ ∈ ν µ ∧ τ ∈ ν µ} ρ c (δ * ) {([[]], [[]])} ∪ ρ c (δ ; δ * ) ρ({[δ]}) {τ | (τ, τ ) ∈ ρ c (δ) ∧ ¬E(τ )} ∪ {cl (τ ) • τ | (τ, τ ) ∈ ρ c (δ) ∧ E(τ )}
In Fig. 2 we present a compensable program that specifies a hotel booking system. In this example the activity bookHotel updates several variables: it decreases the rooms available, sets the booking status to booked , while the price and cancellation fee are set to predefined values. Next, there is a choice between confirming or canceling the booking. These last two activities do not have a compensation, represented by defining compensation as skip. After cancelBooking the process is aborted by executing throw . Regarding the interpretation of HotelBooking, each forward run is paired with a compensation trace that reverts all its successfully terminated activities. For example, the first pair of traces represents a successful execution, where after booking a room the client accepts that reservation. In this case the stored compensation reverts both the acceptance of the booking and the booking it self. Note that as in Example 3, the compensation activity cancelHotel does not revert completely its main activity: it reverts the room booking, charges the cancellation fee, and it leaves the booking status unchanged.

ρ(HotelTransactions) = [[bH1.aB1]] [[bH2.aB2]] ∪ [[E(bH1)?]] [[E(bH2)?]] ∪ [[bH1.cB1.E(throw 1)?.skip 1 .cH1]] [[bH2.cB2.E(throw 2)?.skip 2 .cH2]] ∪ [[bH1.aB1]] [[bH2.cB2.E(throw 2)?.skip 2 .cH2]] ∪ [[bH1.cB1.E(throw 1)?.skip 1 .cH1]] [[bH2.aB2]] ∪ [[E(bH1)?]] [[bH2.cB2.E(throw 2)?.skip 2 .cH2]] ∪ [[bH1.cB1.E(throw 1)?.skip 1 .cH1]] [[E(bH2)?]] ∪ [[bH1.aB1]] [[E(bH2)?]] ∪ [[E(bH1)?]] [[bH2.aB2]]
Fig. 3 shows the parallel composition of two HotelBooking transactions (the subscripts are used only to distinguish activities from different transactions). The set of all possible interleaving is quite large, even after discarding traces that are not satisfied by any possible state. An example of a trace to be discarded is [[E(bH 1 )?.bH 2 .aB 2 ]], as E(bH 1 ) is true in a state s such that s |= rooms ≤ 0 and in that case [[bH 2 .aB 2 ]] could not be executed.

The program of Fig. 3 shows how the interleaved execution of processes may lead to interferences. Consider θ 1 = [[bH 1 .cB 1 .E(throw 1 )?.skip 1 .cH 1 ]] that describes traces where the booking succeeds and is later canceled by the client, and θ 2 = [[E(bH 2 )?]] that describes traces where no rooms are available and therefore no activity can be executed. Take the interleaving of traces of θ 1 and θ 2 on an initial state s such that s |= rooms = 1. In this setting, θ 1 has to be executed first and consequently activity bH 1 books the last room available. There is no serial execution of θ 1 and θ 2 (these sets of traces cannot be sequentially composed), since after the execution of a trace of θ 1 activity bH 2 should succeed (the last room becomes available again after the execution of cB 1 ). However, the following interleaved execution is possible [[bH 1 .E(bH 2 )?.cB 1 .E(throw 1 )?.skip 1 .cH 1 ]], because when bH 2 is executed there are no rooms available. This shows that HotelTransactions is not serializable, since some interleaved traces do not correspond to a serial execution.

The aim of compensable programs is that the overall recoverability of a system can be achieved through the definition of local recovery actions. As the system evolves, those local compensation actions are dynamically composed into a program that reverts all actions performed until then. Therefore, it is uttermost important that the dynamically built compensation trace does indeed revert the current state to the initial state. Next, we define the notion of a correct compensable program, where any failed forward trace can be compensated to a state equivalent to the initial state.

Definition 22 (Correct Compensable Program). Let X be a set of integer variables. A compensable program δ has a correct compensation over X if for all pairs of traces

(τ, τ ) ∈ ρ c (δ), if closed (τ ) and closed (τ ) then first(τ )\ X last(τ ) = last(τ )\ X first(τ ).
Serializability is extended from basic programs to compensable programs: Definition 23 (Serializable compensable parallel programs). Compensable programs δ and γ are serializable if for all (τ, τ ) ∈ ρ c (δ γ) with closed (τ ) and closed (τ ) there exist (ν, ν) ∈ ρ c (δ) and (µ, µ) ∈ ρ c (γ) such that the following holds: Either τ (νµ) or τ (µν) and either τ (ν µ) or τ (µ ν).

The following theorem shows the soundness of our language, since it proves that compensation correctness is ensured by construction: the composition of correct compensable programs results in a correct compensable program.

Theorem 1. Let X be a set of integer variables and δ a serializable compensable program where every compensation pair is correct over X, then δ is correct over X.

As in general serializability is hard to prove we suggest the simpler definition of apartness. If the set of variables updated and consulted by two programs are disjoint, those programs can be concurrently executed since they do not interfere with each other (a similar approach was taken in [START_REF] Caires | A process calculus analysis of compensations[END_REF]). Two compensable programs δ and γ are apart if they do not update or read overlapping variables, then δ and γ can be executed concurrently and their resulting traces can be merged. The final state of a concurrent execution of apart programs can be understood as a join of the resulting states of each program.

Formulas for basic programs can be easily extended to compensable programs as they can be applied to the forward program and stored compensations can be ignored.

The modal operator C(δ) states that every failure of δ is compensable. A weak compensable operator C W (δ) states that some failures of δ are compensable.

We extend the notion of closed traces from basic to compensable programs as closure(δ) {(τ, τ ) | (τ, τ ) ∈ ρ c (δ) ∧ closed (τ ) ∧ closed (τ )}.

Definition 24 (Formula Validity). We extend Definition 16 with the new modal operators for compensable programs.

Conclusion

In this paper we have introduced a rigorous language of compensable concurrent programs together with a dynamic logic for reasoning about compensation correctness and verification of behavioral properties of compensable programs. In this sense we go one step further of the approach in [START_REF] Vaz | Towards compensation correctness in interactive systems[END_REF][START_REF] Caires | A process calculus analysis of compensations[END_REF], where the formulas were mainly concerned with the temporal order of execution of actions in a message-passing calculus with dynamic installation of compensation, by allowing to express properties about the adequacy of the state restored by the compensation after a fault occurred. As detailed in Sections 2.1 and 2.2, our dynamic logic differs from previous proposal for the way in which concurrency is handled and for dealing with compensations. The works presented in [START_REF] Butler | A Trace Semantics for Long-Running Transactions[END_REF][START_REF] Caires | A process calculus analysis of compensations[END_REF] study the soundness of a compensating calculus by formalizing a notion of compensation correctness, which we also address in Theorem 1, but do not tackle the subject of verification of behavioral properties for compensable programs. Furthermore, even though compensation correctness is ensured by construction, our logic allows the verification of strong and weak correctness (through a formula) for compensable programs that contain some compensation pairs that are not correct. Our research programme leaves as ongoing work the development of a suitable computational model and corresponding logic for allowing a quantitative measure of correctness, so that different kinds of compensations can be distinguished (and the best can be selected) depending on their ability to restore a more satisfactory state than the others can do. Moreover, we would like to develop suitable equivalences over states that can reduce the complexity of the analysis, and facilitate the development of automatic reasoning tools.

Fig. 1 .

 1 Fig. 1. eStore example.

  [[-aC]], [[-rC]] and [[throw ]] are not defined, as their condition is not satisfied by any possible state. Building the closure for these traces we can rule out some possibilities, namely [[aO.aC. -bC]], [[aO. -bC.aC]], [[aO.rC. -throw .bC]] and [[aO.rC.bC. -throw ]] and [[aO. -bC.rC. -throw ]] would be excluded. A possible closed trace would be closed ( s aO s . s aC r . rbC s

Fig. 2 .

 2 Fig. 2. HotelBooking example.

Fig. 3 .

 3 Fig. 3. HotelTransactions example.

Proposition 2 .

 2 s |= δ ϕ iff ∃ (τ, τ ) ∈ closure(δ) such that first(τ ) = s ∧ last(τ ) |= ϕ s |= S(δ) iff for all traces (τ, τ ) ∈ closure(δ) if first(τ ) = s then ¬E(τ ) s |= S W (δ) iff ∃(τ, τ ) ∈ closure(δ) such that first(τ ) = s and ¬E(τ ) s |= F(δ) iff s |= ¬S W (δ) s |= C(δ, X) iff for all traces (τ, τ ) ∈ closure(δ) if E(τ ) and first(τ ) = s then first(τ )\ X last(τ ) = last(τ )\ X first(τ ) s |= C W (δ, X) iff ∃(τ, τ ) ∈ closure(δ) such that E(τ ) and first(τ ) = s and first(τ )\ X last(τ ) = last(τ )\ X first(τ )Considering Fig.2a possible formula is HotelBooking status = confirmed . Moreover we can prove C(HotelBooking, {rooms}) for any state. Let δ, γ be two compensable programs that are apart. The following are valid formulas in the presented dynamic logic: C(δ γ, X) ↔ C(δ, X) ∧ C(γ, X)C W (δ γ, X) → C W (δ, X) ∨ C W (γ, X)

  ¬ϕ stating that it is necessary that after executing program α, ϕ is true.

	Definition 8 (Formula Validity). The satisfiability of a formula ϕ in a state s ∈ State(V )
	of a computational domain D = (D, I) is defined by:
	s |= p(t 1 , . . . , t n ) iff p I (val (s, t 1 ), . . . , val (s, t n ))
	s |=	for all s ∈ S
	s |= ¬ϕ	iff not s |= ϕ
	s |= ϕ ∧ ψ	iff s |= ϕ and s |= ψ
	s |= ∀x.ϕ	iff s[x → d] |= ϕ for all d ∈ D
	s |= α ϕ	iff there is a state r such that (s, r) ∈ ρ(α) and r |= ϕ
	A formula is valid in a domain D if it is satisfiable in all states over D, it is valid if it is
	valid in all domains.

  -throw . -bC]] ∪ [[aO. -bC.rC. -throw ]] ∪ [[aO.rC. -bC. -throw ]] ∪ [[-aO]]

	eStore acceptOrder ; ((acceptCard rejectCard ; throw ) bookCourier )
	aO	stock , card := stock -1, unkown	E(aO)	stock ≤ 0
	aC	card := accepted	E(aC)	false
	rC	card := rejected	E(rC)	false
	bC	courier := booked	E(bC)	card = rejected
	throw	skip		E(throw ) true
	ρ(aO ; ((aC rC ; throw ) bC)) =
	[[aO.aC.bC]]		∪ [[aO.bC.aC]]	∪
	[[aO.aC. -bC]]		∪ [[aO. -bC.aC]]	∪
	[[aO.rC. -throw .bC]]	∪ [[aO.bC.rC. -throw ]]	∪ [[aO.rC.bC. -throw ]]	∪
	[[aO.rC.

Research supported by the EU Integrated Project 257414 ASCENS, the Italian MIUR Project IPODS (PRIN 2008).

A Proof Theorem 1

We use ∆ X (τ ) to denote first(τ )\ X last(τ ) and ∇ X (τ ) for last(τ )\ X first(τ ). In the following operation ⊕ denotes the union of two distances of two states. Lemma A. Let s, s , s ∈ State(V ). The following equality holds: s\ X s ⊕ s \ X s = s\ X s Theorem 1. Let X be a set of integer variables and δ a serializable compensable program where every compensation pair is correct over X, then δ is correct over X.

Proof. We proceed by induction on the structure of compensable δ.

1. δ = a ÷ a. For any (τ, τ ) ∈ ρ c (a ÷ a) with ¬E(τ ) we conclude by applying the hypothesis that the compensation pair a ÷ a is correct over X. For any failed trace (τ, τ ) ∈ ρ c (a ÷ a) with E(τ ), we have that τ = s a s for some state s such that s |= E(a). Furthermore, the compensation trace for a failed basic activity is empty.

It is easy to see that ∆ X (τ ) = null , which concludes the proof for this case. 2. δ = δ 1 δ 2 . By induction on δ 1 and δ 2 . 3. δ = δ 1 ; δ 2 . We need to distinguish two cases, by the definition of ρ c (δ 1 ; δ 2 ).

-For any pair

, and ¬E(τ ), then we want to prove that if closed (τ •ν) and closed

As we consider closed traces we can conclude that also closed (τ ) and closed (ν) with last(τ ) = first(ν) and the same holds for the compensation. Thus we can apply the induction hypothesis getting ∆ X (τ ) = ∇ X (τ ) and ∆ X (ν) = ∇ X (ν). We build the union of these two sets, i.e., ∆ X (τ )⊕∆

-For any (τ, τ ) ∈ ρ c (δ 1 ; δ 2 ) such that (τ, τ ) ∈ ρ(δ 1 ) and E(τ ), then the result follows immediately from the induction hypotheses on δ 1 . 4. δ = δ 1 δ 2 . With δ 1 , δ 2 serializable. For any (τ, τ ) ∈ ρ c (δ 1 δ 2 ) with (ν, ν) ∈ ρ c (δ 1 ), (µ, µ) ∈ ρ c (δ 2 ) τ ∈ ν µ, τ ∈ ν µ, we need to show that if closed (τ ) and closed (τ ) then ∆ X (τ ) = ∇ X (τ ).

Note that in general neither closed (ν) and closed (ν) nor closed (µ) and closed (ν) holds, because the interleaving is defined independently of this. According to serializability there exist traces (ν , ν ) ∈ ρ c (δ 1 ) and (µ , µ ) ∈ ρ c (δ 2 ) with several different possibilities for a sequential representation (though at least one holds). Without loss of generality we assume that τ (ν µ ) and τ (ν µ ). (The other representations can be treated similarly.) From closed (ν µ ) we know that closed (ν ), closed (µ ) and last(ν ) = first(µ ). The same holds for closed (ν µ ). Thus we can apply the induction hypothesis. We obtain ∆ X (ν ) = ∇ X (ν ) and ∆ X (µ ) = ∇ X (µ ). As for the sequential case we build the union of the two sets ∆ X (ν ) ⊕ ∆ X (µ ) = ∇ X (µ ) ⊕ ∇ X (ν ). From the equivalences and Lemma A we obtain first(ν )\ X last(µ ) = last(µ )\ X first(ν ) which is equivalent to ∆ X (ν µ ) = ∇ X (ν µ ). From the equivalences for serializability we can conclude ∆ X (τ ) = ∇ X (τ ). 5. δ = δ * 1 (by induction on the depth of recursion).