Métodos Formais em Engenharia de Software

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

Tópicos

Avisos

14 Jun - VF: tinynew.gif O exame de VF realiza-se no dia 19 de Junho (4ª feira), às 14:00, na sala CP2 1.12. Os alunos deverão trazer os seus computadores pessoais com o software utilizado nas aulas instalado. É permitida a consulta da documentação na parte laboratorial do exame.

14 Jun - VF: tinynew.gif As notas dos projecto e notas finais foram lançadas no Blackboard.

11 Jun - VF: As notas do 2º teste foram lançadas no Blackboard.

3 Jun - VF: A apresentação dos projectos realiza-se no dia 12 de Junho (4º feira), às 9:00, na sala 1.10 do DI. As apresentações são de 15 min. + 5 min. para perguntas. Todos os alunos deverão estar presentes na sessão. Os relatórios deverão ser entregues por email até ao dia 10 de Junho.

27 Mai - VF: O 2º teste de VF realiza-se na próxima 5ª feira, 30 de Maio, às 14:00, na sala E7 1.10. Os alunos deverão trazer os seus computadores pessoais com o sistemas Frama-C e CBMC instalados. É permitida a consulta da documentação.

16 Abr - VF: As notas do 1º teste foram lançadas no Blackboard.

16 Abr - VF: A distribuição dos projectos por grupos já está disponível na página de VF.

4 Abr - VF: Os temas dos projectos estão disponíveis. Por favor, comuniquem as vossas escolhas dos projectos a mjf@di.uminho.pt até 15-Abr.

26 Fev - A Workshop ClearSy terá lugar 4ª-feira 6-Mar, às 14h30. Estejam atentos a mais informações. Até lá, recomenda-se que vejam este video.

10 Fev - LEI: a quem estiver interessado - por favor comuniquem as vossas escolhas dos projectos em LEI a jno@di.uminho.pt até 21-Fev.

10 Fev - CSI: as notas após o exame de recurso foram lançadas na página de CSI.

31 Jan - VF: As aulas de Verificação Formal começam a 14-Fev.

29 Jan - Informa-se que o exame de recurso de CSI foi adiado para dia 6-Fev, às 15h00, na sala 0.05 do DI.

29 Jan - EM: as notas do exame foram lançadas no blackboard da disciplina.

28 Jan - O enunciado do teste de CSI tem agora a correcção proposta.

28 Jan - A Workshop ClearSy de que se falou nas aulas está prevista para 6-Mar (em não Fevereiro como arradamente se referiu). Será conduzida por Thierry Lecomte, especialista em uso de MFs na indústria dos transportes.

27 Jan - CSI: as notas à data do teste foram lançadas na página de CSI.

22 Jan - EM: as notas finais da época normal foram lançadas no blackboard da disciplina. (correção parcial na wiki)

16 Jan - CSI: 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.

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 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 » MFES1819 » WebHome » CSI

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

Information Systems by Calculation (E-Learning)

Programa da UC / Course syllabus

  • Métodos formais e qualidade de software. Conceitos básicos: modelo, especificação, verificação e prova.
  • As relações binárias polimórficas como linguagem de especificação formal universal. Setas e diagramas. Estudo do cálculo relacional 'pointfree'. Conexões de Galois. Polimorfismo paramátrico.
  • O papel das funções na taxonomia das relações binárias. Teorema grátis de uma função polimórfica.
  • Atributos e dependências funcionais. O modelo de dados 'pares valores-chave' construído com relações simples, emparelhamentos e coprodutos. Integridade referencial.
  • Preservação de invariantes e satisfação. Cálculo da precondição mais fraca 'wp (f, p)' para uma dada função 'f' e invariante 'p'. Relações (invariantes) como tipos.
  • 'Design by contract' por cálculo apoiado por model-checking.
  • Breve estudo da interpretação abstracta. Funções invariantes. Simulação relacional. Propriedades de segurança e de animação. Redução do espaço de estados por interpretação abstrata.
  • Formal methods for software quality. Basic concepts: model, specification, verification and proof.
  • Polymorphically typed binary relations as a universal formal specification language. Arrows and diagrams. Binary relations in Alloy. Study of the pointfree relational calculus. Galois connections. Parametricity.
  • The role of functions in the taxonomy of binary relations. Relations as types, inc. data type invariants. Theorems for free.
  • Attributes and functional dependencies. Key-value-pair data model = relational simplicity + pairing + coproducts. Referential integrity.
  • Data type invariants: preservation and satisfiability. Calculation of weakest preconditions for invariant preservation.
  • 'Design by contract': combining model-checking with algebraic calculation. Refinement ordering on relations.
  • Brief study of abstract interpretation. Invariant functions. Relational simulation. Safety and liveness properties relationally. Reducing the state space by abstract interpretation.

Bibliografia / Bibliography

  • J.N. Oliveira. Program Design by Calculation. Informatics Department, University of Minho. The chapters that matter for this course in this academic year are the 5th ( 1M), 6th ( 101K) and 7th ( 433K).

Horário / Timetable

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 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) - 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 - Cálculo relacional básico em Haskell (precisa da biblioteca Cp).

  • Script para converter instâncias geradas pelo Alloy para Haskell - 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:

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)

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

r48 - 17 Oct 2020 - 09:08:19 - JoseNunoOliveira
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM