CIn.ufpe.br

CSP-ZDisciplina: Especificação de Sistemas Distribuídos

Mestrado em Ciências da Computação

Aleciano Jr. aflj@cin.ufpe.br

Leonilson Barbosalab5@cin.ufpe.br

Renata Bragarba6@cin.ufpe.br

CIn.ufpe.br

Agenda• Notação Z

– Características– Tipos– Esquemas– Predicados– Exemplos

• CSP-Z– O que é?– Semântica– Visão de bloqueio– Model-checking de CSP-Z

• Considerações Finais

CIn.ufpe.br

Z - O que é?

• Linguagem de especificação formal usada para descrever e modelar sistemas computacionais.

• Especificações formais utilizam notação matemática para descrever as propriedades de um sistema de forma precisa.

CIn.ufpe.br

Z - Características

• Usa a notação da lógica de predicados.

• Utiliza uma variedade de estruturas matemáticas como conjuntos, relações e funções.

• Permite que a especificação possa ser decomposta em pequenos pedaços chamados esquemas.

CIn.ufpe.br

Z - Características

• Esquemas descrevem aspectos estáticos e dinâmicos

• Aspectos estáticos:– Estado que um sistema ocupa– Invariantes de relacionamento que são mantidas

• Aspectos dinâmicos:– Operações possíveis– Relacionamento entre entradas e saídas– Mudanças de estado que acontecem

• Esquemas podem ser combinados e usados em outros sistemas

CIn.ufpe.br

Z – Tipos

• Fortemente Tipada

• Tipos são interpretados como conjuntos

• Tipos podem ser simples ou compostos

CIn.ufpe.br

Z – Tipos

• Tipos podem ser simples ou compostos

• Tipos Simples podem ser:– Primitivos– Básicos

• Tipos Compostos podem ser:– Conjuntos– Produtos cartesianos– Esquemas

• Tipos são interpretados como conjuntos, logo operações como = e pertence () são definidas para todos os tipos

CIn.ufpe.br

Z – Esquemas

• Variáveis – São associadas a um tipo através de declarações.

• Expressões Axiomáticas– Introduz uma ou mais variáveis globais, e

opcionalmente constraints sobre seus valores.

CIn.ufpe.br

Z – Predicados

• Expressões booleanas

• Podem ser definidos isoladamente

• Sobre variáveis pré-definidas

CIn.ufpe.br

Exemplo

CIn.ufpe.br

Z – Exemplo

CIn.ufpe.br

Z – Exemplo

CIn.ufpe.br

Z – Exemplo

CIn.ufpe.br

Z – Exemplo

CIn.ufpe.br

CSP-Z – O que é?

• A linguagem CSP-Z é uma integração semântica da CSP e Z, de modo a que CSP manipula os aspectos simultâneos de um sistema, e Z foca na parte de estruturas de dados.

CIn.ufpe.br

CSP-Z – O que é?

Definições

1. A linguagem CSP-Z é uma extensão conservadora de CSP e Z.

2. Aspectos semânticos de CSP e Z são preservados.3. Aspectos sintáticos e semânticos de CSP são preservados.4. Interpretações de Z ligeiramente diferentes.

CIn.ufpe.br

CSP-Z – O que é?

Motivações

• 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”

CIn.ufpe.br

CSP-Z – Motivações

Integração formal entre CSP e Z

1. Captura tanto aspectos concorrentes quanto de estruturas de dados de um sistema.

2. É uma extensão conservativa de CSP e Z, com diferenças mínimas em ambas.

3. O refinamento de CSP-Z pode ser obtido pelo de CSP ou o de Z com restrições.

CIn.ufpe.br

CSP-Z – Semântica

Breve explicação da Semântica de CSP

• O modelo de semântica padrão de CSP é o modelo de falhas na Divergências.

• A linguagem CSP-Z é uma integração semântica de CSP e Z, em que uma Falhas/Divergência da o significado a Z.

• Uma especificação CSP-Z é definida como a combinação paralela do CSP e as partes Z através da interface, de tal modo que se um canal.

CIn.ufpe.br

CSP-Z – Semântica

Visão de bloqueio em CSP-Z

Em seguida, o pré-requisito de um esquema com_c é dada por

CIn.ufpe.br

CSP-Z – Semântica

Exemplo

CIn.ufpe.br

CSP-Z – Exemplo

Veja tr ser um vestígio de uma especificação CSP-Z. Assim, após a ocorrência de tr o estado do sistema é dada por:

Para um trace vazio

Onde é o operador de

concatenação e e o esquema Z a composição do operador

CIn.ufpe.br

CSP-Z – Exemplo

Por outro lado, se a guarda de uma operação Z é falsaEm seguida, o processo comporta-se como o processo de STOP

CIn.ufpe.br

CSP-Z

• Como verificar o comportamento das especificações CSP-Z e também as suas propriedades?

CIn.ufpe.br

CSP-Z – Model-checking

• Verificar automaticamente que

• Pode ser feito via refinamento no CSP

• Refinamento da parte CSP leva ao refinamento da especificação CSP-Z *

• Estender model-checking de CSP no FDR para o CSP-Z

CIn.ufpe.br

CSP-Z – Model-checking

• Como caracterizar a parte de Z em CSP?

• Como será o comportamento do CSP baseado nesses estados de Z?

• Como combinar e sincronizar as duas partes?

• Exemplo com um buffer finito.

CIn.ufpe.br

CSP-Z – Model-checking

CIn.ufpe.br

CSP-Z – Model-checking

• Forma comum de representar um estado em CSP é por meio da parametrização:

Buffer(State) = in?x -> Buffer(State')

• Para representar o estado de espaços em Z usa-se um conjunto de tuplas:

• Para o exemplo do Buffer, se torna:State = {s | s <- FSeq(T, n) }

• E o estado inicial:Init = { s'| s' <- State, s'== < > }

CIn.ufpe.br

CSP-Z – Model-checking

• Restringindo o comportamento de CSP como função do espaço de estados:

s != <> & out!y -> Buffer(State')

>> Tomando o exemplo do canal out

• As partes de Z se tornam processos

CIn.ufpe.br

CSP-Z – Model-checkingcom(s, In.t) = {s' | s'<-State, s'==s^<t> }

com(s, Out.t) = {s' | s'<-State, s!=<>, t==head(s), s'==tail(s) }

• Como dito antes, CSP e Z se combinam através de uma composição paralela, então define-se a Interface:

Channels = {|in,out|}lChannels = {}Interface = union(Channels, lChannels)

CIn.ufpe.br

CSP-Z – Model-checking

• Então, a parte de Z como um processo, sem a inicialização, fica:

Z(State) = ( [] (States,Comm) <-{ (com(State, c), c) |

c<-Interface } @ States != {} &|~| State': States @ Comm -> Z(State') ) []

terminate -> SKIP

• Então, a parte de Z incluindo a inicialização, fica:

Z_CSP =let

Z(state) = ( como definido acima ) within |~| iState: Init @ Z(iState)

CIn.ufpe.br

CSP-Z – Model-checking

• Combinando a parte de Z (em CSP) e a própria parte de CSP, finalmente, temos:...within (main [|Interface|] Z_CSP ) \lChannels

• A composição paralela por meio dos eventos em Interface une as partes de Z e CSP.

• O hidding é necessário pois em CSP não existe forma de modularizar da mesma forma que com especificações CSP-Z.

CIn.ufpe.br

CSP-Z – Model-checking

P = let-- The InterfaceChannels = {|...|}lChannels = {|...|}Interface = union(Channels, lChannels)-- The CSP Partmain = ...-- The Z PartState = {...}Init = {...}com(sTuple, Comm) = {...}...Z_CSP = ...within (main [|Interface|] Z_CSP)\lChannels

CIn.ufpe.br

CSP-Z – Model-checking

• Executando no ProBE

• Ferramenta de conversão de CSP-Z para CSP-M– Autores: Adalberto Farias, Alexandre Mota e Augusto Sampaio 

(2001)

– Desenvolvida na linguagem Java

CIn.ufpe.br

Considerações Finais

• A notação Z, junto com a álgebra de processos CSP, forma o CSP-Z, um tipo de especificação que une o tratamento de dados de Z com o comportamento de processos representado por CSP.

• No entanto, geralmente converte-se a parte de Z para CSP-M (linguagem do FDR).

• Existem outras notações semelhantes como o CSP-OZ e Circus.

CIn.ufpe.br

BOA TARDE!