Verificação de Sistemas

Código:

CC4084

Sigla:

CC4084

Nível:

400

Áreas Científicas
Classificação	Área Científica
OFICIAL	Ciência de Computadores

Ocorrência: 2024/2025 - 1S

Ativa?	Sim
Página Web:	https://fm-dcc.github.io/sv2425
Unidade Responsável:	Departamento de Ciência de Computadores
Curso/CE Responsável:	Mestrado em Ciência de Computadores

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:CC	5	PE a partir do ano letivo de 2014	1	-	6	42	162

Língua de trabalho

Português - Suitable for English-speaking students

Objetivos

Introdução a técnicas formais de verificação de sistemas informáticos baseadas em modelos (model checking).

Resultados de aprendizagem e competências

Pretende-se que o aluno:
- perceba a importância da utilização da lógica e dos métodos formais no desenvolvimento de sistema informáticos complexos;
- seja capaz de modelar sistemas simples e de especificar propriedades utilizando lógicas temporais.

Modo de trabalho

Presencial

Programa

• Introdução ao model checking


• Modelação de sistemas paralelos: sistemas transição


• Paralelismo e comunicação com álgebras de processos


• Equivalências de sistemas de transição


• Ferramenta: mCRL2 (modelação)


• Lógicas dinâmicas (e relação com equivalências)


• Ferramenta: mCRL2 (verificação)


• Modelos de tempo real


• Ferramenta: Uppaal (modelação)


• Lógicas temporais: linear (LTL) e ramificada (CTL)


• Ferramenta: Uppaal (verificação)


• Introdução a modelos probabilísticos e estocásticos


• Ferramenta: Uppaal (simulações e PLTL)

Bibliografia Obrigatória

Baier Christel; Principles of model checking. ISBN: 978-0-262-02649-9

Bibliografia Complementar

Huth Michael 1962-; Logic in Computer Science. ISBN: 0-521-54310-X
Luca Aceto; Reactive systems. ISBN: 978-0-521-87546-2

Métodos de ensino e atividades de aprendizagem

Aulas expositivas e resolução de problemas e casos de estudo.

Software

Uppaal
mCRL2

Tipo de avaliação

Avaliação distribuída com exame final

Componentes de Avaliação

Designação	Peso (%)
Exame	60,00
Trabalho laboratorial	40,00
Total:	100,00

Componentes de Ocupação

Designação	Tempo (Horas)
Estudo autónomo	84,00
Frequência das aulas	48,00
Elaboração de projeto	30,00
Total:	162,00

Obtenção de frequência

Todos os estudantes serão admitidos a exame.

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

• TP1: A meio do semestre será preciso entregar a 1ª parte de um trabalho de grupo (2 pessoas), que valerá 20%.


• TP2: No final do semestre será preciso entregar a 2ª parte, que valerá 20%.


• Época normal: Os alunos com um mínimo de 6 valores (em 20) para o trabalho de grupo podem realizar um teste na época normal que valerá 60%.


• Época de recurso: todos os alunos poderão realizar o exame de recurso, que valerá o máximo entre 100% e 60% com o trabalho de grupo.

Os alunos que forem aprovados na época normal não precisam de efetuar o exame na época de recurso.

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

Os critérios de avaliação são os mesmos para todos os estudantes.

Melhoria de classificação

Será possível fazer melhoria de classificação em época de recurso.

Observações

Conhecimentos de lógica proposicional e de primeira ordem.