Upload
conlan
View
31
Download
0
Embed Size (px)
DESCRIPTION
Estilos de Especificação. Orientados a Propriedades (Algébricas) Baseados em Modelos Concorrente. Especificação Algébrica. Uma Especificação consiste de Um conjunto de nomes de tipos (sorts) Um conjunto de funções Um conjunto de axiomas (semântica). Um Exemplo Clássico: pilhas. - PowerPoint PPT Presentation
Citation preview
1
Estilos de Especificação
Orientados a Propriedades (Algébricas)
Baseados em Modelos
Concorrente
2
Especificação Algébrica
Uma Especificação consiste de
– Um conjunto de nomes de tipos (sorts)
– Um conjunto de funções
– Um conjunto de axiomas (semântica)
3
Um Exemplo Clássico: pilhas Tipo: pilha-int Funções
vazia: -> pilha-int
push: int pilha-int -> pilha-int
pop: pilha-int -> pilha-int
top: pilha-int -> int
e_vazia: pilha-int -> bool
Axiomaspop (push (i, p)) = p
top (push (i, p)) = i
e_vazia (p) = (p = vazia)
4
Métodos Baseados em Modelos
Componentes de uma Especificação
Um Modelo matemático é usado para descrever o estado do sistema.
5
Um Modelo Matemático para Pilhas
var
pilha, pilha' : seq[Int]
operações (procedimentos, métodos)
vazia = (pilha' = [])
push(i? : Int) = pilha'=[i?]^pilha
pop() = (pilha []) => pilha'= tail pilha
top(i! : Int) = (pilha []) => i! = head pilha
e_vazia (b! : Bool) = b! <=> (pilha = [])
6
Especificação de sistemas concorrentes
Modelos - Exemplos – CSP (Communicating Sequential Processes)– CCS (Calculus of Communicating Systems)
Um sistema é uma rede de processos independentes e comunicantes
Rigor matemático permite especificações, provas e transformações
Algumas diferenças: – notação
– conceito de equivalência
7
Um Exemplo Simples Relógio de parede com cuco
– Modelado por dois componentes:• Contador de 1 a 60• Cuco: aparece a cada 60 minutos
– A interação entre esses componentes se dá a cada 60 minutos
Cookoo
0102030405060
8
Um Exemplo Simples
Contador(min) = tick Contador(min + 1)
Contador(60) = sincroniza Contador(0)
Passaro = sincroniza cuco Passaro
Relogio = Contador(0) || Passaro {sincroniza}
9
Especificação de Sistemas Concorrentes
Tanto CCS como CSP influenciaram
trabalhos futuros. Exemplos:
– CSP: occam, trasputer
– LOTOS foi influenciada por CCS + ACT
ONE
10
Uso Prático de Métodos Formais
Escolha a notação apropriada Estime os custos/benefícios Não abandone métodos tradicionais (use
métodos semi-formais em conjunto com métodos formais). Ex. UML + Z (OCL)
Documente Não esqueça as medidas usuais de
qualidade Teste Reuse
11
Considerações Finais
Um aspecto unificador de estilos: evitar tradução entre linguagens sempre que possível.– Cálculo de Refinamentos [Morgan]– Extendend ML [Sannella]
Na prática, nem sempre é possível usar uma única liguagem. Mas deve haver uma unificação semântica.– Exemplo: De CSP-Z para Java (CTJ)
12
Considerações Finais
Integração de formalismos– Z + CSP – Z + Timed CSP – Object-Z, MooZ – UML + Z (OCL)
Aplicações práticas podem ser citadas– CICS (IBM) – TRANSPUTER (INMOS)– Protocolos – Sistemas de aviação, ...
13
Considerações Finais Mas podemos fazer muito mais
– Padrões: Z, LOTOS, etc. – Literatura – Formação de pessoal– Ambiente de apoio
Formalização de práticas informais