Métodos Formais em Engenharia de Software

Mestrado de [Engenharia] Informática (2012/13)

Tópicos

Avisos

15 Jul - Exame de recurso do módulo CSI - terá lugar dia tinynew.gif 18 de Julho (5ª-feira), às 9h30, na sala DI 1.08.

15 Jul - Publicadas as notas finais da época normal em tinynew.gif Funcionamento

6 Jul - As notas finais de AMT foram publicadas.

10 Jun - As classificações do teste de CSI encontram-se em Funcionamento.

08 Jun - Milestone 4 (PI): recomenda-se a leitura de How to write a great research paper (ver tinynew.gif Projecto) na preparação dos slides+relatório a apresentar nesta milestone final.

06 Jun - A Milestone 4 do PI terá lugar no dia 27-Jun - ver planeamento em tinynew.gif Sumários.

06 Jun - Chama-se a atenção dos alunos para o preenchimento na intranet dos inquéritos pedagógicos até tinynew.gif 3-Jul 2013.

13 Fev - Teste do módulo CSI - terá lugar dia 1 de Março (6ª-feira), às 9h00, na sala DI 1.08.

04 Jan - a milestone nr.1 do Projecto integrado terá lugar na próxima quinta-feira, 10-Jan, das 14h00 às 18h00, na sala DI 1.08 (1º andar do edifício do DI), sendo transmitidas via Skype para os supervisores nas empresas.

13 Nov - A WS de apresentação dos projectos (PI) aos alunos aulas terá lugar na próxima quinta-feira, 15-Nov, das 12h00 às 18h00, na sala DI 1.08 (1º andar do edifício do DI).

28 Set - As aulas iniciam-se na próxima quinta-feira, 4-Out, às 9h00, na sala DI 1.08 (1º andar do edifício do DI).

24 Set - A apresentaçao desta UC na Semana Inaugural MEI @ 2012/2013 terá lugar no dia 27-Set às 16h00, ver Sumários.

13 Set - Criação do site.

Material disponível ou a disponibilizar:

Bibliografia

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

Outros textos

  • J.N. Oliveira. Program Design by Calculation. Departamento de Informática, Universidade do Minho. Capítulo segundo deste livro em preparação.

Acetatos

  • J.N. Oliveira. Data type invariants: starting where (static) type checking stops (31 slides) 2012.

  • J.N. Oliveira. Pre / post-conditions -- starting where (pure) functions stop (35 slides) (updated 2012)

  • Alcino Cunha. An introduction to Alloy. Acetatos ligeiramente desactualizados no que respeita à modelação de sistemas dinâmicos.

  • J.N. Oliveira. PF transform: when everything becomes a relation (57 slides) (last update: Oct-2012)

  • J.N. Oliveira. “Theorems for free”: a (calculational) introduction (29 slides) (last update: Nov-2012)

  • J.N. Oliveira. PF transform: conditions and coreflexives for ESC (35 slides)

  • Alcino Cunha. Alloy: Under the Hood. Acetatos sobre semântica de lógica relacional, sistema de tipos e model finding. Para quem preferir código a notação matemática, pode consultar este programa em Haskell que implementa a semântica e o sistema de tipos.

  • Alcino Cunha. A perspective on model checking. Acetatos sobre modelação, especificação e verificação de sistemas reactivos: estruturas de Kripke, redes de Petri, lógica temporal (LTL e CTL), verificação de modelos por enumeração exaustiva do espaço de estados e simbólica, ordered binary decision diagrams.

Divulgação

  • Eric Bouwers, Joost Visser, Arie van Deursen. Getting What You measure. Communications of the ACM (CACM) 55(7):54-59, July 2012.

Exemplos

Exercícios e formulários

Enunciados de provas de avaliação individual

Módulo de VFS

Ferramentas

Vídeos

Repositórios

r64 - 04 Mar 2015 - 13:34:19 - MariaJoaoFrade
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM