{"id":2618,"date":"2016-06-13T08:25:06","date_gmt":"2016-06-13T11:25:06","guid":{"rendered":"http:\/\/www.inf.ufrgs.br\/profcomp\/?page_id=2618"},"modified":"2019-12-13T15:48:07","modified_gmt":"2019-12-13T18:48:07","slug":"cmp567","status":"publish","type":"page","link":"https:\/\/www.inf.ufrgs.br\/profcomp\/lista-de-disciplinas\/cmp567\/","title":{"rendered":"CMP567"},"content":{"rendered":"

T\u00f3picos Especiais em Computa\u00e7\u00e3o: Teste e Verifica\u00e7\u00e3o de Software<\/strong><\/p>\n

Respons\u00e1vel<\/strong>:\u00a0Leila Ribeiro<\/a> e Lucio Duarte<\/a>
\nCarga Hor\u00e1ria<\/strong>: 60 hs
\nCr\u00e9ditos<\/strong>: 4
\nSemestres Oferecidos<\/strong>: Segundo semestre<\/p>\n

S\u00daMULA<\/strong>
\nT\u00e9cnicas de verifica\u00e7\u00e3o est\u00e1tica e din\u00e2mica. Modelos de comportamento: tipos, modelagem, verifica\u00e7\u00e3o. Verificadores de modelos. Provadores de teoremas.<\/p>\n

OBJETIVOS<\/strong>
\nO principal objetivo da disciplina \u00e9 apresentar conceitos e t\u00e9cnicas fundamentais de verifica\u00e7\u00e3o de software e sua inser\u00e7\u00e3o dentro do desenvolvimento de um software, al\u00e9m de oportunizar a aplica\u00e7\u00e3o pr\u00e1tica destes conceitos e permitir a discuss\u00e3o das vantagens e limita\u00e7\u00f5es de cada t\u00e9cnica apresentada. Ao final da disciplina, espera-se que o aluno: (i) entenda a import\u00e2ncia da valida\u00e7\u00e3o e verifica\u00e7\u00e3o para a qualidade de sistemas computacionais; (ii) possua capacidade de criar modelos de comportamento para sistemas simples; (iii) compreenda o funcionamento de verificadores de modelo e saiba utiliz\u00e1-los para verificar propriedades; (iv) possua conhecimentos b\u00e1sicos de prova de teoremas e esteja habilitado a utilizar uma ferramenta que usa esta t\u00e9cnica de verifica\u00e7\u00e3o; (v) conhe\u00e7a os principais desafios em verifica\u00e7\u00e3o de software.<\/p>\n

PROGRAMA
\nSemana 1 \u2013 Introdu\u00e7\u00e3o<\/strong>
\n– Apresenta\u00e7\u00e3o da disciplina
\n– Conceitos b\u00e1sicos de valida\u00e7\u00e3o e verifica\u00e7\u00e3o;
\n– Aplica\u00e7\u00e3o de valida\u00e7\u00e3o verifica\u00e7\u00e3o no ciclo de desenvolvimento de software e sua import\u00e2ncia.<\/p>\n

Semanas 2 a 7 \u2013 Prova de Teoremas<\/strong>
\n– Revis\u00e3o de Teoria dos Conjuntos e L\u00f3gica de Primeira Ordem
\n– Especifica\u00e7\u00e3o de propriedades
\n– Introdu\u00e7\u00e3o \u00e0 Prova de Teoremas
\n– Provadores de teoremas
\n– Exerc\u00edcios com ferramenta de apoio
\n– T\u00f3picos avan\u00e7ados em Prova de Teoremas
\n– Realiza\u00e7\u00e3o de trabalho pr\u00e1tico<\/p>\n

Semanas 8 a 13 \u2013 Verifica\u00e7\u00e3o de modelos<\/strong>
\n– Introdu\u00e7\u00e3o a L\u00f3gica Temporal
\n– L\u00f3gica Temporal Linear (LTL)
\n– Especifica\u00e7\u00e3o de propriedades em LTL
\n– Introdu\u00e7\u00e3o \u00e0 Verifica\u00e7\u00e3o de Modelos
\n– Modelagem de sistemas
\n– Uso de verificadores de modelos
\n– Realiza\u00e7\u00e3o de trabalho pr\u00e1tico<\/p>\n

Semanas 14 a 15 \u2013 Apresenta\u00e7\u00e3o de trabalhos<\/strong>
\n– Apresenta\u00e7\u00e3o de trabalho comparativo entre o uso de Prova de Teoremas e Verifica\u00e7\u00e3o de Modelos e suas aplica\u00e7\u00f5es em atividades de desenvolvimento de software<\/p>\n

CRIT\u00c9RIOS DE AVALIA\u00c7\u00c3O<\/strong><\/p>\n

Ser\u00e3o realizados tr\u00eas trabalhos, T1, T2 e T3, considerando os seguintes conte\u00fados:<\/p>\n

– T1: Especifica\u00e7\u00e3o de propriedades
\n– T2: Prova de Teoremas
\n– T3: Verifica\u00e7\u00e3o de Modelos<\/p>\n

Os trabalhos T2 e T3 ser\u00e3o pr\u00e1ticos, utilizando as ferramentas computacionais de apoio da disciplina, enquanto os trabalhos T1 e T4 incluir\u00e3o a confec\u00e7\u00e3o de um relat\u00f3rio e apresenta\u00e7\u00e3o em aula.
\nA m\u00e9dia final (M) ser\u00e1 calculada da seguinte forma:<\/p>\n

M = (0,2 * T1) + (0,4 * T2) + (0,4 * T3)<\/p>\n

A convers\u00e3o da m\u00e9dia M para conceitos ser\u00e1 realizada como descrito a seguir:<\/p>\n

Faltas > 25% : FF (reprovado)
\nM < 6.0 : sem conceito (recupera\u00e7\u00e3o) – ver Atividades de Recupera\u00e7\u00e3o Previstas
\n6.0<= M < 7.5 : C (aprovado)
\n7.5 <= M < 9.0 : B (aprovado)
\n9.0 <= M : A (aprovado)<\/p>\n

Obs: Somente ser\u00e3o calculadas as m\u00e9dias finais daqueles alunos que obtiverem, ao longo do semestre, um \u00edndice de frequ\u0308.ncia \u00e0s aulas igual ou superior a 75% das aulas previstas. Aos que n\u00e3o satisfizerem este requisito, ser\u00e1 atribu\u00eddo o conceito FF (Falta de Frequencia).<\/p>\n

Para poder realizar a prova de recupera\u00e7\u00e3o, o aluno deve ter um \u00edndice de frequ\u00eancia de no m\u00ednimo 75% das aulas. Os que n\u00e3o se enquadrarem nesta situa\u00e7\u00e3o ter\u00e3o conceito FF. A recupera\u00e7\u00e3o versar\u00e1 sobre toda a mat\u00e9ria da disciplina. Ser\u00e3o considerados aprovados na recupera\u00e7\u00e3o os alunos que obtiverem um aproveitamento de, no m\u00ednimo, 60% da prova. A estes ser\u00e1 atribu\u00eddo o conceito C. Aos demais, ser\u00e1 atribu\u00eddo o conceito D. N\u00e3o h\u00e1 recupera\u00e7\u00e3o dos trabalhos por n\u00e3o comparecimento\/entrega, exceto nos casos previstos na legisla\u00e7\u00e3o (sa\u00fade, parto, servi\u00e7o militar, convoca\u00e7\u00e3o judicial, luto, etc.), sendo necess\u00e1ria a devida comprova\u00e7\u00e3o.<\/p>\n

BIBLIOGRAFIA<\/strong><\/p>\n

Clarke, E. M.; Grumberg, O.; Peled, D. A.. Model Checking. The MIT Press, 1999. ISBN 0262032708.
\nJastram, M.; Butler, M.. Rodin User’s Handbook v.2.8. CreateSpace Independent Publishing Platform, 2014. ISBN 978-1495438141. Dispon\u00edvel em: http:\/\/handbook.event-b.org<\/a>
\nEvent-B (Rodin platform). Dispon\u00edvel em: http:\/\/www.event-b.org\/<\/a>
\nRodin (project Deploy). Dispon\u00edvel em: http:\/\/www.deploy-project.eu\/<\/a> Magee, J.; Kramer, J.. Concurrency: State Models and Java Programming. Wiley, 2006. ISBN 978-0-470-09355-9.<\/p>\n","protected":false},"excerpt":{"rendered":"

T\u00f3picos Especiais em Computa\u00e7\u00e3o: Teste e Verifica\u00e7\u00e3o de Software Respons\u00e1vel:\u00a0Leila Ribeiro e Lucio Duarte Carga Hor\u00e1ria: 60 hs Cr\u00e9ditos: 4 Semestres Oferecidos: Segundo semestre S\u00daMULA T\u00e9cnicas de verifica\u00e7\u00e3o est\u00e1tica e din\u00e2mica. Modelos de comportamento: tipos, modelagem, verifica\u00e7\u00e3o. Verificadores de modelos. Provadores de teoremas. OBJETIVOS O principal objetivo da disciplina \u00e9 apresentar conceitos e t\u00e9cnicas fundamentais […]<\/p>\n","protected":false},"author":11,"featured_media":0,"parent":462,"menu_order":567,"comment_status":"closed","ping_status":"closed","template":"","meta":[],"_links":{"self":[{"href":"https:\/\/www.inf.ufrgs.br\/profcomp\/wp-json\/wp\/v2\/pages\/2618"}],"collection":[{"href":"https:\/\/www.inf.ufrgs.br\/profcomp\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/www.inf.ufrgs.br\/profcomp\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/www.inf.ufrgs.br\/profcomp\/wp-json\/wp\/v2\/users\/11"}],"replies":[{"embeddable":true,"href":"https:\/\/www.inf.ufrgs.br\/profcomp\/wp-json\/wp\/v2\/comments?post=2618"}],"version-history":[{"count":7,"href":"https:\/\/www.inf.ufrgs.br\/profcomp\/wp-json\/wp\/v2\/pages\/2618\/revisions"}],"predecessor-version":[{"id":3724,"href":"https:\/\/www.inf.ufrgs.br\/profcomp\/wp-json\/wp\/v2\/pages\/2618\/revisions\/3724"}],"up":[{"embeddable":true,"href":"https:\/\/www.inf.ufrgs.br\/profcomp\/wp-json\/wp\/v2\/pages\/462"}],"wp:attachment":[{"href":"https:\/\/www.inf.ufrgs.br\/profcomp\/wp-json\/wp\/v2\/media?parent=2618"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}