Código: | CC4008 | Sigla: | CC4008 | Nível: | 400 |
Áreas Científicas | |
---|---|
Classificação | Área Científica |
OFICIAL | Ciência de Computadores |
Ativa? | Sim |
Unidade Responsável: | Departamento de Ciência de Computadores |
Curso/CE Responsável: | Mestrado em Ciência de Computadores |
Sigla | Nº de Estudantes | Plano de Estudos | Anos Curriculares | Créditos UCN | Créditos ECTS | Horas de Contacto | Horas Totais |
---|---|---|---|---|---|---|---|
M:CC | 17 | PE a partir do ano letivo de 2014 | 1 | - | 6 | 42 | 162 |
MI:ERS | 22 | Plano Oficial desde ano letivo 2014 | 4 | - | 6 | 42 | 162 |
Pretende-se que o aluno:
- em ambas as vertentes, perceba a importância da utilização da lógica e dos sistemas formais no desenvolvimento de sistemas informáticos complexos;
- seja capaz de modelar sistemas simples e de especificar propriedades utilizando lógicas temporais;
- seja capaz de anotar programas simples duma linguagem imperativa ou orientada a objetos de modo a garantir propriedades de segurança e propriedades funcionais.
- Verificação por model checking de sistemas reactivos.
Sistemas reactivos. Lógica temporais: linear (LTL) e ramificada, (CTL e CTL*). Model checkers. NUSMV. Model checking simbólico: BDDs e OBDDs. Algoritmos de decisão baseados em autómatos finitos.
- Verificação de programas.
Cálculos de correção (Lógica de Hoare). Geração de obrigações de prova. Ferramentas para a especificação, verificação e certificação de programas imperativos.
Designação | Peso (%) |
---|---|
Exame | 50,00 |
Teste | 50,00 |
Total: | 100,00 |
Designação | Tempo (Horas) |
---|---|
Estudo autónomo | 50,00 |
Frequência das aulas | 50,00 |
Total: | 100,00 |