Saltar para:
Logótipo
This page in english Ajuda Autenticar-se
Projecto da Casa da U. Porto
Você está em: Início > EIC0039
Autenticação




Mapa das Instalações
Edifício A (Administração) Edifício B (Aulas) - Bloco I Edifício B (Aulas) - Bloco II Edifício B (Aulas) - Bloco III Edifício B (Aulas) - Bloco IV Edifício C (Biblioteca) Edifício D (CICA) Edifício E (Química) Edifício F (Minas e Metalurgia) Edifício F (Minas e Metalurgia) Edifício G (Civil) Edifício H (Civil) Edifício I (Electrotecnia) Edifício J (Electrotecnia) Edifício K (Pavilhão FCNAUP) Edifício L (Mecânica) Edifício M (Mecânica) Edifício N (Garagem) Edifício O (Cafetaria) Edifício P (Cantina) Edifício Q (Central de Gases) Edifício R (Laboratório de Engenharia do Ambiente) Edifício S (INESC) Edifício T (Torre do INEGI) Edifício U (Nave do INEGI) Edifício X (Associação de Estudantes)

Métodos Formais em Engenharia de Software

Código: EIC0039     Sigla: MFES

Áreas Científicas
Classificação Área Científica
OFICIAL Engenharia de Software

Ocorrência: 2008/2009 - 2S

Ativa? Sim
Página Web: http://paginas.fe.up.pt/~apaiva/teach/0809/MFES.htm
Unidade Responsável: Departamento de Engenharia Informática
Curso/CE Responsável: Mestrado Integrado em Engenharia Informática e Computação

Ciclos de Estudo/Cursos

Sigla Nº de Estudantes Plano de Estudos Anos Curriculares Créditos UCN Créditos ECTS Horas de Contacto Horas Totais
MIEEC 5 Plano de estudos oficial a partir de 2006/07 4 - 5 -
Plano de estudos oficial a partir de 2007/08 4 - 5 -
MIEIC 132 Plano de estudos oficial a partir de 2006/07 4 - 5 -

Docência - Horas

Teóricas: 2,00
Teórico-Práticas: 2,00
Tipo Docente Turmas Horas
Teóricas Totais 1 2,00
Ana Cristina Ramada Paiva 2,00
Teórico-Práticas Totais 5 10,00
Hugo José Sereno Lopes Ferreira 4,00
Ana Cristina Ramada Paiva 6,00

Língua de trabalho

Português

Objetivos

Saber aplicar métodos formais de especificação (baseado em modelos; baseado em propriedades; baseado em comportamento) e verificação ("Model-checking", provas formais e teste) no desenvolvimento de sistemas de software.
Conhecer os métodos formais existentes e saber quando devem ser aplicados e quais são mais adequados em cada caso.

Programa

1. Introdução (semanas 1 e 2)
O que são métodos formais.
Importância e aplicabilidade dos métodos formais no desenvolvimento de software.
Modelos de ciclo de vida e processos de desenvolvimento de software incorporando métodos formais.
Especificação, refinamento, implementação, verificação e validação.
Classificação de métodos formais.
Modelos explícitos vs implícitos, executáveis vs não executáveis.
Técnicas de verificação formal.

2. Especificação baseada em modelos (semanas 2-4)
As linguagens VDM-SL e VDM++.
Representação de dados com base em estruturas matemáticas (conjuntos, sequências e funções finitas).
Especificação com estado e sem estado.
Definição de tipos, valores e funções.
Definição de classes, variáveis de instância e operações.
Expressões e instruções.
Design-by-contract: definição de invariantes, pré-condições e pós-condições.
Descrição de algoritmos, especificações executáveis.
Análise de consistência da especificação: obrigações de prova e teste.
Ligação do VDM++ ao UML.
Geração de código a partir de uma especificação formal.
A ferramenta VDMTools.

3. Lógica e "Model Checking" (semanas 5 e 6)
Lógica proposicional, de predicados, temporal linear (LTL), temporal ramificada (CTL).
Representação de estados.
"Model Checking":
- Propriedades: "Safety"; "Fairness"; "Liveness"; Universalidade; Inevitabilidade; Possibilidade; Ausência; Resposta; Precedência.
- Problema de Explosão de estados (técnicas existentes para minorar este problema): Estado Simbólico; "Bounds"; "On-the-fly"; "Partial Order Reduction (POR)"; Abstracção.

4. "Alloy Constraint Analyzer", para modelação e análise semântica (semanas 7-8)
Modelação declarativa.
Diferenças relativas a "model checking".
Comandos Alloy.
Funções; Predicados; Factos; Asserções e Verificações ("Checks").
Modelação estática vs dinâmica.
Simular a execução de uma operação.
Verificar propriedades "safety".
A ferramenta Alloy analyzer.

6. Provas Formais (semana 9-12)
Aplicação de lógica de Hoare à prova de correcção de algoritmos.
Linguagem de especificação Gallina: tipos e expressões; proposições e provas; tipos de dados indutivos; tácticas de prova e automação; predicados indutivos.
Prova de correcção de programas.
As ferramenta Coq, Caduceus, JAPE e Krakatoa.

Bibliografia Obrigatória

B. Bérard; M. Bidoit; A. Finkel; F. Laroussinie; A. Petit; L. Petrucci; Ph. Schnoebelen; P. McKenzie; Systems and Software Verification - Model Checking Techniques and Tools, Springer, 2001. ISBN: 3-540-41523-8
Fitzgerald, John; Validated designs for object-oriented systems. ISBN: 1-85233-881-4
Bertot, Yves; Interactive theorem proving and program development. ISBN: 3-540-20854-2

Bibliografia Complementar

Clarke, Jr., Edmund M.; Model checking. ISBN: 0-262-03270-8
Peled, Doron A.; Software reliability methods. ISBN: 0-387-95106-7
Fitzgerald, John; Modelling systems. ISBN: 0-521-62605-6
Alagar, V. S.; Specification of software systems. ISBN: 0-387-98430-5

Métodos de ensino e atividades de aprendizagem

As aulas teóricas serão usadas para exposição e estudo dos conteúdos programáticos.
As aulas práticas serão usadas para realização de exercícios, para contactar com a diversas ferramentas e para a realização de trabalhos práticos.

Software

VDMTools
Coq
Alloy Analyzer
Krakatoa
Caduceus
JAPE

Palavras Chave

Ciências Tecnológicas > Engenharia > Engenharia de computadores
Ciências Tecnológicas > Tecnologia > Tecnologia de computadores > Tecnologia de software

Tipo de avaliação

Avaliação distribuída com exame final

Componentes de Avaliação

Descrição Tipo Tempo (Horas) Peso (%) Data Conclusão
Participação presencial (estimativa) Participação presencial 52,00
Exames Exame 12,00 2009-07-31
Trabalhos práticos Defesa pública de dissertação, de relatório de projeto ou estágio, ou de tese 50,00 2009-05-29
Total: - 0,00

Componentes de Ocupação

Descrição Tipo Tempo (Horas) Data Conclusão
Estudo individual Estudo autónomo 20 2009-07-31
Total: 20,00

Obtenção de frequência

Nota mínima de 40% na classificação de frequência.

Fórmula de cálculo da classificação final

Avaliação distribuída com exame final, com as seguintes componentes:
a) exame final com consulta, duração 2h30, peso 40%, nota mínima de 40%;
b) classificação de frequência, 60%:
- trabalho prático, peso 30%, nota mínima de 40%;
- trabalho prático, peso 30%, nota mínima de 40%.

Nota: em todo o caso, a classificação final não pode exceder em mais de 3 valores a classificação do exame arredondada para o inteiro mais próximo.

Avaliação especial (TE, DA, ...)

Os trabalhos são obrigatórios para todos os alunos, mesmo para os alunos dispensados de frequência às aulas.

Melhoria de classificação

A classificação do exame pode ser melhorada em exame de recurso.
As classificações obtidas nos trabalhos práticos podem ser melhoradas na edição seguinte da disciplina.
Recomendar Página Voltar ao Topo
Copyright 1996-2019 © Faculdade de Engenharia da Universidade do Porto  I Termos e Condições  I Acessibilidade  I Índice A-Z  I Livro de Visitas
Página gerada em: 2019-04-22 às 22:01:48 | Política de Utilização Aceitável | Política de Proteção de Dados Pessoais