Upload
phila
View
40
Download
0
Embed Size (px)
DESCRIPTION
Métodos Formais. Desenvolvimento Formal de Software. Visão geral. Motivação Um Modelo para Desenvolvimento Formal de Software Estilos de Especificação Considerações Finais. Motivação. Crise de Software Na prática, o desenvolvimento é Ad hoc Não há um padrão para o processo - PowerPoint PPT Presentation
Citation preview
1
Métodos Formais
Desenvolvimento Formal de Software
2
Visão geral
Motivação
Um Modelo para Desenvolvimento Formal de Software
Estilos de Especificação
Considerações Finais
3
Motivação Crise de Software
– Na prática, o desenvolvimento é Ad hoc– Não há um padrão para o processo– São necessários: teorias, técnicas, métodos,
ferramentas,... Profissionais incapazes de controlar
– Custo– Tempo (duração do processo)– Qualidade do produto desenvolvido
Manutenção: 70-80% do esforço dedicado
4
Modelo de Desenvolvimento - Na Prática
Especificação
Projeto
Implementação
Manutenção Especificação: informal Projeto: informal ou estruturado, semi-formal
– JSD, Yourdon, OMT, BON, UML, ... Implementação: sem garantia de realizar o projeto
Verificação e validação são ignorados!
5
O que é um método formal emengenharia de software?
Método de desenvolvimento de software através do qual se pode definir
precisamente um sistema e
desenvolver implementações garantidamente corretas em relação a esta definição.
6
Características de Métodos Formais
Delineamento preciso do processo de desenvolvimento
Baseado em linguagens de especificação e programação com semântica bem definida
Processo de desenvolvimento incremental, que possibilita expressão em vários níveis de abstração
Processo de desenvolvimento usualmente baseado em regras de transformação
7
Por que métodos formais?
Lançador Ariane – Explodiu 40s após lançamento em 1996
Therac-25 – Entre 1985 e 1987, pelo menos 6
acidentes causaram mortes e ferimentos graves durante terapia de radiação
Dezenas de outros acidentes Perda de controle do desenvolvimento
e evolução de sistemas complexos
8
Alguns resultados práticos
CICS da IBM Unidade de ponto flutuante (transputers) Protocolos de comunicação Aplicações espaciais e de aviação Sistemas de controle de trens Equipamentos médicos Arquiteturas de hardware Aplicações bancárias Aplicações meteorológicas
9
Especificação Formal Descrição Matemática Precisa
– Não ambígua – Permite verificar propriedades (ex.
consistência) – Usualmente abstratas e concisas
É a base para– Documento contratual – Documentação do produto – Referência para etapas seguintes
E aspectos como completude, corretude? Especificação é apenas uma etapa!
10
Grau de formalismo no desenvolvimento
Informal ou Ad hoc – Pouca (ou nenhuma) regra pré-definida
Sistemático – Conjunto de regras pré-estabelecidas
Rigoroso – Regras de transformação estritas– Partes críticas desenvolvidas formalmente
Formal – Verificação formal de todo o processo
11
Um Modelo para Desenvolvimento Formal
Modelo Contratual– Cada etapa do desenvolvimento é
caracterizada por um contrato entre um cliente e um fornecedor.
– Por exemplo, na fase de análise de requisitos, o cliente é o usuário final do sistema e o fornecedor é o analista.
– Validação e verificação são realizadas
12