Área de concentração: 55134 - Ciências de Computação e Matemática Computacional

Criação: 24/02/2017

Nº de créditos: 6

Carga horária:

Teórica
Por semana
Prática
Por semana
Estudos
Por semana
Duração Total
3 0 7 9 Semanas 90 Horas

Docentes responsáveis:

Adenilso da Silva Simão
Márcio Eduardo Delamaro


Objetivos:

Permitir o contato dos alunos com métodos formais, baseados em notação matemática, para a especificação de software. Discutir de forma crítica as abordagens existentes atualmente. Dar ao aluno noções básicas de um ou mais métodos formais de especificação e experiência em seu uso em caso prático.


Justificativa:

Cresce em todo o mundo o interesse por métodos de especificação formais de software. Essas técnicas são especialmente importantes no desenvolvimento de sistemas críticos com relação a segurança (sistemas aviônicos, sistemas de controle de processos, sistemas de tempo real, etc.). É importante o domínio de técnicas formais que permitam o desenvolvimento seguro de software, com possibilidade de verificações formais de propriedades.


Conteúdo:

Métodos de especificação de software: visão histórica. paradigmas existentes, comparação entre métodos. Verificadores de Modelo: lógicas para especificação de propriedades, técnicas de verificação. Provadores de teoremas: técnicas de provadores, apoio ao desenvolvimento. Estudos de caso.


Forma de avaliação:

Provas, seminários e projetos.


Observação:

Nenhuma.


Bibliografia:

Fundamental
HINCHEY, M.G., and BOWEN, J.P. Application of Formal Methods, Prentice Hall, 1995.
Complementar
ALAGAR, V.S., and PERIYASAMY,K. Specification of Software Systems, Springer, 1999.
CLARKE, E.M. GRUMBERG, O. AND PELED, D.A. Model checking , Springer 1999
DUFFY, D. A. Principles of Automated Theorem Proving , 1992, John Willey & Sons.
Artigos científicos em periódicos e conferências da área

CONECTE-SE COM A GENTE
 

© 2024 Instituto de Ciências Matemáticas e de Computação