Programação Certificada

1  Novidades

• Primeira versão da página. Encontrará aqui as novidades associadas à disciplina de Programação Certificada. A sua consulta regular é necessária ao bom funcionamento da Unidade Curricular.
• Como colocar uma dúvida ao regente da Unidade Curricular?
  1. Comparecer nas aulas e colocá-la directamente ao regente
  2. Comparecer no horário de atendimento do regente e colocá-la directamente
  3. enviar um email ao regente (desousaUUU@UUUdi.ubi.pt, (retire os UUU) ) com o assunto "PC: XXXX" em que XXX é o título da dúvida em questão. Qualquer outro formato no assunto arrisca condenar o email ao esquecimento.
• Inscrição em turmas práticas: via site dos serviços académicos.
• Os alunos com estatuto de trabalhador estudante são convidados a dirigir-se ao regente para discutir dos critérios de avaliação.

Contents

• 1  Novidades
• 2  Docentes
• 3  Objectivos
  • 3.1  Objectivos Gerais da UC
  • 3.2  Competências da UC ou Resultados da Aprendizagem
  • 3.3  Conteúdos
• 4  Programa
• 5  Critérios de Avaliação
  • 5.1  Componente Ensino/Aprendizagem
  • 5.2  Admissão e Avaliação por Exame
• 6  Datas Importantes
• 7  Software
• 8  Material Pedagógico e Referências Bbliográficas

2  Docentes

Simão Melo de Sousa (regente) - Gabinete 3.17 - Laboratório (Rel)ease (6.25) - Bloco VI

3  Objectivos

3.1  Objectivos Gerais da UC

Esta disciplina visa abordar os principais vectores de que depende o projecto fiável de aplicações à escala industrial.

3.2  Competências da UC ou Resultados da Aprendizagem

Após a conclusão desta UC, o aluno deverá ser capaz de:

• Estudar os diferentes aspectos de fiabilidade
• escolher a tecnologia, o formalismo e as ferramentas adequada a cada projecto de software fiável
• modelar, implementar sistemas fiáveis
• certificar, ou seja demonstrar com a ajuda do computador resultados de fiabilidade.

3.3  Conteúdos

Na sua componente teórica, a visão é a de abordar problemas de software segundo uma autêntica perspectiva de engenharia, criando modelos matemáticos sobre os quais é possível raciocinar e calcular. Na sua componente prática, a disciplina ensina a conceber e animar modelos de problemas, testando-os atempada e exaustivamente antes de se proceder à fase de cálculo e implementação, por forma a evitar erros de perspectiva ou imprecisões de concepção. Em suma: ensina-se a saber modelar, calcular, verificar, testar e avaliar.

4  Programa

• Verificação de Modelos Temporizados
• Provas de programa
• Desenho e Verificação de programas baseada em modelos
• Verificação de programas baseada em contractos
• Analise Estática de Programas

5  Critérios de Avaliação

A avaliação será realizada por avaliação contínua.

Fraudes

A equipa docente gostaria de realçar que qualquer tipo de fraude em qualquer dos itens desta disciplina implica a reprovação automática do aluno faltoso, podendo ainda vir a ser alvo de processo disciplinar. Listamos a seguir as diferentes componentes da avaliação.

5.1  Componente Ensino/Aprendizagem

• A avaliação contínua mede em termos práticos a aquisição dos conceitos expostos. Como tal é baseada na realização de exercícios entregue à equipa docente e que concluem a exposição de cada capítulo do programa previsto. Alguns exercícios poderão ter uma parte opcional que, se realizada, poderá valorizar a nota do exercício.
• A Nota da Componente Avaliação Contínua (NCAC, 20 valores) é a média das notas dos exercícios.

5.2  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 a nota NCAC acima dos mínimos (i.e. NCAC≥ 6).
• A Nota da Prova Escrita do exame substituirá a NCAC.

6  Datas Importantes

• Exame Época 1 : conferir nos SA.
• Exame Época 2 : conferir nos SA.
• Exame Época Especial : conferir nos SA.

7  Software

Proof Assistants : COQ

Design by contract - Deductive Program Verification : Principalmente why3, mas também Frama-C

Model checking: Uppaal

Model based Specification and Verification: Atelier B

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

• Apontamentos apresentados e disponibilizados nas aulas.
• Livro de Apoio: [1] (web-site : aqui)
• Referências Complementares:
  1. José Bacelar Almeida, Maria João Frade, Jorge Sousa Pinto, Simão Melo de Sousa. Rigorous Software Development, An Introduction to Program Verification, volume 103 of Undergraduate Topics in Computer Science. Springer-Verlag, first, 307 p. 52 illus. edition, 2011.
  2. Yves Bertot and Pierre Casteran. Interactive Theorem Proving and Program Development. Springer Verlag, 2004.
  3. J.-R. Abrial. The B-Book: Assigning Programs to Meanings. Cambridge University Press, 1996.
  4. 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.
  5. J-F. Monin. Understanding Formal Methods. Springer Verlag, 2002. Translation editor M. Hinchey.
  6. H. R. Nielson, F. Nielson, and C. L. Hankin. Principles of Program Analysis. Springer-Verlag, 1999.
  7. E.M. Clarke, O. Grumberg, and D Peled. Model Checking. MIT Press, 2000.

Enviar comentários e dúvidas para (retire os UUU) : desousaUUU@UUUdi.ubi.pt

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