Diego Machado Dias

Formação complementar

Idiomas

Áreas de atuação

Participação em eventos

Produções bibliográficas

• DIAS, D. M. ; IYODA, J. M . Behavioural Preservation in Fault Tolerant Patterns. In: Brazilian Symposium on Formal Methods, 2011, São Paulo. Lecture Notes in Computer Science, 2011.

• DIAS, D. M. ; Robson Silva ; Leo Freitas ; Adolfo Duran . Mecanizando o componente de navegação do IBMs CICS: um experimento do Grande Desafio. In: IX Escola Regional de Computação Bahia - Alagoas - Sergipe, 2009, Ilheus. Anais da IX ERBASE, 2009.

• DIAS, DIEGO ; IYODA, JULIANO . Compositionality and correctness of fault tolerant patterns in HOL4. Science of Computer Programming (Print) , 2013.

• DIAS, D. M. ; DURAN, Adolfo Almeida . Verificação formal dos módulos de troca de mensagens, relógio e sleepers de um simple kernel. 2009. (Apresentação de Trabalho/Seminário).

• DIAS, D. M. ; Leo Freitas ; JONES, C. . Abstracting Interference in Postconditions Abstracting Interference in Postconditions. Newcastle: Newcastle University, 2014 (Technical Report (Relatório Técnico)).

Outras produções

Projetos de pesquisa

• 2010 - 2012

  Verificação de Modelos Voltados para Requisitos de Sistemas Aviônicos, Descrição: Requisitos para sistemas aviônicos são descritos usualmente por dois artefatos: um documento de requisitos em linguagem natural e um modelo formal (tipicamente, um diagrama Simulink). Neste projeto, propomos dois objetivos complementares: a tradução de requisitos escritos em linguagem natural controlada (um subconjunto não-ambíguo de linguagem natural) para propriedades em lógica temporal; e a geração de propriedades em lógica temporal a partir de um diagrama Simulink. O primeiro objetivo permite verificarmos de forma 100% automática se um modelo (traduzido de Simulink) satisfaz uma propriedade (traduzida de linguagem natural controlada). O segundo objetivo oferece ao engenheiro projetista uma lista de propriedades que o diagrama Simulink por ele proposto satisfaz. Este feedback pode revelar falhas de projeto ainda na fase de requisitos. Este projeto conta com o apoio da Embraer Empresa Brasileira de Aeronáutica S.A.. , Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (0) / Especialização: (0) / Mestrado acadêmico: (2) / Mestrado profissional: (0) / Doutorado: (0) . , Integrantes: Diego Machado Dias - Integrante / Juliano Manabu Iyoda - Coordenador / Alexandre Cabral Mota - Integrante / Augusto César Alves Sampaio - Integrante / Márcio Lopes Cornélio - Integrante / Flávia de Almeida Barros - Integrante / André Luís Ribeiro Didier - Integrante., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro.

• 2008 - 2009

  FLASH-FS: DESENVOLVIMENTO FORMAL DE COMPONENTES PARA UM SISTEMA DE ARQUIVOS VERIFICADO VOLTADO PARA MEMÓRIAS FLASH, Descrição: Este projeto endereça este mini desafio e propõe o desenvolvimento formal de um sistema de arquivo verificável baseado em memórias flash, compatível com o padrão POSIX. O desafio aqui é gerar: (i) a especificação formal do comportamento das funcionalidades oferecidas pelo sistema de arquivos; (ii) a lista de suposições inerentes ao hardware escolhido; (iii) e o conjunto invariantes, assertions, e propriedades relativas às estruturas de dados e algoritmos utilizados na implementação do sistema de arquivos. A etapa inicial deste projeto consiste na verificação formal de um micro-kernel que dará suporte ao sistema de arquivos a ser especificado. O micro-kernel que foi verificado é o simple-kernel proposto no livro Formal Refinement for Operating System Kernels (Iain D. Craig), que satisfaz as necessidades especificas deste projeto. Esta iniciativa visa potencializar a participação da UFBA no circuito de Métodos Formais. Com o desenvolvimento desse projeto, a UFBA passa a integrar uma comunidade de instituições de excelência que atuam em Métodos Formais.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (2) . , Integrantes: Diego Machado Dias - Integrante / Adolfo Duran - Coordenador / Aline Maria Santos Andrade - Integrante / Leonardo José Simões de Freitas - Integrante / Robson dos Santos e Silva - Integrante., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Bolsa.

• 2007 - 2009

  Melhoria da Infra-estrutura do Grupo de Pesquisa em Métodos Formais em Engenharia de Software (MEFES@UFBA), Descrição: Este projeto visa o fortalecimento do grupo de pesquisa MEFES@UFBA (Métodos Formais em Engenharia de Software), em forma de melhoria da infra-estrutura básica para a realização de atividades de pesquisa, difusão tecnológica, e gerenciamento de projetos. O MEFES@UFBA está cadastrado como Grupo de Pesquisa do CNPq deste 2005, e é sediado na Universidade Federal da Bahia. Com este projeto pretendemos potencializar a participação da Bahia no circuito de pesquisa em Métodos Formais, consolidando o grupo de pesquisa e fazendo parte da comunidade colaborativa que atua nesta área, contribuindo para solucionar os problemas relativos à construção de sistemas críticos verificáveis. Com a melhoria da infra-estrutura do MEFES@UFBA, será possível a articulação de uma rede cooperativa que agregue outros grupos, instituições de pesquisa e ensino, centros tecnológicos e empresas, com o intuito de aumentar a competência do Estado nesta área, além de estarmos colaborando para a construção de um cenário mais favorável à captação e fixação de novos doutores em Engenharia de Software para atuar em futuros programas de pós-graduação em Ciência da Computação na Bahia.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (2) . , Integrantes: Diego Machado Dias - Integrante / Robson dos Santos e Silva - Integrante / Adolfo Almeida Duran - Coordenador., Financiador(es): Fundação de Amparo à Pesquisa do Estado da Bahia - Auxílio financeiro., Número de produções C, T & A: 1

Prêmios