Métodos Formais em Engenharia de Software

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

Tópicos

Avisos

16 Jan - CSI: tinynew.gif o teste de CSI de amanhã decorrerá na sala 0.05 do DI.

15 Jan - EM: as notas do segundo teste foram lançadas no blackboard da disciplina. tinynew.gif

11 Jan - CSI: as notas do mini-teste foram lançadas na página de CSI.

9 Jan - EM: o teste de EM decorrerá na sala 0.05 do DI.

30 Dec - EM: as notas do TP1 e do primeiro mini-teste foram lançadas no blackboard da disciplina.

21 Dec - EM: foi lançado o enunciado do TP2 sobre Alloy na página EM. A data limite da entrega é 20-Jan.

13 Dez - O segundo teste de EM decorrerá no dia 10-Jan às 9h00 (sala a indicar). O segundo teste de CSI decorrerá no dia 17-Jan (sala e hora a confirmar).

8 Dez - Lista recente e actualizada de empresas que usam métodos formais na indústria.

28 Nov - CSI: haverá hoje uma aula de dúvidas às 16h00, na sala 1.16.

24 Nov - CSI: já está disponível o formulário na página de CSI, bem como algumas FAQs.

24 Nov - CSI: o mini-teste decorrerá às 14h00 de 29-Nov, na sala das aulas. Os alunos podem consultar (apenas) informação escrita ou impressa.

14 Nov - EM: o primeiro teste decorrerá às 9h00 na sala das aulas. Podem usar os portáteis para testar execuções no NuSMV.

8 Nov - CSI: em casa, completar os invariantes I3 e I4 do modelo Alloy do problema Plano de Estudos do MEI saído da aula de hoje material pedagógico na página CSI.

5 Nov - CSI: há novo material pedagógico na página CSI.

25 Out - EM: foi lançado o enunciado do TP1 sobre NuSMV na página EM. A data limite da entrega é 11-Nov.

21 Out - CSI: ver exemplos Alloy das aulas na página CSI.

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 Gomes da 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), o sexto ( 101K) e o sétimo ( 433K) tinynew.gif.

Bibliografia adicional

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

Ferramentas

Material

  • Formulário CSI: ( 137K) tinynew.gif - Leis do cálculo relacional básico.

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

  • Módulo Alloy: kerimg.als - o que é o núcleo (kernel) e a imagem (image) de uma relação? Experimentem e observem variando a cláusula run.

  • Módulo Alloy: prod.als - produtos cartesianos em Alloy.

  • Biblioteca Haskell: RelCalc.hs ( nova versão com pragma que faltava, pf verificar se já corre) - Cálculo relacional básico em Haskell (precisa da biblioteca Cp).

  • Script para converter instâncias geradas pelo Alloy p ara Haskell:alloy.sed ( com gralha corrigida) - em Alloy, visualizar instância em modo Txt e copiar para ficheiro, eg. i.txt; de seguida fazer, numa shell, sed -f alloy.sed i.txt

Enunciados:

  • Enunciado do mini-teste de 29 de Novembro (com proposta de resolução).

Casos de estudo

  • Liga de futebol - modelo em Alloy: liga.als

  • Plano de estudos do MEI - em curso, enunciado: (PDF); modelo Alloy com os quatro invariantes .

Atendimento electrónico (FAQs) tinynew.gif

Q01 - Em b ⊥ a ≡ TRUE (página 170 dos apontamentos não devia ser b ⊤ a ≡ TRUE?

R: É uma gralha, obrigado por informar. Aparecerá corrigida na próxima versão desse capítulo. Agradece-se a comunicação de outras gralhas!


Q02 - Tenho uma dúvida na primeira questão do mini teste de 7 de Dezembro 2017. Na cláusula 3, o professor na resolução tem V :E ← V, não deveria ser V :E ← P ?

R: É também uma gralha, que acabo de corrigir. Obrigado por informar.


Q03 - Tentei resolver o exercício 5.45 por igualdade indirecta e não consegui. Muito provavelmente tenho que utilizar a (5.154) mas não consigo ver como.

R: A igualdade c◦ ·(⊤ − c) = ⊥ é equivalente e c◦ ·(⊤−c) ⊆ ⊥. Por (5.151) podemos subir o lado inferior, para c◦ ·(c⇒⊥) ⊆ ⊥. A partir daí aplica-se a (5.154), obtendo-se (c◦ ·c⇒⊥) ⊆ ⊥. Agora é que se pode aplicar a igualdade indirecta para mostrar que c◦ ·c⇒⊥ = ⊥.


Q04 - No exercico 5.24 aplico a definição de injectividade de uma relação seguido da definição de kernel à interseção de R com S, chegando ao ponto (R ∩ S)º . (R ∩ S) contido na identidade. Não sei como hei-de desenvolver o resto da expressão visto que não existe nenhuma fórmula para a composição de interseções.

R: Este é um exemplo em que regras de monotonia ou "thumb rules" ajudam. Veja, por exemplo, como a regra (5.82) o pode ajudar a resolver o exercício.


Q05 - No exercício 5.26 não sei como é que hei-de provar que (⊤.) é um closure operator. Qual é a estratégia?

R: Em (5.97) substitua ⊤ = !º.! e depois use "shunting" e (5.96).


-- JoseNunoOliveira - 15 Sep 2018

r34 - 17 Jan 2019 - 18:11:37 - JoseNunoOliveira
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM