• Tutorial 1: Desenvolvimento de Sistemas Baseado em Modelos

Ministrante: Profa. Dra. Leila Ribeiro

Leila Ribeiro possui graduação em Ciências da Computação pela Universidade Federal do Rio Grande do Sul (1988), mestrado em Ciências da Computação pela Universidade Federal do Rio Grande do Sul (1991) e doutorado em Informática - Technische Universitat Berlin (1996). Atualmente é pesquisadora nível 2 do Conselho Nacional de Desenvolvimento Científico e Tecnológico e professor associado da Universidade Federal do Rio Grande do Sul. É membro do IFIP Working Group 1,3 (Foundations of System Specification). Tem experiência na área de Ciência da Computação, com ênfase em Métodos Formais, atuando principalmente nos seguintes temas: especificação e semântica formal, bioinformática, verificação formal e modelos de computação.

Resumo: Desenvolver software confiável sempre foi difícil. Porém, com o tempo os desenvolvedores de software notaram que a tarefa da manutenção do software é tão ou mais difícil do que desenvolvê-lo. Software está em constante evolução: além de manutenções para remover erros, sempre surgem novas plataformas, novas tecnologias, novos requisitos, e os sistemas precisam ser adequados a estas novas realidades. Mas como fazer isto sem introduzir erros em sistemas que já estavam funcionando? Como fazer de maneira automática ou semi-automática estas mudanças? Como documentar as modificações, para poder revertê-las, caso necessário? Como saber que partes de um sistema precisam ser analisadas (testadas ou verificadas) novamente em decorrência da evolução? Model-Driven Development (MDD), ou Desenvolvimento Guiado por Modelos, é uma abordagem de desenvolvimento de software que surgiu para auxiliar no processo de evolução do software. Em MDD temos modelos para os sistemas e as mudanças são especificadas através de transformações destes modelos. Se os modelos e transformações tem um embasamento formal, pode-se não somente automatizar a evolução, mas também prever onde serão necessários novos testes, quais partes do sistema serão afetadas e como, etc. Neste minicurso apresentaremos os conceitos básicos de MDD, bem como discutiremos a sua aplicação na indústria e questões de pesquisa em aberto.

• Tutorial 2: Síntese automática de programas imperativos: uma abordagem abstrata

Ministrante: Prof. Dr. Alexandre Mota

Alexandre Mota possui doutorado em Ciência da Computação pelo Centro de Informática - UFPE (2001). Atualmente é pesquisador DT nível 2 do Conselho Nacional de Desenvolvimento Científico e Tecnológico e professor Associado III. Especialidade é Métodos Formais, focando: CSP, model checking, theorem proving, modelagem formal e refinamento. Atualmente vem investindo também na parte de Engenharia de Software Experimental, baseada em testes e simulações probabilísticas. Objetivo atual é aplicar Métodos Formais e Engenharia de Software Experimental para auxiliar no desenvolvimento de sistemas aeronáuticos, particularmente no entendimento e aplicação de Métodos Formais em Sistemas de Controle bem como no processo de Safety Assessment. De 2004 a 2008 fez pesquisas relacionadas a uma colaboração entre o Centro de Informática-UFPE e a Motorola. E desde 2006 vem colaborando com a Embraer. Foi vice-coordenador do Projeto COMPASS (Comprehensive Modelling for Advanced Systems of Systems), lado Brasil, financiado pela Comunidade Européia, edital FP7 durante 2011 e 2014. Atualmente é coordenador do projeto de pesquisa CIn-Motorola cujo foco é o teste de celulares.

Resumo: Síntese de programas visa automatizar a tarefa de programação. Neste curso apresentamos uma formulação clara e elegante de síntese de programas como uma análise de uma especificação em Alloy* (Extensão de Alloy para lidar com construtor de alta ordem) que satisfaz um contrato em termos de pré e pós-condiçães. Nossa proposta incorpora a sintaxe e a semântica denotacional de linguagem IMP de Winskel em Alloy*. Ilustramos nossa abordagem sintetizando alguns algoritmos clássicos, tais como o maior divisor comum de Euclides. Nossos experimentos mostram que o nosso tempo de síntese é razoavelmente competitivo. Além disso, Alloy* fornece-nos uma grande plataforma para o desenvolvimento de: um sintetizador elegante com base na semântica denotacional de uma linguagem em uma abordagem semelhante à prototipação rápida.

• Minicurso 1: Safety Critical Applications Development with Atelier B (in English)

Ministrante: Prof. Dr. Thierry Lecomte

Thierry Lecomte is currently in charge of R&D at ClearSy, French SME specialized in safety critical systems. His activities are related to the development of formal/formally proven CASE tools, formal modelling and data / configuration validation.

Resumo: this session introduces the development of proven software in B with Atelier B through a number of examples demonstrating formal specification, model animation, manual and automatic refinement, automatic and interactive proof, C code generation and execution. The examples are chosen among simplified industrial applications from railways and smart-card domains. The B language is introduced little by little as required by the formalizing of the software properties. Examples are demonstrated with Atelier B Community Version and ProB model-checker. Code generation requires basic knowledge of gcc (compilation, linking).

• Minicurso 2: Raciocínio Aproximado

Ministrantes: Prof. Dr. Regivan Santiago e Prof. Dr. Benjamin Bedregal

Regivan Santiago possui graduação em Tecnologia de Processamento de Dados pelo Centro de Estudos Superiores do Pará (1993), mestrado em Ciências da Computação pela Universidade Federal de Pernambuco (1995) e doutorado em Ciências da Computação pela Universidade Federal de Pernambuco (1999). Em 2007 realizou seu sabático junto ao Centro Alemão de Inteligência Artificial em Bremen-Alemanha. Atualmente é Professor Associado 3 da Universidade Federal do Rio Grande do Norte (UFRN). Tem experiência na área de Ciência da Computação, com ênfase em Teoria da Computação, atuando principalmente nos seguintes temas: Matemática Intervalar - fundamentos e aplicações, Especificação Formal, Teoria dos Domínios, Sistemas Fuzzy, Lógica e Semântica. No período de 2004-2005 coordenou o curso de pós-graduação em Sistemas e Computação da UFRN e exerceu o cargo de Secretário Regional da Sociedade Brasileira de Matemática Aplicada e Computacional.

Benjamin Bedregal possui graduação em Ingenieria de Ejecución en Computación e Informática - Universidad de Tarapacá-Chile (1986), mestrado em Ciências da Computação pela Universidade Federal de Pernambuco (1987) e doutorado em Ciências da Computação pela Universidade Federal de Pernambuco (1996). Fez também um pós-doutorado na Universidade Federal do Rio Grande do Sul (2005) e outro na Universidad Pública de Navarra (2011) em Espanha. É professor Titular da Universidade Federal do Rio Grande do Norte, onde ingressou no quadro permanente em 03/1999. Foi professor visitante desta mesma instituição entre 10/1996 a 02/1999. Chefe do Departamento de Informática e Matemática Aplicada no período de 08/2007 a 07/2009. Bolsista de produtividade nível 2 pelo CNPq desde 03/2007 até 02/2013 e a partir de 03/2013 é bolsista produtividade nível 1-D. Faz parte do quadro de professores permanente dos Programas de Pós-Graduação em Sistemas e Computação (PPgSC) e de Engenharia Elétrica e de Computação (PPgEEC), ambos da UFRN. Editor Associado das revistas:TEMA (desde 2014), e IEEE Transaction on Fuzzy Systems (desde janeiro de 2016). Tem experiência na área de Ciência da Computação, com ênfase em Teoria da Computação, atuando principalmente nos seguintes temas: lógica fuzzy, matemática intervalar, linguagens formais e computabilidade.

Resumo: O raciocínio humano tem, em geral, um carácter aproximado. Por exemplo, se você diz: "Se a noite estiver muito frio, então a maioria dos meus convidados não vai a minha festa". Esta frase considera aspectos imprecisos e não é adequadamente capturada em uma fundamentação precisa padrão, em que limiares devem ser fixados de antemão; por exemplo, abaixo de 10 graus Celsius estabelece que "A noite é muito frio" e a percentagem que representa a "maioria dos meus convidados" é de 51%. A lógica pode ser entendida como a ciência ou disciplina que estuda os princípios formais de raciocínio. Em particular, Lógica Fuzzy fornece um quadro preciso para lidar com tais raciocínios aproximados. Para nós, raciocínio aproximado aqui significa o processo a partir do qual conclusões imprecisas são deduzidas de premissas imprecisas. Este processo dedutivo é baseado em Lógica Fuzzy, em que os predicados são declarados através das chamadas variáveis linguísticas, a avaliação das frases considera tabelas verdade imprecisas e as regras de inferência são graduadas. Neste tutorial vamos fornecer uma visão geral desse quadro.

• Mini-curso 3: Definição e Verificação de Propriedades-Padrão sobre Programas

Ministrantes: Profa. Dra. Ana de Melo e Dra. Simone Hanazumi

Ana de Melo possui graduação em Bacharelado Em Ciência da Computação pela Universidade Federal de Pernambuco(1986), mestrado em Ciências da Computação pela Universidade Federal de Pernambuco(1989), Phd In Computer Science pela The University Of Manchester(1995) e pós-doutorado pela University of Oxford(2009). Atualmente é Professor Associado da Universidade de São Paulo, Consultor Ad-hoc do CNPq, CAPES e FAPESP e Revisor de vários Periódicos Internacionais. Tem experiência na área de Ciência da Computação, com ênfase em Teoria da Computação. Atuando principalmente nos seguintes temas: Verificação Formal e Validação de Programas, Métodos Formais, Teoria de Sistemas Concorrentes com Reconfiguração Dinâmica e Reutilização de Software e Hardware. É coordenadora do projeto VVTransv (FAPESP) que tem como objetivo utilizar as atividades de validação de sistemas e verificação de programas de forma complementar.

Simone Hanazumi possui graduação em Bacharelado em Ciência da Computação pela Universidade de São Paulo (2007), mestrado em Ciências da Computação pela Universidade de São Paulo (2010) e doutorado em Ciência da Computação pela Universidade de São Paulo (2015) com Estágio na Carnegie Mellon University/ NASA Ames Research Center (USA). Atualmente á analista e designer de software na HP Inc. do Brasil (R&D). Tem experiência na área de Ciência da Computação, com ênfase em Engenharia de Software, atuando principalmente nos seguintes temas: verificação formal, teste de software e programação Java.

Resumo: Produzir softwares com a qualidade adequada é uma tarefa, em geral, de alto-custo, principalmente porque envolve profissionais especializados em atividades de teste e verificação formal de sistemas e programas. Softwares produzidos como partes de sistemas críticos, nos quais falhas podem acarretar em desastres e perdas de vidas humanas, necessitam de aplicação de técnicas que assegurem a qualidade final do produto (os programas). Para esses sistemas, verificação e teste formal devem ser aplicados com o objetivo de que o produto de software preserve propriedades imprescindíveis ao seu funcionamento. Contudo, definir propriedades adequadas ao sistema desenvolvido, bem como efetivamente verificar essas propriedades sobre os programas que compõem o sistema não são tarefas triviais para os desenvolvedores de sistemas atualmente no mercado. Algumas iniciativas podem aproximar o mercado ao conhecimento e prática de técnicas de verificação e teste formal de software: em particular, facilitar a definição de propriedades com o uso de propriedades padrão (predefinidas) e produzir ferramentas que facilitem a prova de tais propriedades sobre programas. Este minicurso tem como objetivo apresentar técnicas para a definição de propriedades-padrão, frequentemente utilizadas em sistemas críticos, e usar o verificador de modelos JPF (JavaPathfinder - desenvolvido pela NASA) para a prova de propriedades-padrão sobre programas Java. Para a parte prática do minicurso, utilizaremos a ferramenta LTL2JPF (uma extensão do JavaPathfinder) que facilita a definição e prova de propriedades-padrão sobre programas Java.