Código: | EIC0039 | Sigla: | MFES |
Áreas Científicas | |
---|---|
Classificação | Área Científica |
OFICIAL | Engenharia de Software |
Ativa? | Sim |
Página Web: | http://moodle.up.pt/ |
Unidade Responsável: | Departamento de Engenharia Informática |
Curso/CE Responsável: | Mestrado Integrado em Engenharia Informática e Computação |
Sigla | Nº de Estudantes | Plano de Estudos | Anos Curriculares | Créditos UCN | Créditos ECTS | Horas de Contacto | Horas Totais |
---|---|---|---|---|---|---|---|
MIEIC | 135 | Plano de estudos a partir de 2009/10 | 4 | - | 6 | 56 | 162 |
1-CONHECIMENTOS ÚTEIS Conhecimentos de engenharia de software (nomeadamente, processos de desenvolvimento e modelação de software) e conhecimentos de teoria de computação.
2-OBJETIVOS ESPECÍFICOS Desenvolver as capacidades de abstração de forma a descrever o que o sistema deve fazer e não a maneira de o fazer. Estar familiarizados com os métodos formais e forma como eles podem contribuir para aumentar a qualidade dos sistemas de software.
3-CONHECIMENTO PRÉVIO É útil frequência anterior em Engenharia de software, Teoria de computação e Conceção e análise de algoritmos.
4-DISTRIBUIÇÂO PERCENTUAL Componente científica = 75% Componente tecnológica = 25%
5-RESULTADO DA APRENDIZAGEM No final da unidade curricular os estudantes devem ser capazes de: - 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. - identificar os métodos formais existentes e saber quando devem ser aplicados e quais são mais adequados em cada caso.
No final da unidade curricular, os estudantes deverão ser capazes de especificar um sistema de software de forma declarativa, saber distinguir os vários métodos formais existentes e quando os aplicar e perceber a utilidade destas técnicas para a melhoria da qualidade dos sistemas de software.
1. Introdução
1.1 O que são métodos formais.
1.2 Importância e aplicabilidade dos métodos formais no desenvolvimento de software.
1.3 Modelos de ciclo de vida e processos de desenvolvimento de software incorporando métodos formais.
1.4 Especificação, refinamento, implementação, verificação e validação.
1.5 Classificação de métodos formais.
1.6 Modelos explícitos vs implícitos, executáveis vs não executáveis.
1.7 Técnicas de verificação formal.
2. "Alloy Constraint Analyzer", para modelação e análise semântica
2.1 Modelação declarativa.
2.2 Diferenças relativas a "model checking".
2.3 Comandos Alloy.
2.4 Funções; Predicados; Factos; Asserções e Verificações ("Checks").
2.5 Modelação estática vs dinâmica.
2.6 Simular a execução de uma operação.
2.7 Verificar propriedades "safety".
2.8 A ferramenta Alloy analyzer.
3. Lógica e "Model Checking"
3.1 Lógica proposicional, de predicados, temporal linear (LTL), temporal ramificada (CTL).
3.2 Representação de estados.
3.3 "Model Checking":
3.3.1 Propriedades: "Safety"; "Fairness"; "Liveness"; Universalidade; Inevitabilidade; Possibilidade; Ausência; Resposta; Precedência.
3.3.2 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. Provas Formais
4.1 Aplicação de lógica de Hoare à prova de correcção de algoritmos.
4.2 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.
4.3 Prova de correcção de programas.
4.4 A ferramenta Jape.
5. Especificação baseada em modelos (VDM)
5.1 As linguagens VDM-SL e VDM++.
5.2 Representação de dados com base em estruturas matemáticas (conjuntos, sequências e funções finitas).
5.3 Especificação com estado e sem estado.
5.4 Definição de tipos, valores e funções.
5.5 Definição de classes, variáveis de instância e operações.
5.6 Expressões e instruções.
5.7 Design-by-contract: definição de invariantes, pré-condições e pós-condições.
5.8 Descrição de algoritmos, especificações executáveis.
5.9 Análise de consistência da especificação: obrigações de prova e teste.
5.10 Ligação do VDM++ ao UML.
5.11 Geração de código a partir de uma especificação formal.
5.12 A ferramenta VDMTools.
As aulas teóricas serão usadas para exposição e estudo dos conteúdos programáticos, bem como, realização de exercícios práticos. As aulas práticas serão usadas para realização de exercícios, para contactar com diversas ferramentas e para a realização de trabalhos práticos.
Designação | Peso (%) |
---|---|
Exame | 35,00 |
Teste | 40,00 |
Trabalho laboratorial | 25,00 |
Total: | 100,00 |
Designação | Tempo (Horas) |
---|---|
Estudo autónomo | 60,00 |
Frequência das aulas | 52,00 |
Trabalho laboratorial | 50,00 |
Total: | 162,00 |
Nota mínima de 45% na classificação do trabalho prático. A presença nas aulas teórico-práticas é registada e obrigatória conforme legislação em vigor.
Avaliação distribuída com exame final, com as seguintes componentes:
(A) mini teste de Alloy, com consulta, duração de 1h, peso 40%, nota mínima de 45%.
(B) trabalho prático de VDM++, peso 25%, nota mínima de 45%.
(C) exame final com consulta, duração 1h30, peso 35%, nota mínima de 45%.
Classificação Final = (A)*40% + (B)*25% + (C)*35%
Notas: 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. Os alunos que não obtiverem aprovação no mini teste de Alloy poderão fazer um módulo de avaliação adicional no exame final de recurso da unidade curricular. São duas oportunidades de obter aprovação nesta componente: o mini teste e o exame de recurso. A avaliação da componente de Alloy só poderá ser melhorada no exame de recurso.
Mini teste de Alloy na aula teórica do dia 24 de outubro.
Trabalho prático de VDM++: entrega até às 23h do dia 12 de dezembro; defesa do trabalho prático durante as aulas práticas da semana de 15 a 19 de dezembro.
A defesa dos trabalhos práticos é obrigatória para TODOS os alunos.
Os trabalhos são obrigatórios para todos os alunos, mesmo para os alunos dispensados de frequência às aulas. Os alunos dispensados de frequência às aulas devem contactar o docente para sessões especiais de acompanhamento dos trabalhos. A defesa dos trabalhos práticos é obrigatória para TODOS os estudantes.
- A classificação do mini teste só poderá ser melhorada em exame de recurso.
- Os alunos que não obtiverem aprovação no mini teste poderão fazer um módulo adicional de 1h no exame final da época de recurso.
- As classificações obtidas no trabalho prático podem ser melhoradas na edição seguinte da disciplina
- A classificação do exame pode ser melhorada em exame de recurso.
Os alunos com frequência à disciplina do ano anterior terão que fazer exame de 2h30 (com a componente de Alloy e VDM). A classificação obtida no trabalho de VDM++ do ano anterior será usada como classificação do trabalho de VDM++ desta edição.