Á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
© 2024 Instituto de Ciências Matemáticas e de Computação