CSP-Z e sua Verificação
Alexandre Mota and Augusto Sampaio





Motivação
A Linguagem CSP-Z
Um Exemplo: O Relógio de Parede
Verificação Automática de CSP-Z
Traduzindo CSP-Z para CSPM
Motivação

Combinando Teorias e Ferramentas
Capturar todas as propriedades de um sistema

Elegância da Especificação
Aspectos do sistema em módulos distintos

Verificação Automática (Model-Checking)
“Provador de teoremas automático”
CSP-Z
Integração formal entre CSP e Z
 Captura tanto aspectos concorrentes quanto
de estruturas de dados de um sistema
 É uma extensão conservativa de CSP e Z,
com diferenças mínimas em ambas
 O refinamento de CSP-Z pode ser obtido
pelo de CSP ou o de Z com restrições

Exemplo: Relógio de Parede

Dois eventos são visíveis pelo ambiente: ticktack e bird

Ao ocorrer ticktack, o contador do relógio aumenta em 1 min

Quando o contador atinge 60 min, o relógio volta ao seu
estado inicial e mostra um passarinho (bird)
counter
counter == 60
10
20
30
40
50
0
Cookoo
Relógio em CSP-Z
SOUND ::= Cookoo
spec Clock
channel ticktack: []
channel bird: [msg: SOUND]
main = ticktackmain  bird!msgmain
State =^ [Min:N]
Init =^ [State’|Min’=0]
com_ticktack
com_bird
D State
D State
msg!:SOUND
Min<60
Min=60
Min’=Min+1
Min’=0
msg!=Cookoo
end_spec Clock
Interpretação Operacional de
CSP-Z
main (processo)
t (evento)
Init (esquema de inicialização)
e1 (evento)
com_e1 (operação)
en (evento)
com_en (operação)
Semântica de CSP-Z
(Mudança de estado capturada por Z)
P1 (S)
e1
P2 (S;com_e1)
e2
P3 (S;com_e1;com_e2)
Semântica de CSP-Z
(Refutações introduzidas por Z)
stop (refutada por Z)
P1 (S)
 pre com_e2
e1
P2 (S;com_e1)
e2
P3 (S;com_e1;com_e2)
Model-Checking CSP-Z

Z em CSP-Z é uma álgebra de processos como CSP

CSP-Z é por definição uma comp. paralela de CSP
e Z: PCSP-Z = PCSP [|I|] PZ, onde I é a interface de P

Model-checking em CSP é refinamento em CSP

Portanto, verificar se PCSP-Z satisfaz a propriedade
Pr significa perguntar a FDR se:
Pr
PCSP-Z
ou
Pr
PCSP [|I|] PZ
Traduzindo CSP-Z para CSPM
State: parâmetro em processos, P(State)
 Init: processo de início, Init=main(State0)
 com_c: função de tipo StateInStateOut
 pre com_c: função de tipo StateInBool
 Comunicações: compreensão de conjuntos,
envolvendo a pré-condição se necessário
 Tipos: . . .

Convertendo Z
State
Z(S) =
preCom_a1(S,In1?) & a1Z(com_a1 (S,In1?))
•
...
Init
...
...
•
preCom_an(S,Inn?) & anZ(com_an (S,Inn?))
com_a1
...
...
com_a
...
n
-- Definições das operações e pré-condições:
com_a1 (S, In1?) = ...
...
com_an (S, Inn?) = ...
preCom_a1(S,In1?) = ...
...
preCom_an(S,Inn?) = ...
Convertendo CSP-Z
spec P
main = ...
P=
let
main = ...
Z(S) =
preCom_a1(S,In1?) & a1Z(com_a1 (S,In1?))
•
State
...
Init
...
com_a
...
...
com_a
...
end_spec P
...
1
n
•
preCom_an(S,Inn?) & anZ(com_an (S,Inn?))
-- Definições
...
within
main [|{|a1, ..., an|}|] Z(Init)
Tradução do Relógio em CSPM
datatype SOUND = Cookoo
channel ticktack
channel bird: SOUND
Clock =
let
main = ticktackmain [] bird?msgmain
Z(Min) = preTickTack(Min) &
ticktackZ(com_ticktack(Min))
[] preBird(Min) &
bird!snd(com_bird(Min))com_bird(fst(com_bird(Min)))
-- Definições das operações e pré-condições
com_ticktack(Min) = Min + 1
com_bird(Min) = (0, Cookoo)
preTickTack(Min) = (Min < 60)
within
main [|{|ticktack, bird|}|] Z(0)
preBird(Min) = (Min == 60)
Algumas Observações
Registros tornam-se tuplas
 Funções, bags, relações tornam-se
conjuntos ou seqüências
 Uma ! em CSP frente a variável torna-se ?
 O uso de sub-tipos pode levar o sistema a
ter um comportamento diferente
