Computação Fiável

1  Novidades

• e-conteúdos online. Encontrará nos e-conteudos informação actualizada sobre a disciplina de Computação Fiável.
• As aulas práticas começam já na primeira semana de aulas.

Contents

• 1  Novidades
• 2  Docentes
• 3  Objectivos
• 4  Competências por adquirir
• 5  Programa
• 6  Critérios de Avaliação
  • 6.1  Componente Ensino/Aprendizagem Prática
  • 6.2  Componente Ensino/Aprendizagem Teórica
  • 6.3  Admissão e Avaliação por Exame
• 7  Datas Importantes
• 8  Material Pedagógico e Referências Bbliográficas
• 9  Horário
• 10  Atendimento

2  Docentes

3  Objectivos

• Perceber e dominar o ciclo de vida do desenvolvimento de sistemas informáticos baseado em Métodos Formais.
• Conhecer os métodos formais existentes, saber quando devem ser aplicados e quais são os mais adequados em cada caso.
• Aplicar os Métodos Formais de especificação e verificação no desenvolvimento de sistemas informáticos.

4  Competências por adquirir

• saber construir e especificar formalmente um sistema informático, comprovar a correcção desta última e
• estar preparados para abordar as fases de prototipagem rápida e produção de implementações comprovadamente fiáveis

5  Programa

• Introdução: problemática, contexto, história e lugar dos Métodos Formais na Engenharia Informática e na Eng. de Software.
• Especificar, Modelar e Analisar SIs: Especificação formal, máquina abstracta de estados, lógica de Hoare. Semântica operacional, semântica denotacional
• Especificar e Demonstrar Propriedades de SIs: verificação de modelo, sistemas de prova automática, sistemas de ajuda a prova.
• Especificar e Derivar Implementações: extracção de programas, refinamento
• Especificar e Transformar: interpretação abstracta.

6  Critérios de Avaliação

Fraudes

6.1  Componente Ensino/Aprendizagem Prática

• A avaliação contínua mede em termos práticos a aquisição dos conceitos expostos. Como tal é baseada na realização de dois exercícios entregue à equipa docente.
• A Nota da Componente Prática (NCP, 20 valores) é a média das notas dos dois exercícios.

6.2  Componente Ensino/Aprendizagem Teórica

• Esta componente mede em termos teóricos a aquisição dos conceitos expostos. Como tal é baseada na realização de uma prova escrita: a frequência.
• Esta avaliação resulta na Nota da Componente Teórica (NCT, 20 valores).

6.3  Admissão e Avaliação por Exame

• Mínimos: são seguidas as disposições aprovadas pelo Conselho Científico da Universidade aplicadas individualmente as duas componentes de avaliação. É admitido a exame quem tiver ambas as notas NCP e NCT acima dos mínimos (i.e. NCP≥ 6 e NCT ≥ 6).
• A Nota da Prova Escrita do exame substituirá a Nota da Componente Teórica. Ou seja:
• A nota final (NF) continua a ser calculada como a média das duas avaliações:

  NF=

  NCT + NCP 2

7  Datas Importantes

• Entrega do enunciado do primeiro trabalho: semana do 19 de Outubro
• Entrega do primeiro trabalho: semana do 30 de Novembro
• Entrega do enunciado do segundo trabalho: semana do 30 de Novembro
• Entrega do segundo trabalho: semana do 25 de Janeiro
• Frequência: Quarta Feira 16 de Janeiro 2008
• Exame Época 1 : conferir nos SA.
• Exame Época 2 : conferir nos SA.
• Exame Época Especial : conferir nos SA.

8  Material Pedagógico e Referências Bbliográficas

• Apontamentos apresentados e disponibilizados nas aulas.
• Referências principais [11, 3, 10, 15, 16, 17, 9]
• Referências segundárias [8, 4, 5, 6, 13, 14, 2, 7, 19, 1, 18, 12]

9  Horário

10  Atendimento

References

[1]

J.-R. Abrial. The B-Book: Assigning Programs to Meanings. Cambridge University Press, 1996.

[2]

Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci, and Philippe Schnoebelen. Systems and Software Verification. Model-Checking Techniques and Tools. Springer, 2001.

[3]

Y. Bertot and P. Castéran. Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Serie. Springer Verlag, 2004. http://www-sop.inria.fr/lemme/Yves.Bertot/coqart.html

[4]

D. Bjorner. Software Engineering 1 : Abstraction And Modelling. Springer Verlag, 2005.

[5]

D. Bjorner. Software Engineering 2: Specification Of Systems And Languages. Springer Verlag, 2005.

[6]

D. Bjorner. Software Engineering 3: Domains, Requirements, And Software Design. Springer Verlag, 2005.

[7]

E.M. Clarke, O. Grumberg, and D Peled. Model Checking. MIT Press, 2000.

[8]

J. Cooke. Constructing correct software. Formal approaches to computing and information technology. Springer Verlag, 2005.

[9]

E. Gimenez. A tutorial on recursive types in Coq. http://coq.inria.fr/doc-eng.html

[10]

K. Lano and H. Haugthon. Specification in B: An Introduction using the B Toolkit. Imperial College Press, 1996.

[11]

J-F. Monin. Understanding Formal Methods. Springer Verlag, 2002. Translation editor M. Hinchey.

[12]

H. R. Nielson, F. Nielson, and C. L. Hankin. Principles of Program Analysis. Springer-Verlag, 1999.

[13]

B. C. Pierce. Types and Programming Languages. MIT Press, 2002.

[14]

B. C. Pierce, editor. Advanced Topics in Types and Programming Languages. MIT Press, 2005.

[15]

S. Schneider. The B-Method: An Introduction. Cornerstones of Computing series. Palgrave, 2001.

[16]

Coq Development Team. Reference manual of the Coq theorem prover. http://coq.inria.fr/doc-eng.html

[17]

Coq Development Team. A tutorial of the Coq theorem prover. http://coq.inria.fr/doc-eng.html

[18]

R. D. Tennent. Specifying Software. A Hands-On Introduction. Cambridge University Press, 2002.

[19]

G. Winskel. The Formal Semantics of Programming Languages: An Introduction. Foundations of Computing series. MIT Press, Cambridge, Massachusetts, February 1993.

This document was translated from L^AT_EX by H^EV^EA.