Métodos Formais em Engenharia de Software

Mestrado Integrado em Engenharia Informática - MFES 2018/2019

Tópicos

Avisos

02 Out - CSI: preparação para as aulas: ver tinynew.gif sumários previstos e seguir as respectivas indicações nos apontamentos fornecidos na bibliografia. (Em CSI segue-se o método 'Flipped Classroom')

15 Set - Início das aulas: 20-Set, 9h00, sala E7 1.10.

Education » MFES » WebHome » CSI

UC2 - Cálculo de Sistemas de Informação

E-Learning


Docente / Horário

Docente Foto Horário Sala
José Nuno Oliveira jno 5a-feira, 14h-17h Sala E7 1.10

NB: poderá haver trocas de horário entre CSI e EM de acordo com necessidades de serviço dos docentes das duas disciplinas.

Alunos

Afonso Rafael Carvalho Sousa A74196 MiEI
Alexandre Miguel Costa Dias A78425 MiEI
Armando João Isaias Ferreira dos Santos A77628 MiEI
Artur Queiroz PG38014 MMC
Diogo Manuel Macedo e Silva A79021 MiEI
Francisco Fernando Vilela Araújo A79821 MiEI
Fábio Rafael Pereira Araújo A78508 MiEI
Gerson Benjamim Hungulu PG35957 MMC
Gonçalo Medeiros São Pedro Raposo A77211 MiEI
Gonçalo Nuno Esteves Duarte A77508 MiEI
Joana Fernandes Cunha PG38929 MEI
Jorge Fernando Alves da Cruz A78895 MiEI
José Carlos do Vale e Sousa A74678 MiEI
João Manuel da Silva Gomes Fernandes PG38930 MEI
Nelson Loureiro PG37020 MMC
Patrícia Filipa Bouça Barreira A79007 MiEI
Pedro Faria Durães da Silva A78434 MiEI
Pedro Henrique Moreira Gomes Fernandes A77377 MiEI
Pedro Miguel Silva´ PG38935 MEI
Ricardo Guerra Leal A75411 MiEI
Tiago André Araújo Monteiro A78961 MiEI

Programa resumido

Introdução aos métodos formais e seu papel na programação. Verificação e cálculo de soluções informáticas. Problemas e sistemas de informação para os resolver. Modelos e seu papel na concepção de soluções. Importância da abstracção na captação de requisitos. Limites da tipagem estática. Papel das relações binárias na modelação formal. Bases de dados seguindo o modelo 'key-value pair'. Taxonomia e álgebra das relações binárias. O lema "everything is a relation". 'Model checking' usando a ferramenta Alloy. Demonstração de corrrecção usando álgebra relacional. Noção formal de contrato. Pré-condições mais fracas. Lógica de Hoare em formato relacional.

Regime de avaliação

  • Duas provas de avaliação (mini-teste + teste) e exame de recurso.
  • Avaliação contínua com base em problemas dados nas aulas TP.
  • As provas escritas são de consulta de material impresso, apenas.
  • O mini-teste é eliminatório de matéria para o teste e vale 60%.

Bibliografia

  • J.N. Oliveira. Program Design by Calculation. Departamento de Informática, Universidade do Minho. Os capítulos deste livro (em preparação) essenciais para esta disciplina no corrente ano lectivo são o quinto ( 1M) tinynew.gif, o sexto ( ___K) e o sétimo ( ___K).

Bibliografia adicional

  • C.B. Jones. Systematic Software Development Using VDM. Series in Computer Science. Prentice-Hall International, 1986 (first edition). (345 pages)

Ferramentas

Exemplos / bibliotecas Alloy

  • Módulo Alloy: RelCalc.als - Cálculo relacional básico em Alloy.

-- JoseNunoOliveira - 15 Sep 2018

r13 - 18 Oct 2018 - 12:09:47 - JoseNunoOliveira
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM