# A Polyadic pi-Calculus Approach for the Formal  Specification of UML-RT

Authors: J. M. Bezerra; C. M. Hirata
Journal: Advances in Software Engineering
 (2009)

---

## Abstract

UML-RT is a UML real-time profile that allows modeling event-driven and distributed systems; however it is not a formal specification language. This paper proposes a formal approach for UML-RT through a mapping of the UML-RT communicating elements into theπ-calculus (or pi-calculus) process algebra. The formal approach both captures the intended behavior of the system being modeled and provides a rigorous and nonambiguous system description. Our proposal differentiates from other research work because we map UML-RT to π-calculus, and we allow the mapping of dynamic reconfiguration of UML-RT unwired ports. We illustrate the usage and applicability of the mapping through three examples. The first example focuses on explaining the mapping; the second one aims to demonstrate the use of the π-calculus definitions to verify system requirements; the third case is an example of mobile processes called Handover protocol.


---

## Body

## 1. Introduction

The specification and development of real-time systems are a challenge due to their characteristic of criticality and safety. Formal methods have been seen as effective in real-time system development [1, 2]. The main advantage of formal methods is to allow a rigorous and nonambiguous system description; so it is possible, through formal verification, to evaluate some aspects such as consistency, completeness, and correctness. The formal verification involves the formal modeling of the system, the formal specification of requirements or properties, and the inference rules to prove that the model satisfies the properties (model checking) [3–5].The standard DO-178B, Software Considerations in Airborne Systems and Equipment Certification [6], is an acceptable guideline for embedded software approval used by the certification authorities. It suggests the use of formal methods to complement tests, because they generally increase confidence on correct behavior or that anomalous behavior will not occur. Furthermore, formal verification of models helps the designers to find out errors earlier in the modeling phase, which is essential to reduce costs according to Pressman [7].The most well-known modeling language is Unified Modeling Language (UML), officially defined by the Object Management Group (OMG). Up to the UML version 1.5 [8], the standard lacks support for some important aspects of embedded real-time systems, such as time constraints, signals, and independent components. Aiming to adapt UML to real-time system modeling, some UML profiles were proposed [9, 10]. For instance, Rational Software Company (now IBM) defined the UML RealTime (UML-RT) [11] profile that permits to model distributed and event-driven systems. The profile is supported by the IBM Rational Rose RealTime (RoseRT) tool [12].With the advance of UML 2.0 [13], UML was improved to model large-scale software systems including the ability to model entire system architectures. The basis of the improvement comes from the experience with various architectural description languages, such as UML-RT [14]. RoseRT is now commercialized as IBM Rational Rose Technical Developer tool [15]; however the features of UML-RT are still present, because they are the source of UML 2.0 structure concepts, for example, the capsule is directly translated to structured classes in UML 2.0.As UML-RT is not a formal specification language; it is not possible to formally verify the models that are specified in UML-RT. So some researchers propose the transformation of the UML-RT model to a formal model using process algebras [16–19]. The process algebras to which transformation are proposed include CSP [20], CCS [21], and Circus [22]. Other work [23] represents the UML-RT model as timed automata.In the present paper, we propose a formal approach to the UML-RT through a mapping of the UML-RT communicating elements into theπ-calculus [24]. The π-calculus is a process algebra for systems that communicate concurrently. Its advantage is the ability to model mobility, which is made by passing channels as data through channels. The π-calculus does not address the computations that are not related to communication with other processes.This work is an extension of our earlier work on mapping from UML-RT toπ-calculus [25].  In that work, Bezerra et al. present the mapping to a π-calculus syntax version used by HAL-JACK (HD-Automata Laboratory) [26], which is an integrated tool set for the specification, verification, and analysis of concurrent and distributed systems. In this paper, we present the complete mapping using the polyadic π-calculus. The chosen syntax is the one proposed by Milner [24] and not the other one used by HAL-JACK (HD-Automata Laboratory) [26] tool, which is monoadic. The importance of polyadic is the ability to formally represent the communication of more than one message at a time. Besides, we include mapping rules to reason about the following UML-RT concepts: the entry and the exit actions, the composite states, and the transition chains.The rest of the paper is organized as follows. In Section2, we provide an overview of UML-RT and π-calculus, and we also describe the related work. We present the UML-RT to the π-calculus mapping in Section 3, and we illustrate the mapping with three examples in Section 4. The first example is used to explain how to apply the mapping to a UML-RT model and obtain the corresponding π-calculus definitions. The second example is employed to demonstrate that the designer is able to use the π-calculus definitions to verify if the model meets the system requirements. The third example is the Handover protocol presented in [24], and it illustrates the use of polyadic communication. Finally, in Section 5 some conclusions are drawn.


## 2. Theoretical Foundations

This  section starts with the description of the main elements of UML-RT, which are considered in the mapping ofπ-calculus whose description is presented in what follows. We end the section by discussing the related work.


### 2.1. UML-RT

UML-RT is an extension of UML with elements to facilitate the design of real-time systems. Three of the elements,capsule, port, and connector, are used to model system structure; one element, protocol, models the communication inside the system [11].Acapsule is an active class and represents software components that can be concurrent and physically distributed. A capsule has a state diagram and a structure diagram. A state diagram is similar to a UML standard state diagram and describes the capsule behavior. A structure diagram details the internal structure of a capsule, which includes subcapsules and their connections with each other. Figure 1 shows the structure diagram of the capsule TopSystem that comprises four subcapsules: source (instance of the capsule Source), router (instance of the capsule Router), target1 (instance of the capsule ConsumerTarget), and target2 (instance of the capsule ExporterTarget). The model was constructed using the RoseRT tool.Figure 1
The structure diagram of the capsuleTopSystem.Aport permits to exchange messages between capsules. A protocol needs to be specified for a port. A protocol defines both the number of participants in the communication and the signals that are received and sent by each participant. The connectors act as communicating channels between ports that must play different roles of the same protocol. A line between two ports represents a connector. In Figure 1, the ports q and r implement the protocol named ConfigProtocol, and they are connected to each other. The ports play conjugated roles, which can be noted in their representations: q as an empty (blank) square and r as a filled (black) square.A port can be classified in terms of visibility (public and protected), termination (end and relay), and connectivity (wired and unwired).  A public port is located at the capsule border and can interact with other capsule ports. A protected port is not visible from the outside; it serves as the communication point of the capsule with its subcapsules. In Figure 1, the capsule System has the public port out (indicated by the symbol +), and the protected ports setCT and setET (indicated by the symbol #).With respect to the termination, anend port provides the access to the capsule behavior given by its state diagram. In Figure 1, setCT and setET are end ports of the capsule TopSystem. A relay port is used to export the subcapsule interfaces.  When a relay port of a parent capsule receives a message, the message is passed automatically to the connected subcapsule port. And when a subcapsule sends a message through a port connected to a relay port of its parent capsule, the message is directly sent to the outside of the parent capsule. By definition, a relay port is public and wired. In Figure 1, out is a relay port of the capsule TopSystem.Awired port (e.g., q and r in Figure 1) has a connector joining them to exchange messages. An unwired port does not have a connector with other ports, but it allows dynamic communication during runtime through its name registration. In Figure 1, alert, s, and t are examples of unwired ports. Unwired ports can be registered to receive and send signals. For instance, the port s can be registered with the subscriber name x, and t can be registered with the subscriber name y. In this case, if the port alert is configured with the provider name x, the signal sent by Router along alert is received by ConsumerTarget. Similarly, if the port alert is set to y, its signal is received by ExporterTarget. In RoseRT, the subscriber port is called Service Access Point (SAP) and the provider port is called Service Provisioning Point (SPP).As mentioned, a capsule has also a state diagram. Figure2 presents the state diagram of the ExporterTarget capsule. The initial point (filled circle) is a point which explicitly shows the beginning of the state machine. The initial transition, named Initial, connects the initial point to the initial state. It does not have an associated trigger; however it may execute an associated action.Figure 2
The state diagram of the capsuleExporterTarget.Figure 3
The composite stateS2 of ExporterTarger state diagram.Astate is a condition in which the object is ready to process events. In Figure 2, there are states S1, S2, and S3. We can define actions to be performed when the control enters in a state (entry action, indicated by the symbol  ) and when it leaves a state (exit action, indicated by the symbol  ). A state that does not contain substates is called a simple state. A state that contains substates is called a composite or hierarchical state (indicated by the symbol ). For example, S1 and S3 are simple states; whereas S2 is a composite because it is composed of the simple states S4 and S5 as illustrated in Figure 3. Furthermore, a state can be a choice point, for example, S5, which allows a single transition to be split into two outgoing transition segments, after evaluating a condition on which branch to take. For instance, if the decision evaluation inside S5 returns true, the transition exportMsg is triggered; otherwise, the transition consumeMsg is triggered.Atransition is a relationship between two states: a source state and a destination state. It specifies the change of control from the source state to the destination state when an object in the source state receives a specified event and some conditions are met. Three concepts related to a transition include: trigger, guard condition, and action. Trigger indicates which events (signals) from which interfaces (ports) cause the transition to be taken; however the transition fires only if the guard condition is satisfied. After the transition activation, its action is executed. Actions are operation calls, a variable handling or a signal dispatch to another capsule.Transitions can span multiple hierarchies changing context on the way from the source to the destination state. Therefore they must be partitioned into different segments by the junction pointers. Each transition segment has a distinct name. Any segment can execute actions; however only the originating segment has a trigger. For instance, the transitionconfigPort illustrated in Figure 2 connects the states S1 and S2, but it comprises two segments inside the state S2 as shown in Figure 3: the transition configPort itself and the transition Initial1 separated by a junction pointer.It is important to mention that the triggers and the actions are configured internally in the RoseRT tool, and the model screenshot presents only the state and transition names. Table1 presents the transition information of the ExporterTarget state diagram, where the action is specified in C programming language. For example, the transition configPort triggers if it receives along the port setPort the signal portName. The transition action is the storage of the message, received through the port setPort, in the local variable aux using the statement “aux = *rtdata;”. Later the port t is renamed to aux, using the statement “t·registerSAP(aux);”. The transition exportMsg does not have a trigger, but it executes an action of sending along the port export the signal msg with the message d1.Table 1
Transitions of theExporterTarget state diagram.
TransitionTriggerActionInitial——configPortPort:setPortSignal:portNamet·registerSAP(aux);Initial1—Initial2—receiveMsgPort:tm = *rtdata;d1 = m·msg1;Signal:msgd2 = m·msg2;consumeMsg—exportMsg—export·msg(d1)·send();msgConsumed—msgExported—waitMsgPort:timer—Signal:timeoutUML-RT allows defining a class and sending an object of this class as a message. For example, the capsuleExportedTarget receives a message m in the transition receiveMsg with the attributes msg1 and msg2, which are stored, respectively, in d1 and d2 variables, according to Table 1. Later, by the transition exportMsg, the capsule ExportedTarget is able to send the message d1. However, the message m can be seen as two messages m1 and m2 transmitted in a single signal, which characterizes the communication of more than one message at a time in UML-RT.Although, there are other diagrams available in the UML-RT, such as use case, component, deployment, class, collaboration, and sequence diagrams; the proposed mapping rules deal only with the state and structure diagrams of UML-RT capsules.A use case diagram is specially used before the modeling phase in order to identify the functionality of the system. A component diagram shows the dependencies among software components that exist at compilation time, linking time, or run-time. A deployment diagram captures the physical distribution of the run-time processes across a set of processing nodes. As our scope is focused on design, and not on the requirement or implementation, the use case, component, and deployment diagrams are not addressed.A class diagram shows the static structure of the model. It may contain other elements besides classes, such as capsules and protocols. A collaboration diagram captures a desirable pattern of interactions between objects, emphasizing the structural organization of the objects. A capsule structure diagram is a specialized form of the collaboration diagram and includes information available also in the class diagram. A sequence diagram specifies communication scenarios of collaboration; however with the capsule structure diagram and the state diagram of each capsule it is possible to obtain all the possible collaborations; therefore the sequence diagram is not used. So our mapping considers only the state and structure diagrams of UML-RT capsules.


### 2.2. Theπ-Calculus

Theπ-calculus [24] is a process algebra for systems that communicate concurrently, that is, systems composed of processes that run in parallel and interact through channels. The main difference between π-calculus and its predecessors, CSP and CCS, is the possibility to pass channels as data through channels [27–29]. This characteristic allows the π-calculus to express mobility.The prefixπ of the π-calculus represents x̅〈y〉, x(y), or the unobservable action τ. The term x̅〈y〉 indicates that the π-calculus port (or channel) x sends the π-calculus message y. The term x(y) indicates that the message y is received along the port x. The round brackets (y) are used for the binding occurrence of a parametric name (one that may be instantiated by another name), and the angle brackets 〈y〉 for nonbinding occurrences of a name.Theπ-calculus process expression P is defined by the syntax:
(1)P:=∑i∈Iπi·Pi∣P1∣P2∣newaP∣!P.The term∑i∈Iπi·Pi indicates summation, where I is a finite indexing set. The dot is the sequence operation, which means that πi will occur before Pi becomes activated.  If i=2, we have π1·P1+π2·P2. If i=0, we have P=0, that is a stop process. In general, we omit the stop process, for example, we write x(y) instead of x(y)·0. The parallel composition P1∣P2 means that P1 and P2 run concurrently. The term new a P represents the restriction of the name a in the P context, that is, the name a is bound in P and it is not seen outside. The replication operator !P is the composition of unlimited copies of P.For example, considering the following processes ofB, C, D, and E, where
(2)B=(z̅〈x〉+z̅〈y〉),(3)C=z(a)·a̅〈b〉,(4)D=x(c),(5)E=y(d).The processB is able to send the message x along the port z or to send the message y along the port z. The process C can receive a message a through the port z, and later send the message b through the port a. The process D can only receive a message c along the port x. Finally, the process E is able to receive a message d via the port y.Assuming that the processA (Figure 4(a)) consists of B, C, D, and E above, so by using π-calculus, the process A is the parallel composition of the four processes:
(6)A=B∣C∣D∣E.Theπ-calculus mobility. (a) A process,  (b) A1 process, and  (c) A2 process.
(a)(b)(c)We can replace in (6) the definition of each process using (2) to (5), so
(7)A=(z̅〈x〉+z̅〈y〉)∣z(a)·a̅〈b〉∣x(c)∣y(d).To understand how to manipulate the definitions included in the processA definition, it is necessary to understand the π-calculus concepts related to the structural congruence and the reactions.The processesP and Q in the π-calculus are structurally congruent, written P≡Q, if one can be transformed into the other using the rules.(i) Change of Bound Names (Alpha-Conversion).
The alpha-conversion allows bound variable names to be renamed. As an example, in (2), we have that D=x(c). If D′=x(c), so D≡D′, that is, D is the same as D′.(ii) Reordering Terms in a Summation
The reordering terms in a summation are related to the commutative operations. For instance, in (1), we have that B=(z̅〈x〉+z̅〈y〉). But we can rewrite B by reordering its terms, so B=(z̅〈y〉+z̅〈x〉).(iii)P∣0≡P,P∣Q≡Q∣P,P∣(Q∣R)≡(P∣Q)∣R
The first term indicates that the stop process is the neutral element in the parallel composition. The second and the third terms are the commutative and the associative operation, respectively, of the parallel composition. For example, the definition ofA in (6) can also be written by reordering B and C, as A=C|B|D|E.(iv) newx(P∣Q)≡P∣ new xQ, If x Is not a Free Name of P
It states that if a processP does not have the free name x, the restriction of x in the parallel composition P∣Q is kept only in Q.(v)newx0≡0, and newx,yP≡newy,xP
The first term explains that there is no need to use restriction in the stop process. The second term indicates that the order of the names in a restriction operation is not important.(vi)!P≡P∣!P
It states that the replication ofP is the same as a parallel composition of an infinite number of P.The reaction relation overπ-calculus explains how the processes react with each other. It contains exactly the transitions which can be inferred from the following rules.(i) TAU [τ·P+M→P]
It states that in a processτ·P+M, if τ occurs, then we choose the first option of the choice operator and the result is only the P process.(ii) REACT [(x(y)·P+M)∣(x̅〈z〉·Q+N)→{z/y}P∣Q, Where {z/y}P Means that y Must Be Replaced by z]
It states that the two processes running concurrently(x(y)·P+M) and (x̅〈z〉·Q+N) may react, because the second process sends the message z along the port x, while the first process receives a message y along the port x. After the reaction, all occurrences of y in the first process are renamed by z.(iv) PAR [IfP→P′, Then P∣Q→P′∣Q]
It states that in a parallel composition, if one process transits to another, then the parallel composition is maintained.(v) RES [IfP→P′, Then newxP→newxP′]
It states that in a restriction operation, if one process transits to another, then the restriction is maintained.(vi) STRUCT [P→P′ Implies Q→Q′, if P≡Q, P′≡Q′]
It states that ifP transits to P′ it implies that Q transits to Q′, then P and Q are structurally congruent.In the example of the processA defined in (7), the actions z̅〈x〉 of B and z(a) of C are complementary and may interact generating A1:
(8)A1=0∣x̅〈b〉∣x(c)∣y(d).After the reactionA→A1, all occurrences of a in C are replaced by x. Figure 4(b) shows A1 process, where U=x̅〈b〉 and B is not represented because it is a stop process.Additionally, there is another possible interaction inA between z̅〈y〉 of B and z(a) of C, generating A2:
(9)A2=0∣y̅〈b〉∣x(c)∣y(d).After the reactionA→A2, all occurrences of a in C are replaced by y. Figure 4(c) depicts A2 process, where V=y̅〈b〉 and B is not represented because it is a stop process.The example illustrates theπ-calculus mobility concept, because the channels x (in the reaction A→A1) and y (in the reaction A→A2) are passed as message along the channel z, which links processes B and C. The mobility is the main aspect of the π-calculus whose representation is addressed in this paper.The presentedπ-calculus version is the monoadic π-calculus, in which a message contains exactly one name. The polyadic π-calculus [24] permits to exchange messages consisting of more than one name, using the prefixes x(y⃗) and x̅〈z⃗〉. In particular, it admits the cases x() and x̅〈〉 where y⃗ and z⃗ are empty, and we can write as x and x̅ to indicate only the synchronization between the ports.For an example of polyadicπ-calculus, consider the following process:
(10)E=x(y1,y2)·F∣x̅〈z1,z2〉·G∣x̅〈w1,w2〉·H.The first term in (10) may react with the second or the third term along the port x. The reaction with the second term replaces y1,y2 by z1,z2, respectively. While the reaction with the third term replaces y1,y2 by w1,w2, respectively.The definition ofE is different from E′ written in monoadic π-calculus, as follows:
(11)E′=x(y1)·x(y2)·F∣x̅〈z1〉·x̅〈z2〉·G∣x̅〈w1〉·x̅〈w2〉H.In (11), the first term may react with the second and later with the third term, resulting that y1 is replaced by z1, and y2 by w2. It is also possible that the first term may react with the third and later with the second term. In both cases, the result of (11) using monoadic π-calculus is different from that one expected in (10) using polyadic π-calculus. For the correct encoding of the polyadic using monoadic, it is necessary to guarantee that there can be no interference on the channel along which a composite message is sent. It is addressed by Milner in [24].A process in monoadic or polyadicπ-calculus can also have a list of input names written between round brackets, for example,
(12)I(m,n)=m̅〈n〉·I′.In this case, the definition of processI has the port name m and the message n available as input parameters. If a process J uses the definition of I, then J calls I definition passing the input names between angle brackets, for example,
(13)J(p)=p(q)·I〈q,r〉.In (13), J references I definition passing q and r to, respectively, rename I  inputs m and n.So inπ-calculus, the round brackets () are used to both organize the input set of processes and organize the set of messages received through a port. Whereas the angle brackets 〈〉 are used to organize both the input set of process references and the set of messages sent through a port.As described above, theπ-calculus is a process algebra to describe and analyze concurrent systems consisting of processes (or agents) which interact with other connected processes.


### 2.3. Related Work

Some approaches useZ [30] and Object-Z [31] to formalize UML models. Miao et al. [32] deal with the UML class, sequence, and statechart diagrams; while Kim and Carrington [33] present a formal Object-Z model of the UML state machine. However, they consider UML and not UML-RT with its architectural components. That is because Z and Object-Z are suitable for capturing data and states, and not for capturing dynamic communication configurations. On the other hand, π-calculus is suitable to support dynamic communication, that is the focus of our UML-RT formalization proposal. Due to the π-calculus contribution, other formalisms propose the combination of a state-based formalism and a dynamic action-based calculus by integrating the mobility concepts of the π-calculus to Z and Object-Z [34–36].Terriza et al. [16] describe a mapping of UML-RT to CSP + T, whose objective is to provide time elements to UML-RT, making the mapping of the capsule state diagram and the class diagram to CSP + T definitions. CSP + T is a formal specification language that adds time interval description to CSP. Fischer et al. [17] propose the conversion of UML-RT structure diagram to CSP process algebra. Engels et al. [18] describe a translation from the UML-RT capsule state and structure diagrams to CSP. Ramos et al. [19] propose a mapping of UML-RT state, structure, and class diagrams to Circus, which is a formal method that combines concepts of CSP and Z [30].The aforementioned related work deals with synchronous methods. In general, the information in the structure diagram is also provided in the class diagram, and then some authors use one or another. The capsule definition reuse is a criterion that indicates whether the generated definitions in the process algebra can reuse the definition of the capsules. For example, assuming that the capsuleA has two subcapsules of type B, the definition of A in π-calculus references twice the B definition, but for each one, A sets different names as input due to the π-calculus mobility. In CSP and CCS, it would be necessary to write two equations of B, one for each configuration that B may have. An example of this in CSP is the traffic light system in [17].Knapp et al. [23] compile UML-RT state diagram into timed automata and represent the timed-annotated UML collaborations as another timed automaton, using a prototype called HUGO/RT. Afterwards, the prototype calls the model checker UPPAAL to verify the model against the scenario specified by the UML collaboration. Some interesting characteristics include the representation of time considered in a UML-RT timeout and the mapping of the event queue that holds the events not already handled by the machine. However, there are two limitations of this approach. First, the events cannot transmit messages; second, the composite and the choice states are not represented.Additionally, all the above related work considers only the wired ports in their mappings; that is, they do not map the UML-RT unwired ports, so mobility is not addressed.In our previous work, we propose the UML-RT toπ-calculus mapping rules using the π-calculus syntax version accepted by the HAL-JACK tool. The HAL-JACK syntax uses the monoadic π-calculus, which lead us to represent only the communication of one message at a time. Besides, the HAL-JACK syntax requires that all names used in a definition must be declared in its input list; this restriction causes complex mapping rules. In our proposal, we use the π-calculus syntax proposed by Milner and we represent the communication of more than one message through polyadic π-caculus. Other contribution comprises the mapping of the entry and the exit actions, the composite states, and the transition chains.


## 2.1. UML-RT

UML-RT is an extension of UML with elements to facilitate the design of real-time systems. Three of the elements,capsule, port, and connector, are used to model system structure; one element, protocol, models the communication inside the system [11].Acapsule is an active class and represents software components that can be concurrent and physically distributed. A capsule has a state diagram and a structure diagram. A state diagram is similar to a UML standard state diagram and describes the capsule behavior. A structure diagram details the internal structure of a capsule, which includes subcapsules and their connections with each other. Figure 1 shows the structure diagram of the capsule TopSystem that comprises four subcapsules: source (instance of the capsule Source), router (instance of the capsule Router), target1 (instance of the capsule ConsumerTarget), and target2 (instance of the capsule ExporterTarget). The model was constructed using the RoseRT tool.Figure 1
The structure diagram of the capsuleTopSystem.Aport permits to exchange messages between capsules. A protocol needs to be specified for a port. A protocol defines both the number of participants in the communication and the signals that are received and sent by each participant. The connectors act as communicating channels between ports that must play different roles of the same protocol. A line between two ports represents a connector. In Figure 1, the ports q and r implement the protocol named ConfigProtocol, and they are connected to each other. The ports play conjugated roles, which can be noted in their representations: q as an empty (blank) square and r as a filled (black) square.A port can be classified in terms of visibility (public and protected), termination (end and relay), and connectivity (wired and unwired).  A public port is located at the capsule border and can interact with other capsule ports. A protected port is not visible from the outside; it serves as the communication point of the capsule with its subcapsules. In Figure 1, the capsule System has the public port out (indicated by the symbol +), and the protected ports setCT and setET (indicated by the symbol #).With respect to the termination, anend port provides the access to the capsule behavior given by its state diagram. In Figure 1, setCT and setET are end ports of the capsule TopSystem. A relay port is used to export the subcapsule interfaces.  When a relay port of a parent capsule receives a message, the message is passed automatically to the connected subcapsule port. And when a subcapsule sends a message through a port connected to a relay port of its parent capsule, the message is directly sent to the outside of the parent capsule. By definition, a relay port is public and wired. In Figure 1, out is a relay port of the capsule TopSystem.Awired port (e.g., q and r in Figure 1) has a connector joining them to exchange messages. An unwired port does not have a connector with other ports, but it allows dynamic communication during runtime through its name registration. In Figure 1, alert, s, and t are examples of unwired ports. Unwired ports can be registered to receive and send signals. For instance, the port s can be registered with the subscriber name x, and t can be registered with the subscriber name y. In this case, if the port alert is configured with the provider name x, the signal sent by Router along alert is received by ConsumerTarget. Similarly, if the port alert is set to y, its signal is received by ExporterTarget. In RoseRT, the subscriber port is called Service Access Point (SAP) and the provider port is called Service Provisioning Point (SPP).As mentioned, a capsule has also a state diagram. Figure2 presents the state diagram of the ExporterTarget capsule. The initial point (filled circle) is a point which explicitly shows the beginning of the state machine. The initial transition, named Initial, connects the initial point to the initial state. It does not have an associated trigger; however it may execute an associated action.Figure 2
The state diagram of the capsuleExporterTarget.Figure 3
The composite stateS2 of ExporterTarger state diagram.Astate is a condition in which the object is ready to process events. In Figure 2, there are states S1, S2, and S3. We can define actions to be performed when the control enters in a state (entry action, indicated by the symbol  ) and when it leaves a state (exit action, indicated by the symbol  ). A state that does not contain substates is called a simple state. A state that contains substates is called a composite or hierarchical state (indicated by the symbol ). For example, S1 and S3 are simple states; whereas S2 is a composite because it is composed of the simple states S4 and S5 as illustrated in Figure 3. Furthermore, a state can be a choice point, for example, S5, which allows a single transition to be split into two outgoing transition segments, after evaluating a condition on which branch to take. For instance, if the decision evaluation inside S5 returns true, the transition exportMsg is triggered; otherwise, the transition consumeMsg is triggered.Atransition is a relationship between two states: a source state and a destination state. It specifies the change of control from the source state to the destination state when an object in the source state receives a specified event and some conditions are met. Three concepts related to a transition include: trigger, guard condition, and action. Trigger indicates which events (signals) from which interfaces (ports) cause the transition to be taken; however the transition fires only if the guard condition is satisfied. After the transition activation, its action is executed. Actions are operation calls, a variable handling or a signal dispatch to another capsule.Transitions can span multiple hierarchies changing context on the way from the source to the destination state. Therefore they must be partitioned into different segments by the junction pointers. Each transition segment has a distinct name. Any segment can execute actions; however only the originating segment has a trigger. For instance, the transitionconfigPort illustrated in Figure 2 connects the states S1 and S2, but it comprises two segments inside the state S2 as shown in Figure 3: the transition configPort itself and the transition Initial1 separated by a junction pointer.It is important to mention that the triggers and the actions are configured internally in the RoseRT tool, and the model screenshot presents only the state and transition names. Table1 presents the transition information of the ExporterTarget state diagram, where the action is specified in C programming language. For example, the transition configPort triggers if it receives along the port setPort the signal portName. The transition action is the storage of the message, received through the port setPort, in the local variable aux using the statement “aux = *rtdata;”. Later the port t is renamed to aux, using the statement “t·registerSAP(aux);”. The transition exportMsg does not have a trigger, but it executes an action of sending along the port export the signal msg with the message d1.Table 1
Transitions of theExporterTarget state diagram.
TransitionTriggerActionInitial——configPortPort:setPortSignal:portNamet·registerSAP(aux);Initial1—Initial2—receiveMsgPort:tm = *rtdata;d1 = m·msg1;Signal:msgd2 = m·msg2;consumeMsg—exportMsg—export·msg(d1)·send();msgConsumed—msgExported—waitMsgPort:timer—Signal:timeoutUML-RT allows defining a class and sending an object of this class as a message. For example, the capsuleExportedTarget receives a message m in the transition receiveMsg with the attributes msg1 and msg2, which are stored, respectively, in d1 and d2 variables, according to Table 1. Later, by the transition exportMsg, the capsule ExportedTarget is able to send the message d1. However, the message m can be seen as two messages m1 and m2 transmitted in a single signal, which characterizes the communication of more than one message at a time in UML-RT.Although, there are other diagrams available in the UML-RT, such as use case, component, deployment, class, collaboration, and sequence diagrams; the proposed mapping rules deal only with the state and structure diagrams of UML-RT capsules.A use case diagram is specially used before the modeling phase in order to identify the functionality of the system. A component diagram shows the dependencies among software components that exist at compilation time, linking time, or run-time. A deployment diagram captures the physical distribution of the run-time processes across a set of processing nodes. As our scope is focused on design, and not on the requirement or implementation, the use case, component, and deployment diagrams are not addressed.A class diagram shows the static structure of the model. It may contain other elements besides classes, such as capsules and protocols. A collaboration diagram captures a desirable pattern of interactions between objects, emphasizing the structural organization of the objects. A capsule structure diagram is a specialized form of the collaboration diagram and includes information available also in the class diagram. A sequence diagram specifies communication scenarios of collaboration; however with the capsule structure diagram and the state diagram of each capsule it is possible to obtain all the possible collaborations; therefore the sequence diagram is not used. So our mapping considers only the state and structure diagrams of UML-RT capsules.


## 2.2. Theπ-Calculus

Theπ-calculus [24] is a process algebra for systems that communicate concurrently, that is, systems composed of processes that run in parallel and interact through channels. The main difference between π-calculus and its predecessors, CSP and CCS, is the possibility to pass channels as data through channels [27–29]. This characteristic allows the π-calculus to express mobility.The prefixπ of the π-calculus represents x̅〈y〉, x(y), or the unobservable action τ. The term x̅〈y〉 indicates that the π-calculus port (or channel) x sends the π-calculus message y. The term x(y) indicates that the message y is received along the port x. The round brackets (y) are used for the binding occurrence of a parametric name (one that may be instantiated by another name), and the angle brackets 〈y〉 for nonbinding occurrences of a name.Theπ-calculus process expression P is defined by the syntax:
(1)P:=∑i∈Iπi·Pi∣P1∣P2∣newaP∣!P.The term∑i∈Iπi·Pi indicates summation, where I is a finite indexing set. The dot is the sequence operation, which means that πi will occur before Pi becomes activated.  If i=2, we have π1·P1+π2·P2. If i=0, we have P=0, that is a stop process. In general, we omit the stop process, for example, we write x(y) instead of x(y)·0. The parallel composition P1∣P2 means that P1 and P2 run concurrently. The term new a P represents the restriction of the name a in the P context, that is, the name a is bound in P and it is not seen outside. The replication operator !P is the composition of unlimited copies of P.For example, considering the following processes ofB, C, D, and E, where
(2)B=(z̅〈x〉+z̅〈y〉),(3)C=z(a)·a̅〈b〉,(4)D=x(c),(5)E=y(d).The processB is able to send the message x along the port z or to send the message y along the port z. The process C can receive a message a through the port z, and later send the message b through the port a. The process D can only receive a message c along the port x. Finally, the process E is able to receive a message d via the port y.Assuming that the processA (Figure 4(a)) consists of B, C, D, and E above, so by using π-calculus, the process A is the parallel composition of the four processes:
(6)A=B∣C∣D∣E.Theπ-calculus mobility. (a) A process,  (b) A1 process, and  (c) A2 process.
(a)(b)(c)We can replace in (6) the definition of each process using (2) to (5), so
(7)A=(z̅〈x〉+z̅〈y〉)∣z(a)·a̅〈b〉∣x(c)∣y(d).To understand how to manipulate the definitions included in the processA definition, it is necessary to understand the π-calculus concepts related to the structural congruence and the reactions.The processesP and Q in the π-calculus are structurally congruent, written P≡Q, if one can be transformed into the other using the rules.(i) Change of Bound Names (Alpha-Conversion).
The alpha-conversion allows bound variable names to be renamed. As an example, in (2), we have that D=x(c). If D′=x(c), so D≡D′, that is, D is the same as D′.(ii) Reordering Terms in a Summation
The reordering terms in a summation are related to the commutative operations. For instance, in (1), we have that B=(z̅〈x〉+z̅〈y〉). But we can rewrite B by reordering its terms, so B=(z̅〈y〉+z̅〈x〉).(iii)P∣0≡P,P∣Q≡Q∣P,P∣(Q∣R)≡(P∣Q)∣R
The first term indicates that the stop process is the neutral element in the parallel composition. The second and the third terms are the commutative and the associative operation, respectively, of the parallel composition. For example, the definition ofA in (6) can also be written by reordering B and C, as A=C|B|D|E.(iv) newx(P∣Q)≡P∣ new xQ, If x Is not a Free Name of P
It states that if a processP does not have the free name x, the restriction of x in the parallel composition P∣Q is kept only in Q.(v)newx0≡0, and newx,yP≡newy,xP
The first term explains that there is no need to use restriction in the stop process. The second term indicates that the order of the names in a restriction operation is not important.(vi)!P≡P∣!P
It states that the replication ofP is the same as a parallel composition of an infinite number of P.The reaction relation overπ-calculus explains how the processes react with each other. It contains exactly the transitions which can be inferred from the following rules.(i) TAU [τ·P+M→P]
It states that in a processτ·P+M, if τ occurs, then we choose the first option of the choice operator and the result is only the P process.(ii) REACT [(x(y)·P+M)∣(x̅〈z〉·Q+N)→{z/y}P∣Q, Where {z/y}P Means that y Must Be Replaced by z]
It states that the two processes running concurrently(x(y)·P+M) and (x̅〈z〉·Q+N) may react, because the second process sends the message z along the port x, while the first process receives a message y along the port x. After the reaction, all occurrences of y in the first process are renamed by z.(iv) PAR [IfP→P′, Then P∣Q→P′∣Q]
It states that in a parallel composition, if one process transits to another, then the parallel composition is maintained.(v) RES [IfP→P′, Then newxP→newxP′]
It states that in a restriction operation, if one process transits to another, then the restriction is maintained.(vi) STRUCT [P→P′ Implies Q→Q′, if P≡Q, P′≡Q′]
It states that ifP transits to P′ it implies that Q transits to Q′, then P and Q are structurally congruent.In the example of the processA defined in (7), the actions z̅〈x〉 of B and z(a) of C are complementary and may interact generating A1:
(8)A1=0∣x̅〈b〉∣x(c)∣y(d).After the reactionA→A1, all occurrences of a in C are replaced by x. Figure 4(b) shows A1 process, where U=x̅〈b〉 and B is not represented because it is a stop process.Additionally, there is another possible interaction inA between z̅〈y〉 of B and z(a) of C, generating A2:
(9)A2=0∣y̅〈b〉∣x(c)∣y(d).After the reactionA→A2, all occurrences of a in C are replaced by y. Figure 4(c) depicts A2 process, where V=y̅〈b〉 and B is not represented because it is a stop process.The example illustrates theπ-calculus mobility concept, because the channels x (in the reaction A→A1) and y (in the reaction A→A2) are passed as message along the channel z, which links processes B and C. The mobility is the main aspect of the π-calculus whose representation is addressed in this paper.The presentedπ-calculus version is the monoadic π-calculus, in which a message contains exactly one name. The polyadic π-calculus [24] permits to exchange messages consisting of more than one name, using the prefixes x(y⃗) and x̅〈z⃗〉. In particular, it admits the cases x() and x̅〈〉 where y⃗ and z⃗ are empty, and we can write as x and x̅ to indicate only the synchronization between the ports.For an example of polyadicπ-calculus, consider the following process:
(10)E=x(y1,y2)·F∣x̅〈z1,z2〉·G∣x̅〈w1,w2〉·H.The first term in (10) may react with the second or the third term along the port x. The reaction with the second term replaces y1,y2 by z1,z2, respectively. While the reaction with the third term replaces y1,y2 by w1,w2, respectively.The definition ofE is different from E′ written in monoadic π-calculus, as follows:
(11)E′=x(y1)·x(y2)·F∣x̅〈z1〉·x̅〈z2〉·G∣x̅〈w1〉·x̅〈w2〉H.In (11), the first term may react with the second and later with the third term, resulting that y1 is replaced by z1, and y2 by w2. It is also possible that the first term may react with the third and later with the second term. In both cases, the result of (11) using monoadic π-calculus is different from that one expected in (10) using polyadic π-calculus. For the correct encoding of the polyadic using monoadic, it is necessary to guarantee that there can be no interference on the channel along which a composite message is sent. It is addressed by Milner in [24].A process in monoadic or polyadicπ-calculus can also have a list of input names written between round brackets, for example,
(12)I(m,n)=m̅〈n〉·I′.In this case, the definition of processI has the port name m and the message n available as input parameters. If a process J uses the definition of I, then J calls I definition passing the input names between angle brackets, for example,
(13)J(p)=p(q)·I〈q,r〉.In (13), J references I definition passing q and r to, respectively, rename I  inputs m and n.So inπ-calculus, the round brackets () are used to both organize the input set of processes and organize the set of messages received through a port. Whereas the angle brackets 〈〉 are used to organize both the input set of process references and the set of messages sent through a port.As described above, theπ-calculus is a process algebra to describe and analyze concurrent systems consisting of processes (or agents) which interact with other connected processes.


## 2.3. Related Work

Some approaches useZ [30] and Object-Z [31] to formalize UML models. Miao et al. [32] deal with the UML class, sequence, and statechart diagrams; while Kim and Carrington [33] present a formal Object-Z model of the UML state machine. However, they consider UML and not UML-RT with its architectural components. That is because Z and Object-Z are suitable for capturing data and states, and not for capturing dynamic communication configurations. On the other hand, π-calculus is suitable to support dynamic communication, that is the focus of our UML-RT formalization proposal. Due to the π-calculus contribution, other formalisms propose the combination of a state-based formalism and a dynamic action-based calculus by integrating the mobility concepts of the π-calculus to Z and Object-Z [34–36].Terriza et al. [16] describe a mapping of UML-RT to CSP + T, whose objective is to provide time elements to UML-RT, making the mapping of the capsule state diagram and the class diagram to CSP + T definitions. CSP + T is a formal specification language that adds time interval description to CSP. Fischer et al. [17] propose the conversion of UML-RT structure diagram to CSP process algebra. Engels et al. [18] describe a translation from the UML-RT capsule state and structure diagrams to CSP. Ramos et al. [19] propose a mapping of UML-RT state, structure, and class diagrams to Circus, which is a formal method that combines concepts of CSP and Z [30].The aforementioned related work deals with synchronous methods. In general, the information in the structure diagram is also provided in the class diagram, and then some authors use one or another. The capsule definition reuse is a criterion that indicates whether the generated definitions in the process algebra can reuse the definition of the capsules. For example, assuming that the capsuleA has two subcapsules of type B, the definition of A in π-calculus references twice the B definition, but for each one, A sets different names as input due to the π-calculus mobility. In CSP and CCS, it would be necessary to write two equations of B, one for each configuration that B may have. An example of this in CSP is the traffic light system in [17].Knapp et al. [23] compile UML-RT state diagram into timed automata and represent the timed-annotated UML collaborations as another timed automaton, using a prototype called HUGO/RT. Afterwards, the prototype calls the model checker UPPAAL to verify the model against the scenario specified by the UML collaboration. Some interesting characteristics include the representation of time considered in a UML-RT timeout and the mapping of the event queue that holds the events not already handled by the machine. However, there are two limitations of this approach. First, the events cannot transmit messages; second, the composite and the choice states are not represented.Additionally, all the above related work considers only the wired ports in their mappings; that is, they do not map the UML-RT unwired ports, so mobility is not addressed.In our previous work, we propose the UML-RT toπ-calculus mapping rules using the π-calculus syntax version accepted by the HAL-JACK tool. The HAL-JACK syntax uses the monoadic π-calculus, which lead us to represent only the communication of one message at a time. Besides, the HAL-JACK syntax requires that all names used in a definition must be declared in its input list; this restriction causes complex mapping rules. In our proposal, we use the π-calculus syntax proposed by Milner and we represent the communication of more than one message through polyadic π-caculus. Other contribution comprises the mapping of the entry and the exit actions, the composite states, and the transition chains.


## 3. The UML-RT to Polyadicπ-Calculus Mapping

In this section, we propose the mapping from the UML-RT to theπ-calculus. We make some initial considerations regarding the mapping, and later we explain the mappings of the following elements of UML-RT: capsule, structure diagram, state diagram, state, and transition.


### 3.1. Initial Considerations

The processing of a single event at a time by a state machine is known as a run-to-completion (RTC) step, which means that a transition cannot be interrupted by the arrival of an event. When the transition is partitioned into different segments, in the case of the composite states, only the originating segment has a trigger defined, so there is only one event to be processed. So, even in this case, the transition chain (i.e., the sum of all transition segments) is executed in one RTC step. The communication model used by theπ-calculus is the synchronized communication, which is suitable to the RTC step, because the object corresponding to the sender state diagram blocks until it receives the notification about the receipt of the event at the object corresponding to the receiver state diagram.The polyadicπ-calculus definitions resulted from the mapping follow the syntax proposed by Milner [24].  The UML-RT capsule state diagrams are used in the mapping to retrieve the behavior of the capsules, while the structure diagrams are used to retrieve the association between capsules. The base of the mapping is that a UML-RT port is represented by a π-calculus port; whereas the messages transmitted through the signal are represented by the π-calculus messages. In order to be able to represent the transmission of zero or more messages, our approach uses the polyadic π-calculus.UML-RT offers a limited support for time annotations, there is one element to set a timer and simulate a timeout. In the RoseRT tool, this timer is allowed through a port that implements a built-inTiming protocol. In our mapping, the timeout is represented by the unobservable action τ, because it is a private interaction inside the capsule.The main elements of a transition are trigger, action, and guard condition. However, as the focus of the UML-RT toπ-calculus mapping is on communication elements, guard condition is not considered. The transition is triggered by the receipt of a message. The considered transition actions are a message sending or a name reconfiguration, where a name reconfiguration is a way to reconfigure the unwired ports. We assume that the entry and exit actions are only the message sending statements.The RoseRT tool allows the use of three programming languages, C, C++, and Java, to specify the transition and the state actions. Aiming to be independent from programming languages and simplify the notation used in the mapping rules, we propose the following pseudo codes.(i)
The message receipt statement is written as “preceivee(m⃗)”, which means that the port p receives the signal e with the list m⃗ of messages.(ii)
The message sending statement is represented as “psende(m⃗)”, that is, the port p  sends the signal e with the list m⃗ of messages.(iii)
The name reconfiguration statement is written as “name1 = name2”, that is, name1 is from now on used with the value of name2. In the RoseRT, this information is given through the commands SAP or SPP, for example, “name1·registerSAP(name2)”.It is important to recall that the listm⃗ of messages can be empty, when there exists only the synchronization between the ports and no message is transmitted.Some notations used in the mapping rules need to be presented.(i)
The termP(L) represents the π-calculus definition of P with its input set L.(ii)
The termP〈L〉 represents a reference to the π-calculus definition of P. The input set L is passed to the P definition. This notation is used in the syntax proposed by Milner and is commented in Section 2.2.(iii)
The termP represents the π-calculus definition of a component without a defined input set. Each π-calculus reference to this component should be replaced by the definition P.(iv)
The result ofL1-L2 is L1 without the elements contained in L2, where L1 and L2 are sets.(v)
The symbol⋃ is the union operator in sets. So, ⋃i∈NLi=L1∪L2∪⋯∪LN.(vi)
The symbol∑ indicates the application of the choice operator in π-calculus processes. So, ∑i∈NPi=P1+P2+⋯+PN.(vii)
The symbol∏ indicates the application of the sequence operator in π-calculus actions. So, ∏i∈Nπi=π1·π2⋯πN.The result of UML-RT mapping is theπ-calculus definition of the main capsule in UML-RT model. After introducing the essence of the mapping and the notations, we are able to present the capsule mapping.


### 3.2. Capsule Mapping

Each UML-RT capsule has its own state diagram and may contain other capsules in its structure diagram. So, the capsule definition in theπ-calculus is composed by two parts: the structure diagram definition in the π-calculus and the state diagram definition in the π-calculus. These two definitions are arranged with the parallel composition operator of the π-calculus, as presented in Definition 1, because the behavior of the capsule and its subcapsules are executed concurrently in UML-RT.Definition 1 (Capsule definition).
Given a capsuleP, its π-calculus definition is the parallel composition of its state diagram definition and its structure diagram definition. So, the π-calculus definition of the capsule P is given by
(14)P(InputSet[P])=new(RestrictedSet[P])·(P_StructureDiagram∣P_StateDiagram),
where
(i)
InputSet[P]  is the input message set of the P capsule definition. It is defined as the set of the public wired ports of the capsule P.(ii)
RestrictedSet[P] is the set  of messages restricted to the context of the capsule P. Assuming that P has N subcapsules Qi, the restricted set is defined as
(15)RestrictedSet[P]=⋃i∈N(InputSet[P,Qi])-InputSet[P].(iii)
InputSet[P,Qi]: input set used by the parent capsule P to reference the definition of its subcapsule Qi. It is defined in the structure diagram mapping.
In the example presented in Figure1, using Definition 1, the main capsule is TopSystem and its π-calculus definition can be written as
(16)TopSystem(InputSet[TopSystem])=new(RestrictedSet[TopSystem])(TopSystem_StructureDiagram∣TopSystem_StateDiagram)InputSet[TopSystem]={out}RestrictedSet[TopSystem]={InputSet[TopSystem,Source]∪InputSet[TopSystem,Router]∪InputSet[TopSystem,ConsumerTarget]∪InputSet[TopSystem,ExportedTarget]}-{out}.
In order to specify the capsule definition, the next sections explain how to obtain theπ-calculus definitions for the structure diagram and the state diagram.


### 3.3. Structure Diagram Mapping

A capsule may include subcapsules in its structure diagram. If the structure diagram of a capsule does not have subcapsules, this diagram is defined in theπ-calculus as the stop process. In this case, the capsule definition is composed only by the state diagram definition, because the parallel composition between a process and a stop process is the first process. However, if the capsule has subcapsules, its structure diagram definition is the π-calculus parallel composition of the subcapsules’ definitions, as explained in Definition 2, because all UML-RT subcapsules execute concurrently. In this case, the definition of each subcapsule has to be written using Definition 1 and the connections between ports are used to specify how the parent capsule references its subcapsules.Definition 2 (Structure diagram definition).
Given a capsuleP. If P does not have subcapsules, the π-calculus definition of the P structure diagram is the stop process:
(17)P_StructureDiagram=0.
Otherwise, if P has subcapsules, given a set N of subcapsules Qi of P. Given the π-calculus definition of each subcapsule Qi as Qi(InputSet[Qi. ]), the π-calculus definition of the P structure diagram is given by
(18)P_StructureDiagram=Q1〈InputSet[P,Q1]〉∣⋯∣QN〈InputSet[P,QN]〉,
where the InputSet[P,Q1] is defined based on the connection between the wired ports as follows.
(a)
If the portp of the parent capsule P is connected to the public port q1 of the subcapsule Q1, the port q is renamed to p. So,  p∈InputSet[P,Qi].(b)
If the public portq1 of the subcapsule Q1 is connected to the public port q2 of the subcapsule Q2, a new name z is generated dynamically to rename the ports q1 and q2. So,
(19)z∈InputSet[P,Q1],z∈InputSet[P,Q2].In the example shown in Figure1, according to Definition 2, the π-calculus definition of TopSystem structure diagram is the parallel composition of the definition of the subcapsules: Source, Router, ConsumerTarget, and ExporterTarget.  Considering the input sets used by TopSystem to reference its subcapsules, we have that the port setPort of ConsumerTarget is renamed to parent port setCT, the port setPort of ExporterTarget is renamed to parent port setET, and the new name z is created to rename the q1 and r1. So, TopSystem structure diagram is defined as
(20)TopSystem_StructureDiagram=Source〈z〉∣Router〈z〉∣ConsumerTarget〈setCT〉∣ExporterTarget〈setET,out〉.In order to complete the capsule definition inπ-calculus, the next section presents how to obtain the state diagram definition.


### 3.4. State Diagram Mapping

A capsule can specify or not an associated state diagram. If it is not specified, theπ-calculus definition of the capsule state diagram is the stop process. Otherwise, if the capsule has a state diagram, it is composed by states and transitions between them. The first transition to be activated is the initial transition, which is connected to the initial state.  As explained in Section 2.1, the initial transition does not have a trigger, it runs automatically when the state diagram initializes, but it can execute an action. So, the π-calculus definition of the state diagram is the sequence composition between the definition of initial transition action and the definition of the initial state, as explained in Definition 3.Definition 3 (State diagram definition).
Given a capsuleP. If P does not have a state diagram, the π-calculus definition of the state diagram is the stop process:
(21)P_StateDiagram=0.
Otherwise, if P has a state diagram, assuming that InitialTransition is the initial transition and S1 is the initial state, the π-calculus definition of the state diagram is given by
(22)P_StateDiagram=P_InitialTransition_Action·P_S1〈InputSet[P,InitialPoint,S1]〉.
where InputSet[P,InitialPoint,S1] is the input message set used by the initial transition definition to reference the definition of the state S1. It is defined in the transition action mapping.The definition of the initial transition action is explained in the transition action mapping, and the definition of the initial state is explained in the state mapping. Note that the initial transition trigger is not mentioned in Definition3, because the initial transition does not have a trigger, it runs automatically when the state diagram initializes. The definitions of the other states reachable from the initial state, which are included in the capsule state diagram, are considered in the definition of the initial state.In the example presented in Figure2, the ExporterTarget state diagram is defined, using Definition 3 as
(23)ExporterTarget_StateDiagram=ExporterTarget_Initial_Action·ExporterTarget_S1·〈InputSet[ExporterTarget,InitialPoint,S1]〉.According to Definition3, the state diagram definition references the initial state definition, which depends on the other states and transitions in the state diagram. So, the next section details the state and transition mapping.


### 3.5. State Mapping

The name of a UML-RT state in theπ-calculus definition is specified as the concatenation of the UML-RT capsule name and the UML-RT state name to guarantee unique definitions in π-calculus. An entry action is executed whenever the state is entered; regardless of which incoming transition is taken. Besides, a state has multiple outgoing transitions which can be taken. So, the π-calculus definition of the UML-RT state, as explained in Definition 4, is the sequence composition between its entry action definition and the choice composition of each transition definition.Definition 4 (Simple state definition).
Given a simple stateS in the state diagram of a capsule P, and given InputSet[P,S]. Assuming that the state S has an entry action and a set T of outgoing transitions, the π-calculus definition of the state S is given by
(24)P_S(InputSet[P,S])=P_S_EntryAction·∑i∈T(P_S_OutgoingTransitioni),
where InputSet[P,S] is the input message set of  the S definition. It is defined in the transition action mapping.For instance, in Figure2, the S1 definition can be written using Definition 4 as
(25)ExporterTarget_S1(InputSet[ExporterTarget,S1])=ExporterTarget_S1_EntryAction·P_S1_configPort.The UML-RT choice point is a special case of UML-RT state, where there is no entry and exit action, and the transition does not have a trigger, because it is enabled according to the condition specified in the choice point. So, Definition4 can be used to provide the π-calculus definition of a choice point too.According to Definition4, the entry action definition is a part of the state definition. The exit action definition is used only in the transition definition. The entry (or exit) action may not exist in a UML-RT state, so its reference is omitted from the state (or transition) definition. Whether the state performs an entry or exit actions, they include message sending actions in UML-RT, then the π-calculus definition of the entry and exit actions are the sequence composition of the message sending actions. The definition of a state action is provided in Definition 5 and may represent the definition of an entry action or an exit action.Definition 5 (State action definition).
Given a stateS in the state diagram of a capsule P, the state action can be an entry action and an exit action.
If the state action is not defined forS, the π-calculus reference to the state action definition is omitted from the parent definition.
Otherwise, if the state action is specified as a setN of message sending actions “pi sendei(m⃗i)”, the π-calculus definition of the state action is given by
(26)P_S_StateAction=∏i∈N(p̅i〈m⃗i〉).After presenting the state mapping, the next section explains the transition mapping.


### 3.6. Transition Mapping

In a UML-RT model, the transition has an associated trigger and may execute an action after being activated. Considering the state with its outgoing transitions, it is important to mention that the state exit action is taken whenever the control leaves the state from whatever outgoing transition; so the state exit action has to be computed after the transition trigger and before the transition action. Then, the outgoing transition definition in theπ-calculus, as detailed in Definition 6, is a sequence composition of the transition trigger definition, the state exit action, the transition action definition, and the target state definition.Definition 6 (Outgoing transition definition).
Given the simple statesS1 and S2 in the state diagram of a capsule P. Given an outgoing transition from S1 to S2, the π-calculus definition of the transition is
(27)P_S1_OutgoingTransition=P_S1_OutgoingTransition_Trigger·P_S1_ExitAction·P_S1_OutgoingTransition_Action·P_S2〈InputSet[P,S1,S2]〉,
where InputSet[P,S1,S2] is the input message set used by the state S1 to reference the definition of the state S2. It is defined in the transition action mapping.For instance, the transitionreceiveMsg can be defined, using Definition 6, as
(28)ExporterTarget_S4_receiveMsg=ExporterTarget_S4_receiveMsg_Trigger·ExporterTarget_S4_ExitAction·ExporterTarget_S4_receiveMsg_Action·ExporterTarget_S5〈InputSet[ExporterTarget,S4,S5]〉.A special case of a UML-RT transition is when the transition is a transition chain that transposes the boundaries of composite states. As it is explained in Section2.1, this transition is partitioned into different segments by the junction pointers, and only the originating segment has a trigger defined, while all segments can execute actions. In this case, we have to compute in the right order the following aspects: the trigger of the first segment, the actions of all segments, the entry or the exit action of all the transposed parent states, as detailed in Definition 7.Definition 7 (Definition of the outgoing transition chain).
Given an outgoing transition chain from a stateS1 to a state S2, where S1 and S2 belong to the state diagram of a capsule P. Assuming that the outgoing transition chain transposes the boundary of a set N of the parent states CS1’s of S1, and later transposes the boundary of a set M of the parent states CS2’s of S2, where N or M can be empty sets, the transition chain is composed by N+M+1 segments. In this case, the π-calculus definition of the outgoing transition chain is given by
(29)P_S1_OutgoingTransitionChain=P_S1_Segment1_Trigger·P_S1_ExitAction·P_S1_Segment1_Action·(P_S1_OutgoingTransitionChain_Up·P_S1_OutgoingTransitionChain_Down)·P_S2〈InputSet[P,S,S2]〉,
where
(30)P_S1_OutgoingTransitionChain_Up=∏i∈N(P_CS1i_ExitAction·P_S1_Segmenti+1_Action)P_S1_OutgoingTransitionChain_Down=∏j∈M(P_CS2j_EntryAction·P_S1_Segmentj+1+N_Action).TheExporterTarget state diagram, illustrated in Figures 2 and 3, has the transition chain initiating with the segment consumeMsg. This transition chain originates at the state S5 and transposes the boundary of the composite state S2 until reaching the state S3. According to Definition 7, the transition chain consumeMsg is defined as
(31)ExportedTarget_S5_consumeMsg=ExportedTarget_S5_consumeMsg_Trigger·ExportedTarget_S5_ExitAction·ExportedTarget_S5_consumeMsg_Action·ExportedTarget_S2_ExitAction·ExportedTarget_S5_msgConsumed_Action·ExportedTarget_S3〈InputSet[ExporterTarget,S5,S3]〉.As commented in Section3.1, the transition trigger is a message receipt statement and the transition action can be a message sending statement or a name reconfiguration statement. The transition trigger definition is provided in Definition 8, while the transition action definition is explained in Definition 9.Definition 8 (Transition trigger definition).
Given a transition from stateS1 to stateS2 in the state diagram of a capsule P.
If there is no trigger specified to the transition, theπ-calculus reference to the transition trigger definition is omitted from the parent definition.
Otherwise, assuming that the transition can be triggered by a setN of message receipt statements as “pireceiveei(m⃗i)”, the π-calculus definition of the transition trigger is given by
(32)P_S1_Transition_Trigger=∑i∈N(pi(m⃗i)).
A special case occurs when ei is a timeout signal. In this case, the trigger is represented by the unobservable action τ. So,  pi(m⃗i)=τ.Analyzing Definition8, the transition trigger definition considers all the messages that the capsule can receive in the current transition. However, it cannot be defined, for example, in an outgoing transition of a choice point and in the first segment of a transition chain.In Definition9, the transition action considers all the message sending and the reconfiguration statements. In case of a reconfiguration statement, it is important that the old name is the one used by the next state, while the new name is used to reference the next state definition. The input message set of the capsule definition is maintained in the other input sets to keep the consistence of the π-calculus definitions. Note that Definition 9 holds to the actions of all segments in a transition chain.Definition 9 (Transition action definition).
Given a transition from stateS1 to state S2 in the state diagram of a capsule P.
If there is no action associated to the transition, theπ-calculus reference to the transition action definition is omitted from the parent definition.
Otherwise, assuming that the transition action is composed of a setN of message sending statements as “pisendei(m⃗i)” and also by a set M of name reconfiguration statements as “yj=xj”, the π-calculus definition of the transition action is given by
(33)P_S1_Transition_Trigger=∏i∈N(p̅i〈m⃗i〉),InputSet[P,S1,S2]=⋃j∈Mxj∪InputSet[P],InputSet[P,S2]=⋃j∈Myj∪InputSet[P],
where InputSet[P] is the input message set of the P capsule definition, already defined in Definition 1.For instance, the transitionreceiveMsg of the ExporterTarget state diagram, illustrated in Figure 3, has a trigger which can be defined using Definition 8 as follows:
(34)ExporterTarget_S4_receiveMsg_Trigger=t(d1,d2).It is an example of receiving two messages in a single synchronization, which shows the importance of using polyadicπ-calculus in the mapping.As an example to apply Definition9, consider the transition segment exportMsg. So,
(35)ExporterTarget_S5_exportMsg_Action()=export¯〈d1〉.The next section presents three examples that illustrate how the mapping rules can be applied to obtain theπ-calculus definitions from a UML-RT model, and how to manipulate the generated π-calculus definitions in order to verify some system requirements.


## 3.1. Initial Considerations

The processing of a single event at a time by a state machine is known as a run-to-completion (RTC) step, which means that a transition cannot be interrupted by the arrival of an event. When the transition is partitioned into different segments, in the case of the composite states, only the originating segment has a trigger defined, so there is only one event to be processed. So, even in this case, the transition chain (i.e., the sum of all transition segments) is executed in one RTC step. The communication model used by theπ-calculus is the synchronized communication, which is suitable to the RTC step, because the object corresponding to the sender state diagram blocks until it receives the notification about the receipt of the event at the object corresponding to the receiver state diagram.The polyadicπ-calculus definitions resulted from the mapping follow the syntax proposed by Milner [24].  The UML-RT capsule state diagrams are used in the mapping to retrieve the behavior of the capsules, while the structure diagrams are used to retrieve the association between capsules. The base of the mapping is that a UML-RT port is represented by a π-calculus port; whereas the messages transmitted through the signal are represented by the π-calculus messages. In order to be able to represent the transmission of zero or more messages, our approach uses the polyadic π-calculus.UML-RT offers a limited support for time annotations, there is one element to set a timer and simulate a timeout. In the RoseRT tool, this timer is allowed through a port that implements a built-inTiming protocol. In our mapping, the timeout is represented by the unobservable action τ, because it is a private interaction inside the capsule.The main elements of a transition are trigger, action, and guard condition. However, as the focus of the UML-RT toπ-calculus mapping is on communication elements, guard condition is not considered. The transition is triggered by the receipt of a message. The considered transition actions are a message sending or a name reconfiguration, where a name reconfiguration is a way to reconfigure the unwired ports. We assume that the entry and exit actions are only the message sending statements.The RoseRT tool allows the use of three programming languages, C, C++, and Java, to specify the transition and the state actions. Aiming to be independent from programming languages and simplify the notation used in the mapping rules, we propose the following pseudo codes.(i)
The message receipt statement is written as “preceivee(m⃗)”, which means that the port p receives the signal e with the list m⃗ of messages.(ii)
The message sending statement is represented as “psende(m⃗)”, that is, the port p  sends the signal e with the list m⃗ of messages.(iii)
The name reconfiguration statement is written as “name1 = name2”, that is, name1 is from now on used with the value of name2. In the RoseRT, this information is given through the commands SAP or SPP, for example, “name1·registerSAP(name2)”.It is important to recall that the listm⃗ of messages can be empty, when there exists only the synchronization between the ports and no message is transmitted.Some notations used in the mapping rules need to be presented.(i)
The termP(L) represents the π-calculus definition of P with its input set L.(ii)
The termP〈L〉 represents a reference to the π-calculus definition of P. The input set L is passed to the P definition. This notation is used in the syntax proposed by Milner and is commented in Section 2.2.(iii)
The termP represents the π-calculus definition of a component without a defined input set. Each π-calculus reference to this component should be replaced by the definition P.(iv)
The result ofL1-L2 is L1 without the elements contained in L2, where L1 and L2 are sets.(v)
The symbol⋃ is the union operator in sets. So, ⋃i∈NLi=L1∪L2∪⋯∪LN.(vi)
The symbol∑ indicates the application of the choice operator in π-calculus processes. So, ∑i∈NPi=P1+P2+⋯+PN.(vii)
The symbol∏ indicates the application of the sequence operator in π-calculus actions. So, ∏i∈Nπi=π1·π2⋯πN.The result of UML-RT mapping is theπ-calculus definition of the main capsule in UML-RT model. After introducing the essence of the mapping and the notations, we are able to present the capsule mapping.


## 3.2. Capsule Mapping

Each UML-RT capsule has its own state diagram and may contain other capsules in its structure diagram. So, the capsule definition in theπ-calculus is composed by two parts: the structure diagram definition in the π-calculus and the state diagram definition in the π-calculus. These two definitions are arranged with the parallel composition operator of the π-calculus, as presented in Definition 1, because the behavior of the capsule and its subcapsules are executed concurrently in UML-RT.Definition 1 (Capsule definition).
Given a capsuleP, its π-calculus definition is the parallel composition of its state diagram definition and its structure diagram definition. So, the π-calculus definition of the capsule P is given by
(14)P(InputSet[P])=new(RestrictedSet[P])·(P_StructureDiagram∣P_StateDiagram),
where
(i)
InputSet[P]  is the input message set of the P capsule definition. It is defined as the set of the public wired ports of the capsule P.(ii)
RestrictedSet[P] is the set  of messages restricted to the context of the capsule P. Assuming that P has N subcapsules Qi, the restricted set is defined as
(15)RestrictedSet[P]=⋃i∈N(InputSet[P,Qi])-InputSet[P].(iii)
InputSet[P,Qi]: input set used by the parent capsule P to reference the definition of its subcapsule Qi. It is defined in the structure diagram mapping.
In the example presented in Figure1, using Definition 1, the main capsule is TopSystem and its π-calculus definition can be written as
(16)TopSystem(InputSet[TopSystem])=new(RestrictedSet[TopSystem])(TopSystem_StructureDiagram∣TopSystem_StateDiagram)InputSet[TopSystem]={out}RestrictedSet[TopSystem]={InputSet[TopSystem,Source]∪InputSet[TopSystem,Router]∪InputSet[TopSystem,ConsumerTarget]∪InputSet[TopSystem,ExportedTarget]}-{out}.
In order to specify the capsule definition, the next sections explain how to obtain theπ-calculus definitions for the structure diagram and the state diagram.


## 3.3. Structure Diagram Mapping

A capsule may include subcapsules in its structure diagram. If the structure diagram of a capsule does not have subcapsules, this diagram is defined in theπ-calculus as the stop process. In this case, the capsule definition is composed only by the state diagram definition, because the parallel composition between a process and a stop process is the first process. However, if the capsule has subcapsules, its structure diagram definition is the π-calculus parallel composition of the subcapsules’ definitions, as explained in Definition 2, because all UML-RT subcapsules execute concurrently. In this case, the definition of each subcapsule has to be written using Definition 1 and the connections between ports are used to specify how the parent capsule references its subcapsules.Definition 2 (Structure diagram definition).
Given a capsuleP. If P does not have subcapsules, the π-calculus definition of the P structure diagram is the stop process:
(17)P_StructureDiagram=0.
Otherwise, if P has subcapsules, given a set N of subcapsules Qi of P. Given the π-calculus definition of each subcapsule Qi as Qi(InputSet[Qi. ]), the π-calculus definition of the P structure diagram is given by
(18)P_StructureDiagram=Q1〈InputSet[P,Q1]〉∣⋯∣QN〈InputSet[P,QN]〉,
where the InputSet[P,Q1] is defined based on the connection between the wired ports as follows.
(a)
If the portp of the parent capsule P is connected to the public port q1 of the subcapsule Q1, the port q is renamed to p. So,  p∈InputSet[P,Qi].(b)
If the public portq1 of the subcapsule Q1 is connected to the public port q2 of the subcapsule Q2, a new name z is generated dynamically to rename the ports q1 and q2. So,
(19)z∈InputSet[P,Q1],z∈InputSet[P,Q2].In the example shown in Figure1, according to Definition 2, the π-calculus definition of TopSystem structure diagram is the parallel composition of the definition of the subcapsules: Source, Router, ConsumerTarget, and ExporterTarget.  Considering the input sets used by TopSystem to reference its subcapsules, we have that the port setPort of ConsumerTarget is renamed to parent port setCT, the port setPort of ExporterTarget is renamed to parent port setET, and the new name z is created to rename the q1 and r1. So, TopSystem structure diagram is defined as
(20)TopSystem_StructureDiagram=Source〈z〉∣Router〈z〉∣ConsumerTarget〈setCT〉∣ExporterTarget〈setET,out〉.In order to complete the capsule definition inπ-calculus, the next section presents how to obtain the state diagram definition.


## 3.4. State Diagram Mapping

A capsule can specify or not an associated state diagram. If it is not specified, theπ-calculus definition of the capsule state diagram is the stop process. Otherwise, if the capsule has a state diagram, it is composed by states and transitions between them. The first transition to be activated is the initial transition, which is connected to the initial state.  As explained in Section 2.1, the initial transition does not have a trigger, it runs automatically when the state diagram initializes, but it can execute an action. So, the π-calculus definition of the state diagram is the sequence composition between the definition of initial transition action and the definition of the initial state, as explained in Definition 3.Definition 3 (State diagram definition).
Given a capsuleP. If P does not have a state diagram, the π-calculus definition of the state diagram is the stop process:
(21)P_StateDiagram=0.
Otherwise, if P has a state diagram, assuming that InitialTransition is the initial transition and S1 is the initial state, the π-calculus definition of the state diagram is given by
(22)P_StateDiagram=P_InitialTransition_Action·P_S1〈InputSet[P,InitialPoint,S1]〉.
where InputSet[P,InitialPoint,S1] is the input message set used by the initial transition definition to reference the definition of the state S1. It is defined in the transition action mapping.The definition of the initial transition action is explained in the transition action mapping, and the definition of the initial state is explained in the state mapping. Note that the initial transition trigger is not mentioned in Definition3, because the initial transition does not have a trigger, it runs automatically when the state diagram initializes. The definitions of the other states reachable from the initial state, which are included in the capsule state diagram, are considered in the definition of the initial state.In the example presented in Figure2, the ExporterTarget state diagram is defined, using Definition 3 as
(23)ExporterTarget_StateDiagram=ExporterTarget_Initial_Action·ExporterTarget_S1·〈InputSet[ExporterTarget,InitialPoint,S1]〉.According to Definition3, the state diagram definition references the initial state definition, which depends on the other states and transitions in the state diagram. So, the next section details the state and transition mapping.


## 3.5. State Mapping

The name of a UML-RT state in theπ-calculus definition is specified as the concatenation of the UML-RT capsule name and the UML-RT state name to guarantee unique definitions in π-calculus. An entry action is executed whenever the state is entered; regardless of which incoming transition is taken. Besides, a state has multiple outgoing transitions which can be taken. So, the π-calculus definition of the UML-RT state, as explained in Definition 4, is the sequence composition between its entry action definition and the choice composition of each transition definition.Definition 4 (Simple state definition).
Given a simple stateS in the state diagram of a capsule P, and given InputSet[P,S]. Assuming that the state S has an entry action and a set T of outgoing transitions, the π-calculus definition of the state S is given by
(24)P_S(InputSet[P,S])=P_S_EntryAction·∑i∈T(P_S_OutgoingTransitioni),
where InputSet[P,S] is the input message set of  the S definition. It is defined in the transition action mapping.For instance, in Figure2, the S1 definition can be written using Definition 4 as
(25)ExporterTarget_S1(InputSet[ExporterTarget,S1])=ExporterTarget_S1_EntryAction·P_S1_configPort.The UML-RT choice point is a special case of UML-RT state, where there is no entry and exit action, and the transition does not have a trigger, because it is enabled according to the condition specified in the choice point. So, Definition4 can be used to provide the π-calculus definition of a choice point too.According to Definition4, the entry action definition is a part of the state definition. The exit action definition is used only in the transition definition. The entry (or exit) action may not exist in a UML-RT state, so its reference is omitted from the state (or transition) definition. Whether the state performs an entry or exit actions, they include message sending actions in UML-RT, then the π-calculus definition of the entry and exit actions are the sequence composition of the message sending actions. The definition of a state action is provided in Definition 5 and may represent the definition of an entry action or an exit action.Definition 5 (State action definition).
Given a stateS in the state diagram of a capsule P, the state action can be an entry action and an exit action.
If the state action is not defined forS, the π-calculus reference to the state action definition is omitted from the parent definition.
Otherwise, if the state action is specified as a setN of message sending actions “pi sendei(m⃗i)”, the π-calculus definition of the state action is given by
(26)P_S_StateAction=∏i∈N(p̅i〈m⃗i〉).After presenting the state mapping, the next section explains the transition mapping.


## 3.6. Transition Mapping

In a UML-RT model, the transition has an associated trigger and may execute an action after being activated. Considering the state with its outgoing transitions, it is important to mention that the state exit action is taken whenever the control leaves the state from whatever outgoing transition; so the state exit action has to be computed after the transition trigger and before the transition action. Then, the outgoing transition definition in theπ-calculus, as detailed in Definition 6, is a sequence composition of the transition trigger definition, the state exit action, the transition action definition, and the target state definition.Definition 6 (Outgoing transition definition).
Given the simple statesS1 and S2 in the state diagram of a capsule P. Given an outgoing transition from S1 to S2, the π-calculus definition of the transition is
(27)P_S1_OutgoingTransition=P_S1_OutgoingTransition_Trigger·P_S1_ExitAction·P_S1_OutgoingTransition_Action·P_S2〈InputSet[P,S1,S2]〉,
where InputSet[P,S1,S2] is the input message set used by the state S1 to reference the definition of the state S2. It is defined in the transition action mapping.For instance, the transitionreceiveMsg can be defined, using Definition 6, as
(28)ExporterTarget_S4_receiveMsg=ExporterTarget_S4_receiveMsg_Trigger·ExporterTarget_S4_ExitAction·ExporterTarget_S4_receiveMsg_Action·ExporterTarget_S5〈InputSet[ExporterTarget,S4,S5]〉.A special case of a UML-RT transition is when the transition is a transition chain that transposes the boundaries of composite states. As it is explained in Section2.1, this transition is partitioned into different segments by the junction pointers, and only the originating segment has a trigger defined, while all segments can execute actions. In this case, we have to compute in the right order the following aspects: the trigger of the first segment, the actions of all segments, the entry or the exit action of all the transposed parent states, as detailed in Definition 7.Definition 7 (Definition of the outgoing transition chain).
Given an outgoing transition chain from a stateS1 to a state S2, where S1 and S2 belong to the state diagram of a capsule P. Assuming that the outgoing transition chain transposes the boundary of a set N of the parent states CS1’s of S1, and later transposes the boundary of a set M of the parent states CS2’s of S2, where N or M can be empty sets, the transition chain is composed by N+M+1 segments. In this case, the π-calculus definition of the outgoing transition chain is given by
(29)P_S1_OutgoingTransitionChain=P_S1_Segment1_Trigger·P_S1_ExitAction·P_S1_Segment1_Action·(P_S1_OutgoingTransitionChain_Up·P_S1_OutgoingTransitionChain_Down)·P_S2〈InputSet[P,S,S2]〉,
where
(30)P_S1_OutgoingTransitionChain_Up=∏i∈N(P_CS1i_ExitAction·P_S1_Segmenti+1_Action)P_S1_OutgoingTransitionChain_Down=∏j∈M(P_CS2j_EntryAction·P_S1_Segmentj+1+N_Action).TheExporterTarget state diagram, illustrated in Figures 2 and 3, has the transition chain initiating with the segment consumeMsg. This transition chain originates at the state S5 and transposes the boundary of the composite state S2 until reaching the state S3. According to Definition 7, the transition chain consumeMsg is defined as
(31)ExportedTarget_S5_consumeMsg=ExportedTarget_S5_consumeMsg_Trigger·ExportedTarget_S5_ExitAction·ExportedTarget_S5_consumeMsg_Action·ExportedTarget_S2_ExitAction·ExportedTarget_S5_msgConsumed_Action·ExportedTarget_S3〈InputSet[ExporterTarget,S5,S3]〉.As commented in Section3.1, the transition trigger is a message receipt statement and the transition action can be a message sending statement or a name reconfiguration statement. The transition trigger definition is provided in Definition 8, while the transition action definition is explained in Definition 9.Definition 8 (Transition trigger definition).
Given a transition from stateS1 to stateS2 in the state diagram of a capsule P.
If there is no trigger specified to the transition, theπ-calculus reference to the transition trigger definition is omitted from the parent definition.
Otherwise, assuming that the transition can be triggered by a setN of message receipt statements as “pireceiveei(m⃗i)”, the π-calculus definition of the transition trigger is given by
(32)P_S1_Transition_Trigger=∑i∈N(pi(m⃗i)).
A special case occurs when ei is a timeout signal. In this case, the trigger is represented by the unobservable action τ. So,  pi(m⃗i)=τ.Analyzing Definition8, the transition trigger definition considers all the messages that the capsule can receive in the current transition. However, it cannot be defined, for example, in an outgoing transition of a choice point and in the first segment of a transition chain.In Definition9, the transition action considers all the message sending and the reconfiguration statements. In case of a reconfiguration statement, it is important that the old name is the one used by the next state, while the new name is used to reference the next state definition. The input message set of the capsule definition is maintained in the other input sets to keep the consistence of the π-calculus definitions. Note that Definition 9 holds to the actions of all segments in a transition chain.Definition 9 (Transition action definition).
Given a transition from stateS1 to state S2 in the state diagram of a capsule P.
If there is no action associated to the transition, theπ-calculus reference to the transition action definition is omitted from the parent definition.
Otherwise, assuming that the transition action is composed of a setN of message sending statements as “pisendei(m⃗i)” and also by a set M of name reconfiguration statements as “yj=xj”, the π-calculus definition of the transition action is given by
(33)P_S1_Transition_Trigger=∏i∈N(p̅i〈m⃗i〉),InputSet[P,S1,S2]=⋃j∈Mxj∪InputSet[P],InputSet[P,S2]=⋃j∈Myj∪InputSet[P],
where InputSet[P] is the input message set of the P capsule definition, already defined in Definition 1.For instance, the transitionreceiveMsg of the ExporterTarget state diagram, illustrated in Figure 3, has a trigger which can be defined using Definition 8 as follows:
(34)ExporterTarget_S4_receiveMsg_Trigger=t(d1,d2).It is an example of receiving two messages in a single synchronization, which shows the importance of using polyadicπ-calculus in the mapping.As an example to apply Definition9, consider the transition segment exportMsg. So,
(35)ExporterTarget_S5_exportMsg_Action()=export¯〈d1〉.The next section presents three examples that illustrate how the mapping rules can be applied to obtain theπ-calculus definitions from a UML-RT model, and how to manipulate the generated π-calculus definitions in order to verify some system requirements.


## 4. Examples of the Mapping

In this section, we develop three examples. The first one is theTopSystem, shown in  Figure 1 and used in the previous sections to introduce the UML-RT and to exemplify the mapping rules application. The objective is to provide the entire UML-RT model of the TopSystem and to explain step by step how to obtain the π-calculus definition of its Source capsule. The example includes mobility and deals with some UML-RT concepts which were not previously addressed in our previous work, such as the entry and the exit actions, the composite states, and the transition chains.The second example is a Heating System for Air Conditioning, which is an adaptation of [10], and the objective is to use the π-calculus definitions to verify if the UML-RT model correctly implements the system requirements. This example does not include mobility concept; however it is interesting to understand the possible manipulations using π-calculus reactions in order to verify the system behavior.Finally, the third example is the Handover protocol, an example of mobile processes presented by Milner in [24]. It includes the communication of more than one message at a time, so it is suitable case for the polyadic π-calculus.


### 4.1. Router Example

In this section, we explain how to obtain theπ-calculus definition of the entire capsule TopSystem, illustrated in Figure 1, using the mapping rules provided in Section 3. The capsule TopSystem comprises the following capsules: source (instance of the capsule Source), router (instance of the capsule Router), target1 (instance of the capsule ConsumerTarget), and target2 (instance of the capsule ExporterTarget). We provide the state diagram of the capsules TopSystem,Source, Router, and ConsumerTarget, respectively, in Figures 5, 6, 7, and 8.Figure 5
The state diagram of the capsuleTopSystem.Figure 6
The state diagram of the capsuleSource.Figure 7
The state diagram of the capsuleRouter.Figure 8
The state diagram of the capsuleConsumerTarget.The entry and exit actions of the states in the capsule TopSystem and its subcapsules are detailed in Table2. It is important to note that these actions are not considered as a sending message statement or a name reconfiguration statement, because they just set up an internal timeout, so the π-calculus definition of each action is the stop process.Table 2
Entry and exit actions of the states in the capsuleTopSystem and its subcapsules.
CapsuleStateEntry actionExit actionTopSystemS1——SourceS1timer·informIn(RTTimespec(10,0));—S2——S3timer·informIn(RTTimespec(1,0));—RouterS1——S2timer·informIn(RTTimespec(4,0));—S3timer·informIn(RTTimespec(1,0));—ConsumerTargetS1——S2——S3timer·informIn(RTTimespec(2,0));—ExporterTargetS1——S2——S3timer·informIn(RTTimespec(1,0));—S4——S5——The specification of the transitions inside the state diagrams of the capsuleTopSystem and its subcapsules is provided in Table 3. Table 4 presented the pseudocode that represents the transition trigger and the transition action; the pseudocode helps to understand the application of the mapping rules to obtain the π-calculus definitions.Table 3
UML-RT transitions’ specification for the capsuleTopSystem and its subcapsules.
CapsuleTransitionUML-RT triggerUML-RT actionTopSystemInitial—setCT·portName(x)·send();setET·portName(y) ·send();SourceInitial——timeoutPort:timer—Signal:timeoutsendPortX—q·portName(x)·send();sendPortY—q·portName(y)·send();timeout2——RouterInitial——receivePortPort:ra = *rtdata;Signal:portNamealert·registerSPP(a);sendMsgPort:timerm·msg1 = b1;m·msg2 = b2;Signal:timeoutalert·msg(m)·send();waitPortPort:timer—Signal:timeoutConsumerTargetInitial——configPortPort:setPortaux  = *rtdata;Signal:portNames·registerSAP(aux);consumeMsgPort:sm = *rtdata;c1 = m·msg1;Signal:msgc2 = m·msg2;waitMsgPort:timer—Signal:timeoutExporterConsumerInitial——configPortPort:setPortaux = *rtdata;Signal:portNamet·registerSAP(aux);Initial1——Initial2——receiveMsgPort:tm = *rtdata;d1 = m·msg1;Signal:msgd2 = m·msg2;consumeMsg——exportMsg—export·msg(d1) ·send();msgConsumed——msgExported——waitMsgPort:timer—Signal:timeoutTable 4
Pseudocode of the transitions in the capsuleTopSystem and its subcapsules.
CapsuleTransitionTrigger pseudocodeAction pseudocodeTopSystemInitial—setCT send portName(x)setET send portName (y)SourceInitial——timeouttimer receive timeout( )—sendPortX—q send portName(x)sendPortY—q send portName(y)timeout2——RouterInitial——receivePortr receive portName(a)alert =asendMsgtimer receive timeout( )alert send msg(b1,b2)waitPorttimer receive timeout( )—ConsumerTargetInitial——configPortsetPort receive  portName (aux)s = auxconsumeMsgs receive msg(c1,c2)—waitMsgtimer receive timeout( )—ExporterConsumerInitial——configPortsetPort receive portName(aux)t = auxInitial1——Initial2——receiveMsgt receive msg(d1,d2)—consumeMsg——exportMsg—export send msg(d1)msgConsumed——msgExported——waitMsgtimer receive timeout( )—The structure diagrams of theTopSystem subcapsules are not provided because the majority of ports are public, so they can be seen in TopSystem structure diagram (shown in Figure 1). The only exception is the protected port timer presented in all TopSystem subcapsules. The port timer implements the protocol Timing (a built-in protocol of the RoseRT tool) and receives the timeout signal.In order to show how to apply the mapping rules to obtain theπ-calculus definition of a UML-RT capsule, we detail the mapping of the capsule Source.Using Definition1, the π-calculus definition of the capsule Source is the parallel composition of its state diagram definition and its structure diagram definition:
(36)Source(InputSet[Source])=new(RestrictedSet[Source])(Source_StructureDiagram∣Source_StateDiagram),
where
(37)InputSet[Source]={q},RestrictedSet[Source]={}-{q}={}.
So, we have
(38)Source(q)=(Source_StructureDiagram∣Source_StateDiagram).According to Definition2, the structure diagram of the capsule Source is the parallel composition of its subcapsules. As the capsule Source does not have subcapsules, the π-calculus definition of its structure diagram is the stop process:
(39)Source_StructureDiagram=0.Theπ-calculus definition of the Source state diagram, according to Definition 3, can be written as
(40)Source_StateDiagram=Source_Initial_Action·Source_S1〈InputSet[Source,InitialPoint,S1]〉.As theInitial transition does not have an action, using the Definition 9 it is omitted from the Source definition and we have
(41)InputSet[Source,InitialPoint,S1]={q},(42)InputSet[Source,S1]={q},(43)Source_StateDiagram=Source_S1〈q〉.Using the Definition4 and (42), the π-calculus definition of state S1, in the capsule Source, can be written as the sequence composition of its entry action and its unique outgoing transition
(44)Source_S1(q)=Source_S1_EntryAction·Source_S1_timeout.As theS1 entry action is not specified, according to Definition 5 it is omitted from the parent definition, so
(45)Source_S1(q)=Source_S1_timeout.Theπ-calculus definition of the transition timeout is made based on Definition 6. So, from (45), we have
(46)Source_S1(q)=Source_S1_timeout_trigger·Source_S1_ExitAction·P_S1_timeout_Action·Source_S2〈InputSet[Source,S1,S2]〉.The trigger of the transitiontimeoutis the unobservable action τ, based on Definition 8, because the trigger in UML-RT is specified by the receiving of a timeout signal as stated in Table 4. The S1 exit action is not specified, so according to Definition 5 it is omitted from the parent definition. There is no action in transition timeout, so its definition is omitted from the parent definition and InputSet[Source,S1,S2]=InputSet[Source,S2]={q}. From (46), the S1 definition in the π-calculus can be written as
(47)Source_S1(q)=τ·Source_S2〈q〉.TheS1 definition references the state S2. So, it is necessary to specify the π-calculus definition of state S2. So,byusing Definition 4, we have
(48)Source_S2(q)=Source_S2_EntryAction·(Source_S2_sendPortX+Source_S2_sendPortY).Using Definitions5 and 6, from (48), we have
(49)Source_S2(q)=((Source_S2_sendPortX_trigger·Source_S2_ExitAction·P_S2_sendPortX_Action·Source_S3〈InputSet[Source,S2,S3]〉)+(Source_S2_sendPortY_trigger·Source_S2_ExitAction·P_S2_sendPortY_Action·Source_S3〈InputSet[Source,S2,S3]〉)).Using Definitions5, 8, and 9, from (49) the π-calculus definition of S2 is written as
(50)Source_S2(q)=(q̅〈x〉·Source_S3〈q〉)+(q̅〈y〉·Source_S3〈q〉).However, theS2 definition references the state S3. So, it is also necessary to specify the π-calculus definition of the state S3. So, by using Definition 4, we have
(51)Source_S3(q)=Source_S3_EntryAction·Source_S3_timeout2.
Using Definitions 5 and 6, from (51), we have
(52)Source_S3(q)=Source_S3_timeout2_trigger·Source_S3_ExitAction·P_S3_timeout2_Action·Source_S1〈InputSet[Source,S3,S1]〉.Finally, using Definitions5, 8, and 9, from (51) the π-calculus definition of S3 is written as
(53)Source_S3(q)=τ·Source_S1〈q〉.From (47), (50), and (53), the π-calculus definition of the state S1 is
(54)Source_S1(q)=τ·((q̅〈x〉·τ·Source_S1〈q〉)+(q̅〈y〉·τ·Source_S1〈q〉)).Finally, using (38), (39), (43), and (54), the π-calculus definition of the capsule Source is given by
(55)Source(q)=Source_S1〈q〉Source_S1(q)=τ·((q̅〈x〉·τ·Source_S1〈q〉)+(q̅〈y〉·τ·Source_S1〈q〉)).Using the mapping rules and the specifications of transitions in Table4, it is possible to define the π-calculus definition of the other capsules that compose the TopSystem example, as written in
(56)Router(r)=Router_S1〈r〉Router_S1(r)=r(a)·Router_S2〈a,r〉Router_S2(alert,r)=τ·alert¯〈b1,b2〉·τ·Router_S1〈r〉(57)ConsumerTarget(setPort)=setPort(aux)·ConsumerTarget_S2〈aux,setPort〉ConsumerTarget_S2(s,setPort)=s(c1,c2)·τ·ConsumerTarget_S2〈s,setPort〉(58)ExporterTarget(setPort,export)=setPort(aux)·ExporterTarget_S4〈aux,setPort,export〉ExporterTarget_S4(t,setPort,export)=t(d1,d2)·(τ·ExporterTarget_S4〈t,setPort,export〉+(export¯〈d1〉·τ·ExporterTarget_S4〈t,setPort,export〉))(59)TopSystem(out)=newz,setCT,setET·(Source〈z〉∣Router〈z〉∣ConsumerTarget〈setCT〉·∣ExporterTarget〈setET,out〉∣setCT¯〈x〉·setET¯〈y〉).Through the definition of a capsule it is possible to capture the behavior of this capsule, for example, the capsuleSource in (55) executes an unobservable action (i.e., a timeout), sends the message x or y along the port q, and returns to a state (in this case S1), where it is possible to repeat the same behavior. Due to the connection between the subcapsules Source and Router in the capsule TopSystem, the parent capsule references its subcapsule Source renaming the port q to z, and references its subcapsule Router renaming the port r to z. Therefore, the message x or y sent by the subcapsule Source is received by the subcapsule Router, and it is stored in the name a, according to (56). The definition of Router_S1 references the definition of Router_S2 renaming alert with a, so the subcapsule Router is now able to send the messages b1 and b2 through the port alert, which can be x or y.The capsuleTopSystem in (59) sends x to its subcapsule ConsumerTarget and sends y to its subcapsule ExporterTarget. According to (57), the subcapsule ConsumerTarget configures its port s with x to be able to receive the message from the capsule Router. Similarly, according to (58), the subcapsule ExporterTarget configures its port t with y to be able to receive the message from the capsule Router. After receiving the message from the Router, the control of the subcapsule ExporterTarget can return to ExporterTarget_S4, or it can send the received message through its port export and later the control returns to ExporterTarget_S4. Note that the port export is in fact renamed to out, which is a public interface of the capsule TopSystem, according to (59).In the example, theπ-calculus definitions corresponding to the UML-RT model were specified. Using the generated π-calculus definitions, it is possible to analyze the interactions between the system components, therefore some undesirable system behavior can be uncovered during the modeling phase.


### 4.2. Heating System

In this section, we use an example of a system, which was adapted from the example described in [10] and is called Heating System for Air Conditioning. In this example, the system requirements are provided as well as the UML-RT model that implements the requirements. Furthermore, the π-calculus definitions for the system are generated following the mapping rules. Some scenarios are proposed according to the system requirements. Later, we compose the π-calculus definitions of the system and the scenarios in order to verify if the model meets the requirements. The handlings are made manually.The heating system consists of the standard heating subsystem and the additional heating subsystem that is used to shorten the time needed to increase the temperature in the car. The specification of the heating system is provided through the requirements R1 to R7. In the requirements’ descriptions we anticipate the UML-RT states of the state diagrams of this section. They are named between parentheses. The requirements are as follows.R1
The heating system has two levels: level1 (Level1 state) and level2 (Level2 state). In level1 only the standard heating system is active, while in level2 the additional heating system is also active.R2
An incoming init event changes the heating system’s status from shutdown (Shutdown state) to level1 and from start (Start state) to level2.R3
The heating system automatically changes its status from level2 to level1 after 10 minutes.R4
The heating system automatically changes its status from start to shutdown after 10 minutes.R5
Exceptions regarding invalid voltage or ignition key in status “cold” immediately cause deactivation of the heating system for 10 seconds.R6
As soon as there is no more exception, the heating system continues operating on the selected level.R7
The heating system’ status changes to shutdown if the ignition key stays in status “cold” for 5 minutes, or if the key is removed.The heating system model (Figure9) was constructed using the RoseRT tool. It is a capsule called HeatingSystem composed of three subcapsules: low (instance of the capsule LowExceptions in Figure 10), high (instance of the capsule HighExceptions in Figure 11), and controller (instance of the capsule HeatingController in Figure 12). The interface of the HeatingSystem is the ports to receive the ignition status (KL15off, KL15radio, and KL15cold), the voltage invalid status (iVolt), the signal to start and shutdown the controller operation (startController and shutdownController, resp.). The specification of the transitions inside each capsule state diagram is in Table 5; whereas the entry and exit actions of the states are detailed in Table 6.Table 5
Transitions in theHeatingSystem subcapsules.
CapsuleTransitionUML-RT triggerUML-RT actionLowExceptionsInitial——receiveExceptionPort:ignitionColdoff·sig()·send();Signal:sigPort:invalidVoltageSignal:sigexpireExceptionPort:timeron·sig()·send();Signal:timeoutHighExceptionsInitial——receiveIgnitionKeyRadioPort:ignitionRadioon·sig()·send();Signal:sigreceiveIgnitionKeyColdPort:ignitionCold—Signal:sigreceiveIgnitionKeyRadio2Port:ignitionRadio—Signal:sigreceiveIgnitionKeyOffPort:ignitionOffoff·sig()·send();Signal:sigafter5minutesPort:timeroff·sig()·send();Signal:timeoutHeatingControllerInitial——InitiatePort:on—Signal:sigPort:initSignal:sigTerminatePort:off—Signal:sigPort:endSignal:sigAfter10minutesPort:timer—Signal:timeoutTable 6
Entry and exit actions of the states in theHeatingSystem subcapsules.
CapsuleStateEntry actionExit actionLowExceptionsOkayLPrio——OffLPriotimer·informIn(RTTimespec(10,0));—HighExceptionsOffHPrio——OkayHPrio——WaitHPriotimer·informIn(RTTimespec(300,0));—HeatingControllerStarttimer·informIn(RTTimespec(600,0));—Level2out·msg(L2)·send();—timer·informIn(RTTimespec(600,0));Level1out·msg(L1) ·send();—Shutdownout·msg(BAD) ·send();—Figure 9
The structure diagram of the capsuleHeatingSystem.Figure 10
The state diagram of the capsuleLowExceptions.Figure 11
The state diagram of the capsuleHighExceptions.Figure 12
The state diagram of the capsuleHeatingController.The capsuleLowExceptions starts at the state OkayLPrio and changes to OffLPrio, if it receives a signal through the port ignitionCold or invalidVoltage. During this transition, the capsule sends a signal through the port off in order to shutdown the heating controller temporarily. After 10 seconds, the capsule LowExceptions is ready to receive more exception information, when it returns to the state OkayLPrio.The capsuleHighExceptions starts at the state OffHPrio and changes to OkayHPrio, if it receives a signal through the port ignitionRadio. This transition executes an action of sending a signal along the port on in order to start the heating controller, because there is no more high exception to be handled. After receiving a signal through the port ignitionCold at the state OkayHPrio, the capsule HighExceptions changes to the state WaitHPrio. At the state WaitHPrio, the capsule can change to the state OkayHPrio if the ignition returns to the status radio; or it can detect a high exception if the ignition exceeds 5 minutes in the status cold, or if the ignition changes to the status off. In case of detecting a high exception, the capsule sends a signal along the port off aiming to shutdown the heating controller.The capsuleHeatingController begins at the state Start and changes to Level2 if it receives a signal through the ports on or init. At the state Level2, the capsule can changes to the state Level1 after 10 minutes, or it can shutdown after receiving a signal along the ports off or end. At the state Level1, the capsule can shutdown too. The capsule is able to notify its status in each state sending a message through the port out.Some system requirements can be verified by a visual inspection in the model, for example, the requirements R1 to R4 are addressed by the transitions specified in the state diagram of the capsuleHeatingController. Other requirements are modeled, for example, R5 to R7, however we do not know if the behavior of the system interacting components complies with the requirements. In order to verify some properties originated immediately from the requirements, we can use the system formal specification in the π-calculus.Theπ-calculus definitions of the heating system are provided below; however we omit the capsule name in each state name due to space limitation
(60)HeatingSystem(KL15radio,KL15cold,KL15off,iVolt,startController,shutdownController,heatingStatus)=newon,off(HeatingController〈Set1Ref〉∣LowExceptions〈Set2Ref〉∣HighExceptions〈Set3Ref〉),
where
(61)Set1Ref={startController,shutdownController,on,off,heatingStatus},Set2Ref={KL15cold,iVolt,on,off},Set3Ref={KL15radio,KL15cold,KL15off,on,off}.DeclaringSet1={init,end,on,off,out} as the input set of HeatingController definition, we have
(62)HeatingController(List1)=Start〈Set1〉Start(Set1)=(on+init)·Level2〈Set1〉+τ·Shutdown〈Set1〉Level2(Set1)=out¯〈L2〉·((off+end)·Shutdown〈Set1〉+τ·Level1〈Set1〉)Level1(Set1)=out¯〈L1〉·((off+end)·Shutdown〈Set1〉)Shutdown(Set1)=out¯〈BAD〉·((on+init)·Level1〈Set1〉).Declaringet2={ignitionCold,invalidVoltage, on,  off} as the input set of LowExceptions definition, we have
(63)LowExceptions(Set2)=OkayLPrio〈Set2〉OkayLPrio(Set2)=(ignitionCold+invalidVoltage)·off¯·OffLPrio〈Set2〉OffLPrio(Set2)=τ·on¯·OkayLPrio〈Set2〉.DeclaringSet3 = {ignitionRadio, ignitionCold, ignitionOff, on, off} as the input set of HighExceptions definition, we have
(64)HighExceptions(Set3)=OffHPrio〈Set3〉OffHPrio(Set3)=ignitionRadio·on¯·OkayHPrio〈Set3〉OkayHPrio(Set3)=ignitionCold·WaitHPrio〈Set3〉WaitHPrio(Set3)=ignitionRadio·OkayHPrio〈Set3〉+ignitionOff·off¯·OffHPrio〈Set3〉+τ·off¯·OffHPrio〈Set3〉.After obtaining the definitions of the components in the model, it is desirable to verify its properties. In order to verify the requirements R5 and R6, we assume the scenario where an external actor sends astartController¯ event and, later, it sends an iVolt¯ event. The scenario can be specified as
(65)Scenario1=startController¯·heatingStatus(s1)·iVolt¯·heatingStatus(s2)·heatingStatus(s3).
After the startController¯ event, the information that the system is at the level2 is expected, so s1 will receive “L2”. After the iVolt¯ event, the information that the system is shutdown is due, so s2 will receive “BAD”. After the timeout of the low exception (in this case, the invalid voltage), the information that the system is at the level2 is waited, so s3 will be “L2”, because the requirement R6 specifies that the system has to return to the selected level after the exceptions.Composing the heating system and the scenario, we obtain(66)HeatingSystem(KL15radio,KL15cold,KL15off,iVolt,startController,shutdowController,heatingStatus)∣Scenario1.Using (60) and (65), we have
(67)newon,off(HeatingController〈Set1Ref〉∣LowExceptions〈Set2Ref〉∣HighExceptions〈Set3Ref〉)∣(startController¯·heatingStatus(s1)·iVolt¯·heatingStatus(s2)·heatingStatus(s3)).Replacing the definitions of theHeatingSystem subcapsules, we obtain
(68)newon,off(((on+startController)·Level2〈Set1Ref〉+τ·Shutdown〈Set1Ref〉)∣((KL15cold+iVolt)·off¯·OffLPrio〈Set2Ref〉)∣(KL15radio·on¯·OkayHPrio〈Set3Ref〉)∣(startController¯·heatingStatus(s1)·iVolt¯·heatingStatus(s2)·heatingStatus(s3))).After the reaction betweenstartController¯ and startController, we have
(69)newon,off(Level2〈Set1Ref〉∣((KL15cold+iVolt)·off¯·OffLPrio〈Set2Ref〉)∣(KL15radio·on¯·OkayHPrio〈Set3Ref〉)∣(heatingStatus(s1)·iVolt¯·heatingStatus(s2)·heatingStatus(s3))).Replacing the definition ofLevel2〈Set1Ref〉, we obtain
(70)newon,off((heatingStatus¯〈L2〉·((off+shutdownController)·Shutdown〈Set1Ref〉+τ·Level1〈Set1Ref〉))∣((KL15cold+iVolt)·off¯·OffLPrio〈Set2Ref〉)∣(KL15radio·on¯·OkayHPrio〈Set3Ref〉)∣(heatingStatus(s1)·iVolt¯·heatingStatus(s2)·heatingStatus(s3))).After the reaction betweenheatingStatus¯〈L2〉 and heatingStatus(s1), the name s1 receives the message “L2” as required in the scenario specification. So,
(71)newon,off(((off+shutdownController)·Shutdown〈Set1Ref〉+τ·Level1〈Set1Ref〉)∣((KL15cold+iVolt)·off¯·OffLPrio〈Set2Ref〉)∣(KL15radio·on¯·OkayHPrio〈Set3Ref〉)∣(iVolt¯·heatingStatus(s2)·heatingStatus(s3))).After the reaction betweeniVolt¯ and iVolt, we have
(72)newon,off(((off+shutdownController)·Shutdown〈Set1Ref〉+τ·Level1〈Set1Ref〉)∣(off¯·OffLPrio〈Set2Ref〉)∣(KL15radio·on¯·OkayHPrio〈Set3Ref〉)∣(heatingStatus(s2)·heatingStatus(s3))).After the reaction betweenoff¯ and off, we obtain
(73)newon,off(Shutdown〈Set1Ref〉∣OffLPrio〈Set2Ref〉∣(KL15radio·on¯·OkayHPrio〈Set3Ref〉)∣(heatingStatus(s2)·heatingStatus(s3))).Replacing the definition ofShutdown and OffLPrio, we have
(74)newon,off((heatingStatus¯〈BAD〉·((on+startController)·Level1〈Set1Ref〉))∣(τ·on¯·OkayLPrio〈Set2Ref〉)∣(KL15radio·on¯·OkayHPrio〈Set3Ref〉)∣(heatingStatus(s2)·heatingStatus(s3))).After the reaction betweenheatingStatus¯〈BAD〉 and heatingStatus(s2), the name s2 receives the message “BAD” as required in the scenario specification. So,
(75)newon,off(((on+startController)·Level1〈Set1Ref〉)∣(τ·on¯·OkayLPrio〈Set2Ref〉)∣(KL15radio·on¯·OkayHPrio〈Set3Ref〉)∣heatingStatus(s3)).After theτ  reaction that represents the 10 seconds after the low exception, we obtain
(76)newon,off(((on+startController)·Level1〈Set1Ref〉)∣(on¯·OkayLPrio〈Set2Ref〉)∣(KL15radio·on¯·OkayHPrio〈Set3Ref〉)∣heatingStatus(s3)).After the reaction betweenon¯ and  on, we have
(77)newon,off(Level1〈Set1Ref〉∣OkayLPrio〈Set2Ref〉∣(KL15radio·on¯·OkayHPrio〈Set3Ref〉)∣heatingStatus(s3)).Replacing the definition ofOkayLPrio, we obtain
(78)newon,off((heatingStatus¯〈L1〉·(off+shutdownController)·shutdown〈Set1Ref〉))∣OkayLPrio〈Set2Ref〉∣(KL15radio·on¯·OkayHPrio〈Set3Ref〉)∣heatingStatus(s3)).Now there is the possibility of the reaction betweenheatingStatus¯〈L1〉 and heatingStatus(s3), then the name s3 receives the message “L1”. Note that the heating system is in level1, which is an active status, so the requirement R5 is satisfied. Otherwise, the requirement R6 is not met, because the heating system was at level2 before the low exception and now it is at level1, when it should continue in level2. In this example, the designer can uncover the error in the model analyzing the state diagrams; however in a more complex system, the visual analysis is very difficult, so the formal analysis is necessary.Aiming to verify the requirement R7, we propose a scenario composed by the following steps: the ignition key is in status radio, an external event initiates the controller and, later, the ignition key is in status off. The scenario is specified as(79)Scenario2=KL15radio¯·startController¯·heatingStatus(s1)·KL15off¯·heatingStatus(s2).After thestartController¯ event, it is expected to be informed that the system is at the level2, so s1 will receive “L2”. After the KL15off¯ event, it is expected to be informed that the system is shutdown, so s2 will receive “BAD”. Analyzing this scenario, we note that, after receiving the event startController¯, the HighExceptions capsule sends the event on¯ to initiate the heating controller. So, a component to manage exceptions can initiate the controller for the first time, before it has been initiated by the external event startController¯. In this case, we obtain an unexpected behavior according to the proposed scenario; however we are not sure if it is an error in the model or a missing requirement specification.Then, using the system specification in theπ-calculus and the scenarios or properties proposed according to the system requirements, it is possible to analyze the interaction between the system components and find out the undesirable behavior due to errors in  modeling or and a lack of specification.


### 4.3. Handover Protocol

In this section, we show the example of mobile processes called Handover Protocol presented by Milner in [24]. The Handover system (Figure 13) is composed by a control tower (Control capsule), two communicating towers (Trans capsules: trans1 and trans2), and a car (capsule Car). For a better visualization of Figure 13, the protocol type of each port is omitted. The control tower has fixed connections with the communicating towers; it is expressed through the wired ports between the capsule Control and the two capsules Trans. The car communicates with a Trans tower, but an event can make it communicates with the other Trans.Figure 13
The structure diagram of the capsuleHandover.The state diagrams of the capsulesCar, Trans, and Control are presented in  Figure 14. The state diagram of the top level capsule Handover is not shown; however it is composed only by the initial transition and an initial state called S1. The UML-RT specifications for the transitions of all capsules are available in Table 7.Table 7
Transitions in the capsuleHandoverand its subcapsules.
CapsuleTransitionUML-RT triggerUML-RT actionHandoverInitial—m·talk = talk1;m·change = change1;setCar·signal(m)·send();CarInitial——startPort:setCarm = *rtdata;t = m·talk;Signal:signalc = m·change;talk·registerSAP(t);change·registerSAP(c);updateConnectionPort:changem = *rtdata;t = m·talk;Signal:signalc = m·change;talk·registerSAP(t);change·registerSAP(c);communicatePort:timertalk·signal(info)·send();Signal:timeoutTransInitial——activatePort:gainm = *rtdata;t = m·talk;Signal:signalc = m·change;talk·registerSPP(t);change·registerSPP(c);deactivatePort:losem = *rtdata;t  = m·talk;c = m·changeSignal:signalm2·talk = t;m2·change = c;change·signal(m2)·send();communicatePort:talkmyinfo = *rtdata;Signal:signalControlInitial—m·talk = talk1;m·change = change1;gain1·signal(m)·send();startControl1Port:timerm·talk = talk1;m·change = change1;Signal:timeoutlose2·signal(m)·send();gain1·signal(m)·send();startControl2Port:timerm·talk = talk2;m·change = change2;Signal:timeoutlose1·signal(m)·send();gain2·signal(m)·send();The state diagrams of the capsules: (a)Car,  (b) Trans, and  (c) Control.
(a)(b)(c)The overall behavior is the following. the transitionInitial of the capsule Handover sends two messages talk1 and change1 along the protected setCar. The messages are received by the car in order to make the initial configuration of its unwired ports talk and change. On the other hand, when control initializes, it sends to trans1 the messages talk1 and change1 that are used by trans1 to configure the unwired ports talk and change. At this moment, the car is able to communicate to trans1 by sending a message through the port talk.However,controlcan activate the trans2. In this case, the control sends the messages talk2 and change2 to trans1 (via the port lose1) and to trans2 (via the port gain2). The trans1 receives the messages talk2 and change2, and it sends to the car (via the port change). So, the car uses the messages to reconfigure its unwired ports talk and change. Besides, the trans2 receives the messages talk2 and change2 from the control to configure its unwired ports talk and change. At this moment, the car is able to communicate to trans2 by sending a message through the port talk.Thecontrol continues its processing either activating trans1 or activating trans2. It allows the car always to communicate to some tower, that is, trans1 or trans2.It is desirable to obtain theπ-calculus definition of the Handover system, so it is important to analyze each capsule based on Figure 14 and Table 7in order to apply the mapping rules proposed in Section 3.Analyzing the capsuleCar, in the transition start, it receives the messages t and c in order to make the initial configuration of its unwired ports. After the initial configuration, Car in the state Operating is ready to send the message info to a tower through the port talk. However, Car can also receive from trans1 two messages (t and c) simultaneously along the port change, indicating a new name for the port talk and a new name for the port change, respectively. This is the step that the car reconfigures its ports to start to operate with the other tower. Then, the π-calculus definition of the capsule Car is written as
(80)Car(setCar)=Car_Idle〈setCar〉Car_Idle(setCar)=setCar(t,c,setCar)·Car_Operating〈t,c,setCar〉Car_Operating(talk,change,setCar)=τ·talk¯〈info〉·Car_Operating(talk,change,setCar)+change(t,c)·Car_Operating(talk,change,setCar).The towerTrans begins in the state Idle, where it is possible to receive the configuration for its unwired ports talk and change via the transition activate. In the Active state, Trans can receive a message myinfo from Car using the transition communicate. However, Trans can also receive a message from Control with the new names t and c. These names are later sent to Car via the port change and indicate how its unwired ports must be reconfigured. Using the mapping rules, the capsule Trans is defined in the π-calculus as
(81)Trans(gain,lose)=Trans_Idle〈gain,lose〉Trans_Idle(gain,lose)=gain(t,c)·Trans_Active(t,c,gain,lose)Trans_Active(talk,change,gain,lose)=talk(myinfo)·Trans_Active(talk,change,gain,lose)+lose(t,c)·change¯〈t,c〉·Trans_Idle〈gain,lose〉.The state diagram ofControl initiates (transition Initial) sending the messages talk1 and change1 along the port gain1. In the Control1 state, after a timeout (transition startControl2), Control can send the messages talk2 and change2 through the port lose1, and later through the port gain2. In a similar way, in the Control2 state, after a timeout (transition startControl1), Control can send the messages talk1 and change1 through the port lose2, and later through the port gain1. In this way, the transition startControl2 indicates that trans2 is apt to talk with the car; while the transition startControl1 indicates that trans1 is now ready to talk with the car. Then, the π-calculus definition of the capsule Control is written as
(82)Control(gain1,lose1,gain2,lose2)=gain1¯〈talk1,change1〉·Control_Control1〈gain1,lose1,gain2,lose2〉Control_Control1(gain1,lose1,gain2,lose2)=τ·lose1¯〈talk2,change2〉·gain2¯〈talk2,change2〉·Control_Control2〈gain1,lose1,gain2,lose2〉Control_Control2(gain1,lose1,gain2,lose2)=τ·lose2¯〈talk1,change1〉·gain1¯〈talk1,change1〉·Control_Control2〈gain1,lose1,gain2,lose2〉.Finally, theHandover system is defined in the π-calculus as the parallel composition of the definition of its state diagram and its structure diagram definition.  The state diagram definition is the possibility to send the messages talk1 and change1 along the port setCar. The structure diagram definition includes a reference to each subcapsule definition. So, the Handoverdefinition is written as
(83)Handover()=new(setCar,zgain1,zlose1,zgain2,zlose2)(Car〈setCar〉∣Trans〈zgain1,zlose1〉∣Trans〈zgain2,zlose2〉∣Control〈zgain1,zlose1,zgain2,zlose2〉∣setCar¯〈talk1,change1〉).It is important to understand each term in the parallel composition shown in (83). The first term represents the subcapsule car (instance of Car). The second and the third terms represent the subcapsules trans1 and trans2 (instance of Trans), respectively. The fourth term indicates the subcapsule control (instance of Control). The last term is the definition of the Handover state diagram. Besides, the names setCar, zgain1, zlose1, zgain2, zlose2 are used to represent the wired connections between the subcapsules in the π-calculus definitions. For example, the name zgain1 allows the communication between the port gain1 of control and the port gain of trans1, because the subcapsule’s ports are renamed to the same name zgain1.The Handover system is an example of mobile processes, where the messages received by a process in a communication can be used to rename its ports and, consequently, to allow the reconfiguration of its connections with other processes. Besides, the present example includes the need of the communication of more than one message at a time between processes, which emphasizes the importance of the polyadicπ-calculus approach.


## 4.1. Router Example

In this section, we explain how to obtain theπ-calculus definition of the entire capsule TopSystem, illustrated in Figure 1, using the mapping rules provided in Section 3. The capsule TopSystem comprises the following capsules: source (instance of the capsule Source), router (instance of the capsule Router), target1 (instance of the capsule ConsumerTarget), and target2 (instance of the capsule ExporterTarget). We provide the state diagram of the capsules TopSystem,Source, Router, and ConsumerTarget, respectively, in Figures 5, 6, 7, and 8.Figure 5
The state diagram of the capsuleTopSystem.Figure 6
The state diagram of the capsuleSource.Figure 7
The state diagram of the capsuleRouter.Figure 8
The state diagram of the capsuleConsumerTarget.The entry and exit actions of the states in the capsule TopSystem and its subcapsules are detailed in Table2. It is important to note that these actions are not considered as a sending message statement or a name reconfiguration statement, because they just set up an internal timeout, so the π-calculus definition of each action is the stop process.Table 2
Entry and exit actions of the states in the capsuleTopSystem and its subcapsules.
CapsuleStateEntry actionExit actionTopSystemS1——SourceS1timer·informIn(RTTimespec(10,0));—S2——S3timer·informIn(RTTimespec(1,0));—RouterS1——S2timer·informIn(RTTimespec(4,0));—S3timer·informIn(RTTimespec(1,0));—ConsumerTargetS1——S2——S3timer·informIn(RTTimespec(2,0));—ExporterTargetS1——S2——S3timer·informIn(RTTimespec(1,0));—S4——S5——The specification of the transitions inside the state diagrams of the capsuleTopSystem and its subcapsules is provided in Table 3. Table 4 presented the pseudocode that represents the transition trigger and the transition action; the pseudocode helps to understand the application of the mapping rules to obtain the π-calculus definitions.Table 3
UML-RT transitions’ specification for the capsuleTopSystem and its subcapsules.
CapsuleTransitionUML-RT triggerUML-RT actionTopSystemInitial—setCT·portName(x)·send();setET·portName(y) ·send();SourceInitial——timeoutPort:timer—Signal:timeoutsendPortX—q·portName(x)·send();sendPortY—q·portName(y)·send();timeout2——RouterInitial——receivePortPort:ra = *rtdata;Signal:portNamealert·registerSPP(a);sendMsgPort:timerm·msg1 = b1;m·msg2 = b2;Signal:timeoutalert·msg(m)·send();waitPortPort:timer—Signal:timeoutConsumerTargetInitial——configPortPort:setPortaux  = *rtdata;Signal:portNames·registerSAP(aux);consumeMsgPort:sm = *rtdata;c1 = m·msg1;Signal:msgc2 = m·msg2;waitMsgPort:timer—Signal:timeoutExporterConsumerInitial——configPortPort:setPortaux = *rtdata;Signal:portNamet·registerSAP(aux);Initial1——Initial2——receiveMsgPort:tm = *rtdata;d1 = m·msg1;Signal:msgd2 = m·msg2;consumeMsg——exportMsg—export·msg(d1) ·send();msgConsumed——msgExported——waitMsgPort:timer—Signal:timeoutTable 4
Pseudocode of the transitions in the capsuleTopSystem and its subcapsules.
CapsuleTransitionTrigger pseudocodeAction pseudocodeTopSystemInitial—setCT send portName(x)setET send portName (y)SourceInitial——timeouttimer receive timeout( )—sendPortX—q send portName(x)sendPortY—q send portName(y)timeout2——RouterInitial——receivePortr receive portName(a)alert =asendMsgtimer receive timeout( )alert send msg(b1,b2)waitPorttimer receive timeout( )—ConsumerTargetInitial——configPortsetPort receive  portName (aux)s = auxconsumeMsgs receive msg(c1,c2)—waitMsgtimer receive timeout( )—ExporterConsumerInitial——configPortsetPort receive portName(aux)t = auxInitial1——Initial2——receiveMsgt receive msg(d1,d2)—consumeMsg——exportMsg—export send msg(d1)msgConsumed——msgExported——waitMsgtimer receive timeout( )—The structure diagrams of theTopSystem subcapsules are not provided because the majority of ports are public, so they can be seen in TopSystem structure diagram (shown in Figure 1). The only exception is the protected port timer presented in all TopSystem subcapsules. The port timer implements the protocol Timing (a built-in protocol of the RoseRT tool) and receives the timeout signal.In order to show how to apply the mapping rules to obtain theπ-calculus definition of a UML-RT capsule, we detail the mapping of the capsule Source.Using Definition1, the π-calculus definition of the capsule Source is the parallel composition of its state diagram definition and its structure diagram definition:
(36)Source(InputSet[Source])=new(RestrictedSet[Source])(Source_StructureDiagram∣Source_StateDiagram),
where
(37)InputSet[Source]={q},RestrictedSet[Source]={}-{q}={}.
So, we have
(38)Source(q)=(Source_StructureDiagram∣Source_StateDiagram).According to Definition2, the structure diagram of the capsule Source is the parallel composition of its subcapsules. As the capsule Source does not have subcapsules, the π-calculus definition of its structure diagram is the stop process:
(39)Source_StructureDiagram=0.Theπ-calculus definition of the Source state diagram, according to Definition 3, can be written as
(40)Source_StateDiagram=Source_Initial_Action·Source_S1〈InputSet[Source,InitialPoint,S1]〉.As theInitial transition does not have an action, using the Definition 9 it is omitted from the Source definition and we have
(41)InputSet[Source,InitialPoint,S1]={q},(42)InputSet[Source,S1]={q},(43)Source_StateDiagram=Source_S1〈q〉.Using the Definition4 and (42), the π-calculus definition of state S1, in the capsule Source, can be written as the sequence composition of its entry action and its unique outgoing transition
(44)Source_S1(q)=Source_S1_EntryAction·Source_S1_timeout.As theS1 entry action is not specified, according to Definition 5 it is omitted from the parent definition, so
(45)Source_S1(q)=Source_S1_timeout.Theπ-calculus definition of the transition timeout is made based on Definition 6. So, from (45), we have
(46)Source_S1(q)=Source_S1_timeout_trigger·Source_S1_ExitAction·P_S1_timeout_Action·Source_S2〈InputSet[Source,S1,S2]〉.The trigger of the transitiontimeoutis the unobservable action τ, based on Definition 8, because the trigger in UML-RT is specified by the receiving of a timeout signal as stated in Table 4. The S1 exit action is not specified, so according to Definition 5 it is omitted from the parent definition. There is no action in transition timeout, so its definition is omitted from the parent definition and InputSet[Source,S1,S2]=InputSet[Source,S2]={q}. From (46), the S1 definition in the π-calculus can be written as
(47)Source_S1(q)=τ·Source_S2〈q〉.TheS1 definition references the state S2. So, it is necessary to specify the π-calculus definition of state S2. So,byusing Definition 4, we have
(48)Source_S2(q)=Source_S2_EntryAction·(Source_S2_sendPortX+Source_S2_sendPortY).Using Definitions5 and 6, from (48), we have
(49)Source_S2(q)=((Source_S2_sendPortX_trigger·Source_S2_ExitAction·P_S2_sendPortX_Action·Source_S3〈InputSet[Source,S2,S3]〉)+(Source_S2_sendPortY_trigger·Source_S2_ExitAction·P_S2_sendPortY_Action·Source_S3〈InputSet[Source,S2,S3]〉)).Using Definitions5, 8, and 9, from (49) the π-calculus definition of S2 is written as
(50)Source_S2(q)=(q̅〈x〉·Source_S3〈q〉)+(q̅〈y〉·Source_S3〈q〉).However, theS2 definition references the state S3. So, it is also necessary to specify the π-calculus definition of the state S3. So, by using Definition 4, we have
(51)Source_S3(q)=Source_S3_EntryAction·Source_S3_timeout2.
Using Definitions 5 and 6, from (51), we have
(52)Source_S3(q)=Source_S3_timeout2_trigger·Source_S3_ExitAction·P_S3_timeout2_Action·Source_S1〈InputSet[Source,S3,S1]〉.Finally, using Definitions5, 8, and 9, from (51) the π-calculus definition of S3 is written as
(53)Source_S3(q)=τ·Source_S1〈q〉.From (47), (50), and (53), the π-calculus definition of the state S1 is
(54)Source_S1(q)=τ·((q̅〈x〉·τ·Source_S1〈q〉)+(q̅〈y〉·τ·Source_S1〈q〉)).Finally, using (38), (39), (43), and (54), the π-calculus definition of the capsule Source is given by
(55)Source(q)=Source_S1〈q〉Source_S1(q)=τ·((q̅〈x〉·τ·Source_S1〈q〉)+(q̅〈y〉·τ·Source_S1〈q〉)).Using the mapping rules and the specifications of transitions in Table4, it is possible to define the π-calculus definition of the other capsules that compose the TopSystem example, as written in
(56)Router(r)=Router_S1〈r〉Router_S1(r)=r(a)·Router_S2〈a,r〉Router_S2(alert,r)=τ·alert¯〈b1,b2〉·τ·Router_S1〈r〉(57)ConsumerTarget(setPort)=setPort(aux)·ConsumerTarget_S2〈aux,setPort〉ConsumerTarget_S2(s,setPort)=s(c1,c2)·τ·ConsumerTarget_S2〈s,setPort〉(58)ExporterTarget(setPort,export)=setPort(aux)·ExporterTarget_S4〈aux,setPort,export〉ExporterTarget_S4(t,setPort,export)=t(d1,d2)·(τ·ExporterTarget_S4〈t,setPort,export〉+(export¯〈d1〉·τ·ExporterTarget_S4〈t,setPort,export〉))(59)TopSystem(out)=newz,setCT,setET·(Source〈z〉∣Router〈z〉∣ConsumerTarget〈setCT〉·∣ExporterTarget〈setET,out〉∣setCT¯〈x〉·setET¯〈y〉).Through the definition of a capsule it is possible to capture the behavior of this capsule, for example, the capsuleSource in (55) executes an unobservable action (i.e., a timeout), sends the message x or y along the port q, and returns to a state (in this case S1), where it is possible to repeat the same behavior. Due to the connection between the subcapsules Source and Router in the capsule TopSystem, the parent capsule references its subcapsule Source renaming the port q to z, and references its subcapsule Router renaming the port r to z. Therefore, the message x or y sent by the subcapsule Source is received by the subcapsule Router, and it is stored in the name a, according to (56). The definition of Router_S1 references the definition of Router_S2 renaming alert with a, so the subcapsule Router is now able to send the messages b1 and b2 through the port alert, which can be x or y.The capsuleTopSystem in (59) sends x to its subcapsule ConsumerTarget and sends y to its subcapsule ExporterTarget. According to (57), the subcapsule ConsumerTarget configures its port s with x to be able to receive the message from the capsule Router. Similarly, according to (58), the subcapsule ExporterTarget configures its port t with y to be able to receive the message from the capsule Router. After receiving the message from the Router, the control of the subcapsule ExporterTarget can return to ExporterTarget_S4, or it can send the received message through its port export and later the control returns to ExporterTarget_S4. Note that the port export is in fact renamed to out, which is a public interface of the capsule TopSystem, according to (59).In the example, theπ-calculus definitions corresponding to the UML-RT model were specified. Using the generated π-calculus definitions, it is possible to analyze the interactions between the system components, therefore some undesirable system behavior can be uncovered during the modeling phase.


## 4.2. Heating System

In this section, we use an example of a system, which was adapted from the example described in [10] and is called Heating System for Air Conditioning. In this example, the system requirements are provided as well as the UML-RT model that implements the requirements. Furthermore, the π-calculus definitions for the system are generated following the mapping rules. Some scenarios are proposed according to the system requirements. Later, we compose the π-calculus definitions of the system and the scenarios in order to verify if the model meets the requirements. The handlings are made manually.The heating system consists of the standard heating subsystem and the additional heating subsystem that is used to shorten the time needed to increase the temperature in the car. The specification of the heating system is provided through the requirements R1 to R7. In the requirements’ descriptions we anticipate the UML-RT states of the state diagrams of this section. They are named between parentheses. The requirements are as follows.R1
The heating system has two levels: level1 (Level1 state) and level2 (Level2 state). In level1 only the standard heating system is active, while in level2 the additional heating system is also active.R2
An incoming init event changes the heating system’s status from shutdown (Shutdown state) to level1 and from start (Start state) to level2.R3
The heating system automatically changes its status from level2 to level1 after 10 minutes.R4
The heating system automatically changes its status from start to shutdown after 10 minutes.R5
Exceptions regarding invalid voltage or ignition key in status “cold” immediately cause deactivation of the heating system for 10 seconds.R6
As soon as there is no more exception, the heating system continues operating on the selected level.R7
The heating system’ status changes to shutdown if the ignition key stays in status “cold” for 5 minutes, or if the key is removed.The heating system model (Figure9) was constructed using the RoseRT tool. It is a capsule called HeatingSystem composed of three subcapsules: low (instance of the capsule LowExceptions in Figure 10), high (instance of the capsule HighExceptions in Figure 11), and controller (instance of the capsule HeatingController in Figure 12). The interface of the HeatingSystem is the ports to receive the ignition status (KL15off, KL15radio, and KL15cold), the voltage invalid status (iVolt), the signal to start and shutdown the controller operation (startController and shutdownController, resp.). The specification of the transitions inside each capsule state diagram is in Table 5; whereas the entry and exit actions of the states are detailed in Table 6.Table 5
Transitions in theHeatingSystem subcapsules.
CapsuleTransitionUML-RT triggerUML-RT actionLowExceptionsInitial——receiveExceptionPort:ignitionColdoff·sig()·send();Signal:sigPort:invalidVoltageSignal:sigexpireExceptionPort:timeron·sig()·send();Signal:timeoutHighExceptionsInitial——receiveIgnitionKeyRadioPort:ignitionRadioon·sig()·send();Signal:sigreceiveIgnitionKeyColdPort:ignitionCold—Signal:sigreceiveIgnitionKeyRadio2Port:ignitionRadio—Signal:sigreceiveIgnitionKeyOffPort:ignitionOffoff·sig()·send();Signal:sigafter5minutesPort:timeroff·sig()·send();Signal:timeoutHeatingControllerInitial——InitiatePort:on—Signal:sigPort:initSignal:sigTerminatePort:off—Signal:sigPort:endSignal:sigAfter10minutesPort:timer—Signal:timeoutTable 6
Entry and exit actions of the states in theHeatingSystem subcapsules.
CapsuleStateEntry actionExit actionLowExceptionsOkayLPrio——OffLPriotimer·informIn(RTTimespec(10,0));—HighExceptionsOffHPrio——OkayHPrio——WaitHPriotimer·informIn(RTTimespec(300,0));—HeatingControllerStarttimer·informIn(RTTimespec(600,0));—Level2out·msg(L2)·send();—timer·informIn(RTTimespec(600,0));Level1out·msg(L1) ·send();—Shutdownout·msg(BAD) ·send();—Figure 9
The structure diagram of the capsuleHeatingSystem.Figure 10
The state diagram of the capsuleLowExceptions.Figure 11
The state diagram of the capsuleHighExceptions.Figure 12
The state diagram of the capsuleHeatingController.The capsuleLowExceptions starts at the state OkayLPrio and changes to OffLPrio, if it receives a signal through the port ignitionCold or invalidVoltage. During this transition, the capsule sends a signal through the port off in order to shutdown the heating controller temporarily. After 10 seconds, the capsule LowExceptions is ready to receive more exception information, when it returns to the state OkayLPrio.The capsuleHighExceptions starts at the state OffHPrio and changes to OkayHPrio, if it receives a signal through the port ignitionRadio. This transition executes an action of sending a signal along the port on in order to start the heating controller, because there is no more high exception to be handled. After receiving a signal through the port ignitionCold at the state OkayHPrio, the capsule HighExceptions changes to the state WaitHPrio. At the state WaitHPrio, the capsule can change to the state OkayHPrio if the ignition returns to the status radio; or it can detect a high exception if the ignition exceeds 5 minutes in the status cold, or if the ignition changes to the status off. In case of detecting a high exception, the capsule sends a signal along the port off aiming to shutdown the heating controller.The capsuleHeatingController begins at the state Start and changes to Level2 if it receives a signal through the ports on or init. At the state Level2, the capsule can changes to the state Level1 after 10 minutes, or it can shutdown after receiving a signal along the ports off or end. At the state Level1, the capsule can shutdown too. The capsule is able to notify its status in each state sending a message through the port out.Some system requirements can be verified by a visual inspection in the model, for example, the requirements R1 to R4 are addressed by the transitions specified in the state diagram of the capsuleHeatingController. Other requirements are modeled, for example, R5 to R7, however we do not know if the behavior of the system interacting components complies with the requirements. In order to verify some properties originated immediately from the requirements, we can use the system formal specification in the π-calculus.Theπ-calculus definitions of the heating system are provided below; however we omit the capsule name in each state name due to space limitation
(60)HeatingSystem(KL15radio,KL15cold,KL15off,iVolt,startController,shutdownController,heatingStatus)=newon,off(HeatingController〈Set1Ref〉∣LowExceptions〈Set2Ref〉∣HighExceptions〈Set3Ref〉),
where
(61)Set1Ref={startController,shutdownController,on,off,heatingStatus},Set2Ref={KL15cold,iVolt,on,off},Set3Ref={KL15radio,KL15cold,KL15off,on,off}.DeclaringSet1={init,end,on,off,out} as the input set of HeatingController definition, we have
(62)HeatingController(List1)=Start〈Set1〉Start(Set1)=(on+init)·Level2〈Set1〉+τ·Shutdown〈Set1〉Level2(Set1)=out¯〈L2〉·((off+end)·Shutdown〈Set1〉+τ·Level1〈Set1〉)Level1(Set1)=out¯〈L1〉·((off+end)·Shutdown〈Set1〉)Shutdown(Set1)=out¯〈BAD〉·((on+init)·Level1〈Set1〉).Declaringet2={ignitionCold,invalidVoltage, on,  off} as the input set of LowExceptions definition, we have
(63)LowExceptions(Set2)=OkayLPrio〈Set2〉OkayLPrio(Set2)=(ignitionCold+invalidVoltage)·off¯·OffLPrio〈Set2〉OffLPrio(Set2)=τ·on¯·OkayLPrio〈Set2〉.DeclaringSet3 = {ignitionRadio, ignitionCold, ignitionOff, on, off} as the input set of HighExceptions definition, we have
(64)HighExceptions(Set3)=OffHPrio〈Set3〉OffHPrio(Set3)=ignitionRadio·on¯·OkayHPrio〈Set3〉OkayHPrio(Set3)=ignitionCold·WaitHPrio〈Set3〉WaitHPrio(Set3)=ignitionRadio·OkayHPrio〈Set3〉+ignitionOff·off¯·OffHPrio〈Set3〉+τ·off¯·OffHPrio〈Set3〉.After obtaining the definitions of the components in the model, it is desirable to verify its properties. In order to verify the requirements R5 and R6, we assume the scenario where an external actor sends astartController¯ event and, later, it sends an iVolt¯ event. The scenario can be specified as
(65)Scenario1=startController¯·heatingStatus(s1)·iVolt¯·heatingStatus(s2)·heatingStatus(s3).
After the startController¯ event, the information that the system is at the level2 is expected, so s1 will receive “L2”. After the iVolt¯ event, the information that the system is shutdown is due, so s2 will receive “BAD”. After the timeout of the low exception (in this case, the invalid voltage), the information that the system is at the level2 is waited, so s3 will be “L2”, because the requirement R6 specifies that the system has to return to the selected level after the exceptions.Composing the heating system and the scenario, we obtain(66)HeatingSystem(KL15radio,KL15cold,KL15off,iVolt,startController,shutdowController,heatingStatus)∣Scenario1.Using (60) and (65), we have
(67)newon,off(HeatingController〈Set1Ref〉∣LowExceptions〈Set2Ref〉∣HighExceptions〈Set3Ref〉)∣(startController¯·heatingStatus(s1)·iVolt¯·heatingStatus(s2)·heatingStatus(s3)).Replacing the definitions of theHeatingSystem subcapsules, we obtain
(68)newon,off(((on+startController)·Level2〈Set1Ref〉+τ·Shutdown〈Set1Ref〉)∣((KL15cold+iVolt)·off¯·OffLPrio〈Set2Ref〉)∣(KL15radio·on¯·OkayHPrio〈Set3Ref〉)∣(startController¯·heatingStatus(s1)·iVolt¯·heatingStatus(s2)·heatingStatus(s3))).After the reaction betweenstartController¯ and startController, we have
(69)newon,off(Level2〈Set1Ref〉∣((KL15cold+iVolt)·off¯·OffLPrio〈Set2Ref〉)∣(KL15radio·on¯·OkayHPrio〈Set3Ref〉)∣(heatingStatus(s1)·iVolt¯·heatingStatus(s2)·heatingStatus(s3))).Replacing the definition ofLevel2〈Set1Ref〉, we obtain
(70)newon,off((heatingStatus¯〈L2〉·((off+shutdownController)·Shutdown〈Set1Ref〉+τ·Level1〈Set1Ref〉))∣((KL15cold+iVolt)·off¯·OffLPrio〈Set2Ref〉)∣(KL15radio·on¯·OkayHPrio〈Set3Ref〉)∣(heatingStatus(s1)·iVolt¯·heatingStatus(s2)·heatingStatus(s3))).After the reaction betweenheatingStatus¯〈L2〉 and heatingStatus(s1), the name s1 receives the message “L2” as required in the scenario specification. So,
(71)newon,off(((off+shutdownController)·Shutdown〈Set1Ref〉+τ·Level1〈Set1Ref〉)∣((KL15cold+iVolt)·off¯·OffLPrio〈Set2Ref〉)∣(KL15radio·on¯·OkayHPrio〈Set3Ref〉)∣(iVolt¯·heatingStatus(s2)·heatingStatus(s3))).After the reaction betweeniVolt¯ and iVolt, we have
(72)newon,off(((off+shutdownController)·Shutdown〈Set1Ref〉+τ·Level1〈Set1Ref〉)∣(off¯·OffLPrio〈Set2Ref〉)∣(KL15radio·on¯·OkayHPrio〈Set3Ref〉)∣(heatingStatus(s2)·heatingStatus(s3))).After the reaction betweenoff¯ and off, we obtain
(73)newon,off(Shutdown〈Set1Ref〉∣OffLPrio〈Set2Ref〉∣(KL15radio·on¯·OkayHPrio〈Set3Ref〉)∣(heatingStatus(s2)·heatingStatus(s3))).Replacing the definition ofShutdown and OffLPrio, we have
(74)newon,off((heatingStatus¯〈BAD〉·((on+startController)·Level1〈Set1Ref〉))∣(τ·on¯·OkayLPrio〈Set2Ref〉)∣(KL15radio·on¯·OkayHPrio〈Set3Ref〉)∣(heatingStatus(s2)·heatingStatus(s3))).After the reaction betweenheatingStatus¯〈BAD〉 and heatingStatus(s2), the name s2 receives the message “BAD” as required in the scenario specification. So,
(75)newon,off(((on+startController)·Level1〈Set1Ref〉)∣(τ·on¯·OkayLPrio〈Set2Ref〉)∣(KL15radio·on¯·OkayHPrio〈Set3Ref〉)∣heatingStatus(s3)).After theτ  reaction that represents the 10 seconds after the low exception, we obtain
(76)newon,off(((on+startController)·Level1〈Set1Ref〉)∣(on¯·OkayLPrio〈Set2Ref〉)∣(KL15radio·on¯·OkayHPrio〈Set3Ref〉)∣heatingStatus(s3)).After the reaction betweenon¯ and  on, we have
(77)newon,off(Level1〈Set1Ref〉∣OkayLPrio〈Set2Ref〉∣(KL15radio·on¯·OkayHPrio〈Set3Ref〉)∣heatingStatus(s3)).Replacing the definition ofOkayLPrio, we obtain
(78)newon,off((heatingStatus¯〈L1〉·(off+shutdownController)·shutdown〈Set1Ref〉))∣OkayLPrio〈Set2Ref〉∣(KL15radio·on¯·OkayHPrio〈Set3Ref〉)∣heatingStatus(s3)).Now there is the possibility of the reaction betweenheatingStatus¯〈L1〉 and heatingStatus(s3), then the name s3 receives the message “L1”. Note that the heating system is in level1, which is an active status, so the requirement R5 is satisfied. Otherwise, the requirement R6 is not met, because the heating system was at level2 before the low exception and now it is at level1, when it should continue in level2. In this example, the designer can uncover the error in the model analyzing the state diagrams; however in a more complex system, the visual analysis is very difficult, so the formal analysis is necessary.Aiming to verify the requirement R7, we propose a scenario composed by the following steps: the ignition key is in status radio, an external event initiates the controller and, later, the ignition key is in status off. The scenario is specified as(79)Scenario2=KL15radio¯·startController¯·heatingStatus(s1)·KL15off¯·heatingStatus(s2).After thestartController¯ event, it is expected to be informed that the system is at the level2, so s1 will receive “L2”. After the KL15off¯ event, it is expected to be informed that the system is shutdown, so s2 will receive “BAD”. Analyzing this scenario, we note that, after receiving the event startController¯, the HighExceptions capsule sends the event on¯ to initiate the heating controller. So, a component to manage exceptions can initiate the controller for the first time, before it has been initiated by the external event startController¯. In this case, we obtain an unexpected behavior according to the proposed scenario; however we are not sure if it is an error in the model or a missing requirement specification.Then, using the system specification in theπ-calculus and the scenarios or properties proposed according to the system requirements, it is possible to analyze the interaction between the system components and find out the undesirable behavior due to errors in  modeling or and a lack of specification.


## 4.3. Handover Protocol

In this section, we show the example of mobile processes called Handover Protocol presented by Milner in [24]. The Handover system (Figure 13) is composed by a control tower (Control capsule), two communicating towers (Trans capsules: trans1 and trans2), and a car (capsule Car). For a better visualization of Figure 13, the protocol type of each port is omitted. The control tower has fixed connections with the communicating towers; it is expressed through the wired ports between the capsule Control and the two capsules Trans. The car communicates with a Trans tower, but an event can make it communicates with the other Trans.Figure 13
The structure diagram of the capsuleHandover.The state diagrams of the capsulesCar, Trans, and Control are presented in  Figure 14. The state diagram of the top level capsule Handover is not shown; however it is composed only by the initial transition and an initial state called S1. The UML-RT specifications for the transitions of all capsules are available in Table 7.Table 7
Transitions in the capsuleHandoverand its subcapsules.
CapsuleTransitionUML-RT triggerUML-RT actionHandoverInitial—m·talk = talk1;m·change = change1;setCar·signal(m)·send();CarInitial——startPort:setCarm = *rtdata;t = m·talk;Signal:signalc = m·change;talk·registerSAP(t);change·registerSAP(c);updateConnectionPort:changem = *rtdata;t = m·talk;Signal:signalc = m·change;talk·registerSAP(t);change·registerSAP(c);communicatePort:timertalk·signal(info)·send();Signal:timeoutTransInitial——activatePort:gainm = *rtdata;t = m·talk;Signal:signalc = m·change;talk·registerSPP(t);change·registerSPP(c);deactivatePort:losem = *rtdata;t  = m·talk;c = m·changeSignal:signalm2·talk = t;m2·change = c;change·signal(m2)·send();communicatePort:talkmyinfo = *rtdata;Signal:signalControlInitial—m·talk = talk1;m·change = change1;gain1·signal(m)·send();startControl1Port:timerm·talk = talk1;m·change = change1;Signal:timeoutlose2·signal(m)·send();gain1·signal(m)·send();startControl2Port:timerm·talk = talk2;m·change = change2;Signal:timeoutlose1·signal(m)·send();gain2·signal(m)·send();The state diagrams of the capsules: (a)Car,  (b) Trans, and  (c) Control.
(a)(b)(c)The overall behavior is the following. the transitionInitial of the capsule Handover sends two messages talk1 and change1 along the protected setCar. The messages are received by the car in order to make the initial configuration of its unwired ports talk and change. On the other hand, when control initializes, it sends to trans1 the messages talk1 and change1 that are used by trans1 to configure the unwired ports talk and change. At this moment, the car is able to communicate to trans1 by sending a message through the port talk.However,controlcan activate the trans2. In this case, the control sends the messages talk2 and change2 to trans1 (via the port lose1) and to trans2 (via the port gain2). The trans1 receives the messages talk2 and change2, and it sends to the car (via the port change). So, the car uses the messages to reconfigure its unwired ports talk and change. Besides, the trans2 receives the messages talk2 and change2 from the control to configure its unwired ports talk and change. At this moment, the car is able to communicate to trans2 by sending a message through the port talk.Thecontrol continues its processing either activating trans1 or activating trans2. It allows the car always to communicate to some tower, that is, trans1 or trans2.It is desirable to obtain theπ-calculus definition of the Handover system, so it is important to analyze each capsule based on Figure 14 and Table 7in order to apply the mapping rules proposed in Section 3.Analyzing the capsuleCar, in the transition start, it receives the messages t and c in order to make the initial configuration of its unwired ports. After the initial configuration, Car in the state Operating is ready to send the message info to a tower through the port talk. However, Car can also receive from trans1 two messages (t and c) simultaneously along the port change, indicating a new name for the port talk and a new name for the port change, respectively. This is the step that the car reconfigures its ports to start to operate with the other tower. Then, the π-calculus definition of the capsule Car is written as
(80)Car(setCar)=Car_Idle〈setCar〉Car_Idle(setCar)=setCar(t,c,setCar)·Car_Operating〈t,c,setCar〉Car_Operating(talk,change,setCar)=τ·talk¯〈info〉·Car_Operating(talk,change,setCar)+change(t,c)·Car_Operating(talk,change,setCar).The towerTrans begins in the state Idle, where it is possible to receive the configuration for its unwired ports talk and change via the transition activate. In the Active state, Trans can receive a message myinfo from Car using the transition communicate. However, Trans can also receive a message from Control with the new names t and c. These names are later sent to Car via the port change and indicate how its unwired ports must be reconfigured. Using the mapping rules, the capsule Trans is defined in the π-calculus as
(81)Trans(gain,lose)=Trans_Idle〈gain,lose〉Trans_Idle(gain,lose)=gain(t,c)·Trans_Active(t,c,gain,lose)Trans_Active(talk,change,gain,lose)=talk(myinfo)·Trans_Active(talk,change,gain,lose)+lose(t,c)·change¯〈t,c〉·Trans_Idle〈gain,lose〉.The state diagram ofControl initiates (transition Initial) sending the messages talk1 and change1 along the port gain1. In the Control1 state, after a timeout (transition startControl2), Control can send the messages talk2 and change2 through the port lose1, and later through the port gain2. In a similar way, in the Control2 state, after a timeout (transition startControl1), Control can send the messages talk1 and change1 through the port lose2, and later through the port gain1. In this way, the transition startControl2 indicates that trans2 is apt to talk with the car; while the transition startControl1 indicates that trans1 is now ready to talk with the car. Then, the π-calculus definition of the capsule Control is written as
(82)Control(gain1,lose1,gain2,lose2)=gain1¯〈talk1,change1〉·Control_Control1〈gain1,lose1,gain2,lose2〉Control_Control1(gain1,lose1,gain2,lose2)=τ·lose1¯〈talk2,change2〉·gain2¯〈talk2,change2〉·Control_Control2〈gain1,lose1,gain2,lose2〉Control_Control2(gain1,lose1,gain2,lose2)=τ·lose2¯〈talk1,change1〉·gain1¯〈talk1,change1〉·Control_Control2〈gain1,lose1,gain2,lose2〉.Finally, theHandover system is defined in the π-calculus as the parallel composition of the definition of its state diagram and its structure diagram definition.  The state diagram definition is the possibility to send the messages talk1 and change1 along the port setCar. The structure diagram definition includes a reference to each subcapsule definition. So, the Handoverdefinition is written as
(83)Handover()=new(setCar,zgain1,zlose1,zgain2,zlose2)(Car〈setCar〉∣Trans〈zgain1,zlose1〉∣Trans〈zgain2,zlose2〉∣Control〈zgain1,zlose1,zgain2,zlose2〉∣setCar¯〈talk1,change1〉).It is important to understand each term in the parallel composition shown in (83). The first term represents the subcapsule car (instance of Car). The second and the third terms represent the subcapsules trans1 and trans2 (instance of Trans), respectively. The fourth term indicates the subcapsule control (instance of Control). The last term is the definition of the Handover state diagram. Besides, the names setCar, zgain1, zlose1, zgain2, zlose2 are used to represent the wired connections between the subcapsules in the π-calculus definitions. For example, the name zgain1 allows the communication between the port gain1 of control and the port gain of trans1, because the subcapsule’s ports are renamed to the same name zgain1.The Handover system is an example of mobile processes, where the messages received by a process in a communication can be used to rename its ports and, consequently, to allow the reconfiguration of its connections with other processes. Besides, the present example includes the need of the communication of more than one message at a time between processes, which emphasizes the importance of the polyadicπ-calculus approach.


## 5. Comments and Conclusions

We propose a formal semantics to the UML-RT communicating elements through the mapping from the UML-RT to the polyadicπ-calculus. The UML-RT is a UML profile widely used for the real-time system modeling, and the π-calculus is one of the main formalisms of the concurrent systems modeling. The proposed mapping from the UML-RT to the π-calculus is a practical approach of π-calculus, and it enables the use of formal methods during system development.We described three examples. In the first example, we explained how to obtain theπ-calculus definition of a UML-RT model using the proposed mapping rules. In the second example, we illustrated the possibility to formally verify system requirements using the π-calculus definitions of the model and some scenarios specified from the requirements. During the verification process, we showed that we can uncover some undesirable behavior, which are consequences of a poor system specification or an error introduced during the modeling phase. Finally, in the third example, we present the Handover protocol. This example demonstrates the importance of the reconfiguration of the connections between processes and the need of modeling of communication of more than one message at a time, which is well addressed using the polyadic π-calculus.A real-time system designer who desires to formally reason about a UML-RT model can apply the proposed mapping rules on the UML-RT model to obtain the correspondingπ-calculus definitions. Afterwards, the designer can manipulate the π-calculus definitions to explore possible execution paths and find situations that can cause functional problems or inconsistencies with functional requirements. Problems and inconsistencies include deadlock and nonsatisfaction of safety properties. This practice increases the confidence in the system development, because it anticipates the detection of problems in the modeling phase.Two main contributions of the mapping proposed in this paper are due to polyadicπ-calculus mobility, which is provided by name reconfiguration. The first contribution is the reuse of the capsule definition. For example, if a parent capsule has three instances of the same subcapsule, it is necessary to write one definition in the π-calculus for the subcapsule, and this definition is referenced three times by the parent capsule. It helps to reduce the number of the π-calculus definitions for the system. The second contribution of the name reconfiguration is the ability to represent the dynamic configuration of the unwired ports. It is important because a UML-RT capsule can rename an unwired port during its state diagram execution, as it is shown in the first example.Other contributions include the option for the polyadicπ-calculus, which represents the communication of more than one message at a time. Besides, the proposed mapping deals with the following UML-RT concepts not yet addressed: the entry and the exit actions of a state, the composite states, and the transition chains.In order to test the consistency of the mapping rules, we used the mapping to obtainπ-calculus models of other UML models, besides the examples presented in this work. For instance, we have used the mapping on a system composed by a pair of semaphores to prove that two green lights of both semaphores cannot occur at the same time.Future research directions include the improvement of the mapping rules to represent other UML-RT elements, such as history junction points, the guard conditions, and the capsule cardinalities. An interesting topic to investigate is to capture, from the UML-RT sequence diagram, theπ-calculus definitions of the desirable scenarios to be met by the system under design. Another research issue is the study of formal approaches to represent the UML-RT timeouts, in order to be able to verify the time constraints of the modeled system.



---

*Source: 656810-2009-08-13.xml*