View
137
Download
5
Category
Preview:
Citation preview
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período Slide 1
Métodos Formais
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período Slide 2
Métodos Formais
São técnicas baseadas em formalismos matemáticos para a especificação, desenvolvimento e verificação dos sistemas de softwares e hardwares.
Na Ciência da Computação...
... o termo método formal foi restrito para o uso de notação formal para representar modelos de sistemas durante o processo de desenvolvimento.
... É difícil formalizar domínios que possuem muitos casos especiais ou contém muito conhecimento subentendido ou sujeito a mudanças.
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período Slide 3
Métodos Formais
Não se tornaram as principais técnicas de desenvolvimento de software• Outras técnicas foram utilizadas que resultou em melhorias na
qualidade do software. • O time-to-market é preferível.• O escopo de métodos formais é limitado.• A formalização é bem sucedida em domínios restritos ou
organizados.• No desenvolvimento de software não se pode validar
resultados apenas provando teoremas.
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período Slide 4
Benefícios de Métodos Formais
Usados para reduzir o número de erros do sistema. Reduz tempo de desenvolvimento. Proporciona melhor documentação. Melhora a comunicação (entre equipe com o usuário). Facilita manutenção. Ajuda a organizar as atividades durante o ciclo de
vida.
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período Slide 5
Métodos Formais
Especificação Formal. Análise e prova da especificação. Verificação do programa.
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período Slide 6
Especificação Formal
É uma especificação expressa em uma determinada linguagem cujo vocabulário, sintaxe e semântica são formalmente definidos e rígidos.
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período Slide 7
Especificação Formal
Especificação vs. Implementação– O quê? vs. Como?
Especificações formais vs. especificações informais
– Formais: A notação utilizada possui uma sintaxe e uma semântica totalmente precisa
– Informal: Escritas em linguagem natural
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período Slide 8
Especificação Formal
Uma especificação formal provê: Uma notação (domínio sintático); Um universo de objetos (domínio semântico); Regra precisa que define que objetos satisfazem cada
especificação.
Uma especificação é uma sentença escrita em termos de elementos do domínio sintático.
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período Slide 9
Especificação Formal
Uma linguagem de especificação é uma tripla <Sin, Sem, Sat>:
Sin e Sem são conjuntos. Sat é uma relação entre Sin e Sem. Se Sat(sin, sem), então sin é uma especificação de sem, e
sem é um especificando de sin.
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período Slide 10
Domínio Sintático
Definido em termos de: um conjunto de símbolos (por exemplo, constantes,
variáveis e conectores lógicos). Um conjunto de regras gramaticais para combinar esses
símbolos.
Necessidade de sentenças bem formadas. O domínio sintático não se restringe a um
formato textual. Pode-se usar elementos gráficos.
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período Slide 11
Domínio Semântico
As linguagens de especificação diferem na escolha do domínio semântico.
Exemplos: Linguagens de especificação de tipos abstratos de dados. Linguagens de especificação de sistemas distribuídos e
concorrentes. Linguagens de programação.
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período Slide 12
Propriedades de uma Especificação
Não ambigüidade: Cada especificação é mapeada em exatamente um
especificando.
Consistente: Deve ter uma interpretação semântica significativa.
Completa: A coleção de propriedades especificadas deve ser suficiente
para estabelecer compatibilidade com especificações de mais alto nível.
Mínima
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período Slide 13
Especificação no Processo de Software
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período Slide 14
Custo do Processo de Software
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período Slide 15
Técnicas de Especificação
Algébrica– O sistema é descrito em termos de operações e
relacionamentos entre elas.
Baseada em modelo– Um modelo do sistema é construído usando construções
matemáticas tais como conjuntos e seqüências e as operações são definidas em termos de como elas alteram o estado do sistema.
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período Slide 16
Linguagens de Especificação Formal
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período Slide 17
Estrutura de uma Especificação Algébrica
sort < nome >imports < LISTA DE NOMES DA ESPECIFICAÇÃO>
Descrição informal do sort e de suas operações
Assinaturas de operação, que estabelecem os nomes e os tipos de parâmetros às operações definidas sobre o sort
Axiomas que definem as operções sobre o sort
< Nome da Especificação>
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período Slide 18
Componentes da Especificação
Introdução– Define o sort (o nome do tipo) e declara outras
especificações que são usadas
Descrição– Descreve informalmente as operações
Assinatura– Define a sintaxe e seus parâmetros
Axioma– Define a semântica das operações
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período Slide 19
Especificação algébrica sistemática
Estruturação da especificação Nomeação da especificação Seleção da operação Especificação informal de operação Definição da sintaxe Definição dos axiomas
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período Slide 20
Especificação de uma Lista
sort Listaimports INTEIRO
Define uma lista em que elementos são adicionados ao seu final e removidos de seu início. As operações são CREATE, que busca uma lista vazia; CONS, que cria uma nova lista com a adição de um membro;Length, que avalia o tamanho da lista; HEAD, que avalia o primeiro elemento da lista; eTAIL, que cria uma lista removendo o HEAD de sua lista de entrada. UNDEFINED representa um valor indefinido do tipo Elem.
Create → ListCons(List,Elem) → ListHead(List) → ElemLength(List) → InteiroTail(List) → List
LISTA ( Elem )
Create → ListCons(List,Elem) → ListHead(List) → ElemLength(List) → InteiroTail(List) → List
Head(Create) = Undefined exception (empty List)Head(Cons(L,v)) = if L=Create then v else Head(L) Length(Create) = 0Length(Cons(L,v)) = Length(L) + 1Tail(Create) = CreateTail(Cons(L,v)) = if L=Create then Create else Cons(Tail(L),v)
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período Slide 21
Especificações recursivas Operações são frequentemente especificadas
recursivamente Tail (Cons (L, v)) = if L = Create then Create
else Cons (Tail (L), v)• Cons ([5, 7], 9) = [5, 7, 9]• Tail ([5, 7, 9]) =
• Tail (Cons ( [5, 7], 9)) = • Cons (Tail ([5, 7]), 9) = • Cons (Tail (Cons ([5], 7)), 9) = • Cons (Cons (Tail ([5]), 7), 9) = • Cons (Cons (Tail (Cons ([], 5)), 7), 9) = • Cons (Cons ([Create], 7), 9) = • Cons ([7], 9) = [7, 9]
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período Slide 22
Especificações recursivas(*Funcao adiciona um item na lista, ListDadoTempo*)
fun adic(item,[]) = [item]
| adic(item,item1::lista) =
[item]^^([item1]^^lista);
(*Funcao adiciona um item na lista, ListDadoTempoS*)
fun adic1((item,tsr,s),[]) = [(item,agora(),s)]
| adic1((item,tsr,s),(item1,tsr1,sn)::ListdadotempoS) =
[(item,agora(),s)]^^([(item1,tsr1,sn)]^^ListdadotempoS);
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período Slide 23
Especificações recursivas(*Funcao retira um item da lista, ListDadoTempoS*)
fun retira([]) = 0 |
retira((S1,item1,tsr)::lis) =
item1;
fun retira1([]) = 0 |
retira1((item1,tsr,s)::lis) =
Tsr;
©Ian Sommerville - Software Engineering – TraduçãoProf Pedro Fernandes - Métodos Formais, 6o Período Slide 24
Especificações recursivas(*Funcao que define a capacidade maxima de
armazenamento do sensor*)
(*A lista eh invertida (rev), depois eh retirado o 1o elemento dela (tl) e depois ela eh invertida mais uma vez pra voltar a ordem original*)
fun memoria(list:ListDadoTempoS):ListDadoTempoS =
if length(list) > 8
then rev(tl(rev(list)))
else list;
Recommended