Métodos Formais em Engenharia de Software

Mestrado Integrado em Engenharia Informática - MFES 2020/2021

Tópicos

Avisos

30 Out - CSI: módulo RelCalc.als já está disponível.

27 Out - EM: o servidor do alloy4fun já está a funcionar.

24 Out - CSI: preparação para as aulas tinynew.gif #03: ler secções 5.6 a 5.8 de Program Design by Calculation.

23 Out - CSI: aconselha-se os alunos a prestar atenção às FAQs que já começaram a sair na página da disciplina.

20 Out - CSI: foi enviado um e-mail aos alunos que estão listados na página de CSI. Quem porventura o não tiver recebido deve pf entrar em contacto com o docente.

17 Out - CSI: preparação para as aulas #02: ler secções 5.2 a 5.5 de Program Design by Calculation.

17 Out - CSI: como preparação para as aulas ver os sumários previstos e seguir as indicações semanais aqui nestes avisos. (Em CSI segue-se o método 'Flipped Classroom')

12 Out - As aulas iniciam-se esta semana.

17 Set - Vídeo de apresentação da edição 2020/21 de MFES.

Education » MFES » WebHome » CSI

Cálculo de Sistemas de Informação | Information Systems by Calculation (H507R1)

Horário | Timetable

Docente Foto Horário Salaup
José Nuno Oliveira jno 5ª-feira, tinynew.gif 13h-16h 1-1.21

Alunos | Students

# Nome Curso
a83916 Ana João Dias de Almeida MiEI
a85516 António Manuel Carvalho Gonçalves MiEI
a82529 Carlos Manuel Marques Afonso MiEI
a34900 Cecília da Conceição de Oliveira Soares MiEI
a67683 César Eduardo da Silva Magalhães MiEI
pg41842 César Hugo Moreira da Silva MEI
a80970 Davide da Silva Matos MiEI
a76089 Etienne da Silva Filipe Amado da Costa MiEI
a85731 Gonçalo José Azevedo Esteves MiEI
a86617 Gonçalo Pinto Nogueira MiEI
a81283 Hugo Filipe Oliveira de Sousa Faria MiEI
a85573 Jorge Gabriel Alves Cerqueira MiEI
a84776 José Emanuel Silva Rodrigues MiEI
pg42839 José Gonçalo Macedo Costa MEI
a84577 José Pedro Oliveira Silva MiEI
a85954 Luís Mário Macedo Ribeiro MiEI
a78566 Marcos Daniel Teixeira da Silva MiEI
a71407 Maurício Zulueta Lima Salgado MiEI
a82400 Márcio Alexandre Mota Sousa MiEI
a85700 Pedro Miguel Araújo Costa MiEI
a84783 Pedro Miguel Borges Rodrigues MiEI
a86266 Rafael Inácio Lourenço MiEI
a75411 Ricardo Guerra Leal MiEI
a81716 Rodolfo António Vieira da Silva MiEI
a80789 Rui Filipe Brito Azevedo MiEI
pg36086 Vítor Hugo Gonçalves Silva MEI

Programa | 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.


Regime de avaliação | Assessment

  • Duas provas escritas de avaliação (mini-teste + teste) e exame de recurso. | 2 written exams
  • As provas escritas são de consulta de material impresso. | The exams are open-book
  • O mini-teste é eliminatório de matéria para o teste e vale 50%. | The first exam amounts to 50% of the final mark


Bibliografia | Bibliography

  • J.N. Oliveira. Program Design by Calculation (, 2.4Mb), Departamento de Informática, Universidade do Minho. Textbook in preparation. Chapters relevant for this course: 5, 6, 7 (and possibly 8, time permitting).

Bibliografia adicional | Other bibliography

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


Ferramentas | Tools


Material | Teaching material

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


Atendimento electrónico | FAQs

Q01 - Eu resolvi o exercício 5.1 mas não precisei de usar a lei (5.17). Porque é que essa regra é sugerida?

R: O uso da lei (5.17), para f=sq e o resto identidades, poupa passos na resolução, que fica praticamente imediata.


Links

TBC

-- JoseNunoOliveira - 28 Sep 2020

r15 - 30 Oct 2020 - 08:39:33 - JoseNunoOliveira
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM