Embed Size (px)
DESCRIPTION
Uma Visão em CSP para os Diagramas de UML-RT. Alexandre Mota ([email protected]). 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. System1. capsule CapsA. capsule CapsB. capsule CapsX. - PowerPoint PPT Presentation
Citation preview
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
