Uma Visão em CSP para os Diagramas de UML-RT

Uma Visão em CSP para os Diagramas de UML-RT

Alexandre Mota(acm@cin.ufpe.br)

Objetivos Apresentar uma formalização dos

diagramas de UML-RT em (Object-)Z

Apresentar tradução de UML-RT em CSP

Exemplos de UML-RT

capsule CapsA capsule CapsB

capsuleCapsX

capsuleCapsY

c1

p1 q1

c2

p2 q2

c3

r1

capsule A3

q

capsule B3

p

c {u,v,w}

System2

System1

System1 em CSPSejam CapsX, CapsY, CapsB classes em CSP-OZ

CapsX[RX] {c1}||{c1,c2} CapsY[RY]RX={p1 c1}

RY={q1 c1, p2 c2}

{

capsuleCapsX

capsuleCapsY

c1

p1 q1 p2

c2

System1 em CSP

CapsA=(CapsX[RX] {c1}||{c1,c2} CapsY[RY])[c2 q2]\{c1}

capsule CapsA

capsuleCapsX

capsuleCapsY

c1

p1 q1

c2

p2 q2

System1 em CSP

capsule CapsA capsule CapsB

capsuleCapsX

capsuleCapsY

c1

p1 q1

c2

p2 q2

c3

r1

System1

System1=(CapsA[q2 c3] {c3}||{c3} CapsB[r1 c3])\{c3}

System2 em CSP

A(Adrp)=Produce(e) ; (|||out:Adrp p.out!eSKIP) ; A(Adrp)

Onde Adrp será instanciado com {u,v,w}

capsule A3

p

{u,v,w}

System2 em CSP

B=(q?xSKIP); Consume(x) ; B

q

capsule B3

{u,v,w}

MB=|||in:{u,v,w} B[q q.in]

B[q q.in] =(q.in?xSKIP) ; Consume(x) ; B[q q.in]

System2 em CSP

System2=(A({u,v,w})[p c] {c}||{c} MB[q c])\{c}

capsule A3

q

capsule B3

p

c {u,v,w}

System2

Convenções da Proposta Portas brancas são de entrada (?) Portas pretas são de saída (!) Cápsulas múltiplas só podem ter uma

porta Composição entre cápsula simples e

cápsula múltipla induz em uso de potras múltiplas na cápsula simples

Entre duas portas só pode haver um conector (Comunicação binária)

Nomes de cápsulas são únicos

Formalização de Diagramas de UML-RT em Z

[PortName, ConName, CapName, InstName]

Colour ::= black | white

name: PortNamecname: CapNamecolour: ColourMulti: IN1

colour = white multi = 1

Port

Formalização de Diagramas de UML-RT em ZConnector

name: ConNameports: IF Port# ports = 2

C: CapName Capsule na: dom C na = C(na).name

^

name: CapNameports: IF Port p: ports p.cname = name

Capsule

Formalização de Diagramas de UML-RT em ZCompCapsule

inherit Capsule

scnames: IF CapNameconn: IF Connector

c: conn c.ports ports {sn: scnames C(sn).ports} c1,c2: conn c1.ports c2.ports c1 = c2

c: conn p, p’: c.ports p p’ p.cname p’.cname c: conn p, p’: c.ports (p p’

(p ports p.multi = p’.multi p.colour = p’.colour)(p,p’ ports p.colour p’.colour

((p.multi=1 p’.multi = C(p.cname).multi)(p’.multi=1 p.multi = C(p’.cname).multi))

Formalização de Diagramas de UML-RT em Z

MultiCapsule

scname: CapNamemulti: IN1

inames: IF InstName# inames = multi

inherit Capsule

Tradução de Diagramas em UML-RT para CSP

[Process, Chans, Val]

Data ::= basic Val | comp InstName Data

Events == Chans Data

: Process IP Events

T: Capsule ProcessEquations

Tradução de Diagramas em UML-RT para CSP

(1) Seja BC uma cápsula básica com BC.ports={p1, ..., pm, q1 , ..., qn}, onde m, n IN e p1, ..., pm são portas simples (pi.multi=1, i=1, ..., m) e q1

, ..., qn são portas múltiplas (qj.multi>1, j=1, ..., n). Então, assumimos novos parâmetros formais Adr1, ..., Adrn representando conjuntos de nomes de instâncias, que servirão de endereços para onde as portas múltiplas poderão conectar-se

T(BC) BC.name(Adr1, ..., Adrn) = RHSOnde RHS é o nome da classe CSP-OZ correspondente

Tradução de Diagramas em UML-RT para CSP

(2) Seja CC uma cápsula composta com CC.ports={p1, ..., pm,q1 , ..., qn} e Adr1, ..., Adrn como na regra (1)

T(CC)

CC.name(Adr1, ..., Adrn) =

((||SN:CC.scnames[C(SN).ports[RSN,CC]]

SN(B1, ..., Bk(SN))[RSN,CC])[PCC])\HCCT(C(SN)), para todo SN: CC.scnames

Tradução de Diagramas em UML-RT para CSP

Bi=Adrpj, se ri estiver conectado a uma porta

múltipla pública pj de CC

Bi=MC.inames, se ri estiver conectado a uma

porta simples pj de uma cápsula múltipla MC

dentro de CCRSN, CC={pn: PortName; cn: ConName |

p: C(SN).ports; c: CC.conn p c.ports pn=p.name cn=c.name (pn cn)}

Suponha que r1, ..., rk(SN) sejam as portas-múltiplas da sub-cápsula de nome SN

Tradução de Diagramas em UML-RT para CSP

PCC={cn: ConName; pn: PortName | p: CC.ports; c: CC.conn p c.ports pn=p.name cn=c.name (cn pn)}

HCC={c: CC.conn c.name}

Tradução de Diagramas em UML-RT para CSP

(3) Seja MC uma cápsula múltipla com C(MC.cname).ports={p1, ..., pm, q1 , ..., qn} e Adr1, ..., Adrn como na regra (1) e (2)

T(MC)

MC.name(Adr1, ..., Adrn) =

|||in:MC.inamesMC.scname(Adr1, ..., Adrn)[ in ]

T(C(MC.scname)))

( )

P[ in ]=P[{ch: Chans; d: Data | ch.d (P) ch.d ch.in.d}]

( )

Referências Fischer, C., Olderog, E.R., e

Wehrheim, H. A CSP View on UML-RT Structure Diagrams. FASE 2001, LNCS 2029, pp. 91-108