Rede Celular
Patrícia Muniz Ferreira
Sidney Nogueira
À Rede Celular
MSC
CEL0
ERB0
CEL1
ERB1
CEL2
CEL(origem) -> ERB(origem) -> MSC ->
ERB(destino) -> CEL(destino) -> ERB(destino) -> MSC ->
ERB(origem) -> CEL(origem)
Roteiro do Projeto

1a parte

Especificação CSP (FDR)
• CELULAR
• ERB
• MSC
CELs = (||| c:ConjuntoCel@CELULAR(c))
ERBs = (||| e:ConjuntoERB@ERB(e))
REDE_CELULAR =
(CELs [| chs_CEL_ERB |] ERBs)
[| chs_ERB_MSC |]
MSC
assert REDE_CELULAR :[ deadlock free [FD] ]
assert REDE_CELULAR :[ livelock free [FD] ]
assert REDE_CELULAR :[ deterministic [FD] ]
Roteiro do Projeto

2a parte

(Z-Eves)
• Esquemas Z de cada operação em CSP
do CELULAR
• Prova dos esquemas
Roteiro do Projeto
Roteiro do Projeto

2a parte

(Z-Eves)
• Esquemas Z de cada operação em CSP
do CELULAR
• Prova dos esquemas
• Refinamento de dados
Roteiro do Projeto
Roteiro do Projeto

2a parte

(Z-Eves)
• Esquemas Z de cada operação em CSP
do CELULAR
• Prova dos esquemas
• Refinamento de dados

(FormW)
• Criação do CSP-Z
Roteiro do Projeto
Roteiro do Projeto

2a parte

(Z-Eves)
• Esquemas Z de cada operação em CSP
do CELULAR
• Prova dos esquemas
• Refinamento de dados

(FormW)
• Criação do CSP-Z
• Conversão para CSPM
Roteiro do Projeto
Roteiro do Projeto

2a parte

(Z-Eves)
• Esquemas Z de cada operação em CSP do
CELULAR
• Prova dos esquemas
• Refinamento de dados

(FormW)
• Criação do CSP-Z
• Conversão para CSPM

Equivalência no FDR
Roteiro do Projeto
-- EQUIVALENCIA PROCESSO A PROCESSO
assert CELULAR(CEL0) [T= CELULAR_CSPZ(CEL0,areaCoberturaCelular(CEL0))
assert CELULAR(CEL0) [F= CELULAR_CSPZ(CEL0,areaCoberturaCelular(CEL0))
assert CELULAR(CEL0) [FD= CELULAR_CSPZ(CEL0,areaCoberturaCelular(CEL0))
assert CELULAR_CSPZ(CEL0,areaCoberturaCelular(CEL0)) [T= CELULAR(CEL0)
assert CELULAR_CSPZ(CEL0,areaCoberturaCelular(CEL0)) [F= CELULAR(CEL0)
assert CELULAR_CSPZ(CEL0,areaCoberturaCelular(CEL0)) [FD= CELULAR(CEL0)
-- EQUIVALENCIA SISTEMA A SISTEMA
REDE_CELULAR_CSPZ = (CELs_CSPZ [| chs_CEL_ERB |] ERBs) [| chs_ERB_MSC |] MSC
assert REDE_CELULAR [T= REDE_CELULAR_CSPZ
assert REDE_CELULAR [F= REDE_CELULAR_CSPZ
assert REDE_CELULAR [FD= REDE_CELULAR_CSPZ
assert REDE_CELULAR_CSPZ [T= REDE_CELULAR
assert REDE_CELULAR_CSPZ [F= REDE_CELULAR
assert REDE_CELULAR_CSPZ [FD= REDE_CELULAR
-- PROPRIEDADES DO SISTEMA
assert REDE_CELULAR_CSPZ :[ deadlock free [FD] ]
assert REDE_CELULAR_CSPZ :[ livelock free [FD] ]
assert REDE_CELULAR_CSPZ :[ deterministic [FD] ]
Considerações
Entendimento de dados com Z
 Reuso (parcial) entre os modelos do
Z-EVES e FormW
 Limitações do FormW (readme.txt)
 Conhecimento do processo
CSP -> Z -> CSPZ -> CSPM
