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: 2023/2024 - 1S

Ativa?	Sim
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.

Propriedades temporais lineares: segurança, vivacidade e justeza.

Introdução às propriedades regulares.

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

Modelação e especificação usando um model checker

Algoritmos de model checking para LTL e CTL.

Problema da explosão de estados. Equivalência de modelos.

Model checking simbólico: BDDs e OBDDs.

Técnicas de implementação de model checking.

Algoritmos de decisão baseados em autómatos.

Introdução à verificação de modelos temporizado e probabilístico.

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

Métodos de ensino e atividades de aprendizagem

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

Tipo de avaliação

Avaliação distribuída com exame final

Componentes de Avaliação

Designação	Peso (%)
Exame	100,00
Total:	100,00

Componentes de Ocupação

Designação	Tempo (Horas)
Estudo autónomo	114,00
Frequência das aulas	48,00
Total:	162,00

Obtenção de frequência

- A meio do semestre  haverá um teste, não obrigatório, cotado para 20 valores.
- O exame da época normal tem duas partes. A matéria da primeira parte corresponde à do teste, a da segunda parte à restante matéria lecionada na UC.
-Os alunos deverão obter um mínimo de 6 valores (em 20) em cada uma das partes.
- Os estudantes com cotação de seis ou mais valores no teste podem optar por não realizar a primeira parte do exame e usar
a nota obtida no teste para o cálculo da nota final (média aritmética).


Todos os alunos poderão realizar o exame de recurso.

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

Sendo PP a classificação obtida na primeira parte e SP a
classificação obtida na segunda parte, a nota final é dada por:
F = PP*(0.5) + SP*(0.5)
PP,SP >= 6 e F >= 9.5

Não obterão aprovação na avaliação distribuída, os alunos que não obtiverem um mínimo de 6 valores (em 20) em cada teste.
Para os alunos que não obtiverem aprovação, haverá um exame de recurso cotado para 20 valores.

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