Métodos Formais para Sistemas Críticos

Código:

M.EIC037

Sigla:

MFS

Áreas Científicas
Classificação	Área Científica
OFICIAL	Engenharia de Software

Ocorrência: 2024/2025 - 2S

Ativa?	Sim
Página Web:	http://moodle.up.pt/
Unidade Responsável:	Departamento de Engenharia Informática
Curso/CE Responsável:	Mestrado em Engenharia Informática e Computação

Ciclos de Estudo/Cursos

Sigla	Nº de Estudantes	Plano de Estudos	Anos Curriculares	Créditos UCN	Créditos ECTS	Horas de Contacto	Horas Totais
M.EIC	0	Plano de estudos oficial	1	-	6	39	162

Língua de trabalho

Inglês

Objetivos

Esta unidade curricular tem como objetivo geral familiarizar os estudantes com o desenvolvimento de sistemas críticos e como utilizar técnicas de especificação e verificação formal para aumentar a qualidade e confiabilidade de sistemas de software.

Resultados de aprendizagem e competências

No final da unidade curricular os estudantes devem ser capazes de:

1. Identificar os principais conceitos e técnicas associados ao desenvolvimento de sistemas críticos ("safety critical") baseados em software.


2. Identificar os principais conceitos e técnicas de especificação e verificação formal de sistemas baseados em software e reconhecer a sua importância e aplicabilidade.


3. Aplicar métodos de verificação formal por "model checking" na concepção de sistemas de software reativos de pequena e média complexidade com suporte de ferramentas.


4. Aplicar métodos de verificação formal por prova de teoremas a sistemas de software sequenciais de pequena e média complexidade com suporte de ferramentas.

Modo de trabalho

Presencial

Programa

1. Introdução aos sistemas críticos ("safety critical"): definição, normas internacionais, ciclo de vida, análise de risco, técnicas de garantia de segurança funcional, tolerância a falhas.


2. Introdução aos métodos formais de especificação e verificação de software: definição, importância, ciclo de vida, técnicas.


3. Verificação formal durante a concepção de sistemas reativos por "model checking": modelação de sistemas reativos, especificação de propriedades com lógica de primeira ordem e temporal, "model checking", ferramentas.


4. Verificação formal de sistemas sequenciais por prova de teoremas: lógica de Hoare, cálculo de pré-condição mais fraca, desenho por contrato ("design by contract"), ferramentas.

Bibliografia Obrigatória

Huth, M., & Ryan, M. ; Logic in Computer Science, Cambridge University Press, 2004. ISBN: 978-0-511-26401-6
Daniel Jackson; Software Abstractions, MIT Press, 2006. ISBN: 0-262-10114-9

Bibliografia Complementar

Alagar, V. S.; Specification of software systems. ISBN: 0-387-98430-5
Derrick G. Kourie, Bruce W. Watson; The correctness-by-construction approach to programming. ISBN: 978-3-642-27918-8
John Knight; Fundamentals of Dependable Computing for Software Engineers, Chapman & Hall, 2012. ISBN: 978-1439862551

Métodos de ensino e atividades de aprendizagem

Cerca de metade do tempo das aulas será usado para a exposição e estudo dos conteúdos programáticos, bem como resolução de desafios práticos em estilo tutorial. A outra metade do tempo será usada para a realização de exercícios práticos com suporte de ferramentas e realização do trabalho prático.

Software

Alloy4Fun
Dafny extension for Visual Studio Code
Alloy Analyzer 6
Dafny

Palavras Chave

Ciências Tecnológicas > Engenharia > Engenharia de computadores
Ciências Tecnológicas > Tecnologia > Tecnologia de computadores > Tecnologia de software

Tipo de avaliação

Avaliação distribuída sem exame final

Componentes de Avaliação

Designação	Peso (%)
Teste	60,00
Trabalho prático ou de projeto	40,00
Total:	100,00

Componentes de Ocupação

Designação	Tempo (Horas)
Estudo autónomo	60,00
Frequência das aulas	52,00
Trabalho laboratorial	50,00
Total:	162,00

Obtenção de frequência

• A presença nas aulas teórico-práticas é registada e obrigatória conforme legislação em vigor.


• Nota mínima de 40% no trabalho prático.

Fórmula de cálculo da classificação final

Avaliação distribuída sem exame final, com as seguintes componentes:

1. Miniteste 1 (MT1), duração 1h30, peso 30%, nota mínima de 40%.


2. Miniteste 2 (MT2), duração 1h30, peso 30%, nota mínima de 40%.


3. Trabalho prático (TP), peso 40%, nota mínima de 40%.

Provas e trabalhos especiais

Existirá um exame de recurso com duas partes (correspondentes a MT1 e MT2) a que todos os estudantes podem aceder (desde que tenham cumprido as regras de assiduidade, tenham atingido um mínimo de 40% no trabalho prático, e tenham realizado os dois minitestes, atingindo ou não a nota mínima nestes), para obtenção de aprovação ou melhoria de classificação a uma ou ambas as partes. Não existe recurso à componente prática (TP).

Trabalho de estágio/projeto

O trabalho prático será desenvolvido em grupo, onde se espera que os alunos apliquem as ferramentas estudadas nas aulas a um sistema crítico baseado em software de média dimensão.

Avaliação especial (TE, DA, ...)

Melhoria de classificação

A classificação dos minitestes pode ser melhorada em exame de recurso.