Funded projects

Um framework para a verificação de sistemas críticos (2020 - today / coordinator)

FAPERJ SEI-260003/001674/2021. Sistemas críticos exigem alta confiabilidade e estão presentes em diversas aplicações. As técnicas padrão de engenharia de software não são suficientes para garantir a ausência de falhas inaceitáveis e/ou que os requisitos críticos sejam atendidos. A verificação e certificação de sistemas ainda apresenta desafios. Este projeto se baseia no uso de lógica e linguagens com interpretação gráfica para a modelagem, verificação e geração de código certificado. Utilizam-se dois formalismos com suporte nativo à concorrência: redes de Petri e Reo. Esses são combinados a lógicas dinâmicas, possibilitando o uso de model checkers e o desenvolvimento de uma teoria da prova. A abordagem adotada consiste na construção de ferramentas que traduzam essas linguagens a modelos formais para ferramentas que automatizem a verificação e validação dos modelos.

Uma proposta para interoperabilidade de dados na nuvem (2020 - today)

Prefeitura de Niterói. No mundo moderno onde as informações circulam com uma rapidez fantástica, existe a necessidade de sistemas mais inteligentes e interligados que produz conhecimento para assessoramento dos gestores, de forma clara, precisa, concisa e rápida, na tomada de decisão. É no nível do município, onde seus moradores procuram ganhar a vida, existe a necessidade crescente e ao mesmo tempo, crucial que seus gestores tenham em mãos informações corretas e completas. Esta pesquisa pretende analisar a integração dos sistemas do município e principalmente, sua interoperabilidade, de forma que o conhecimento produzido possa ser empregado estrategicamente, taticamente e operacionalmente em benefício dos moradores e para uma gestão mais eficiente.
Este projeto tem por objetivo propor um modelo de interoperabilidade que permita a transformação de dados originados de diferentes sistemas para um modelo genérico de dados utilizando recursos de computação em nuvem, visando automatizar e ampliar a interoperabilidade dos sistemas e minimizar o custo monetário e/ou o tempo de comunicação entre os sistemas. Este modelo genérico seria obtido através do uso de técnicas de representação do conhecimento para gerar ontologias que atendam aos diferentes padrões de dados provenientes dos sistemas. O conjunto de ferramentas consiste de aplicações capazes de converter os padrões de diferentes dados no modelo genérico e uma API e/ou modelo para a incorporação de novos padrões de dados de forma dinâmica. Dessa forma, com os recursos disponibilizados online seria possível criar uma base de conhecimento dinâmica que armazena informações de sistemas antigos e novos. Além disso, o conjunto de ferramentas disponíveis em sistemas computacionais em nuvem garante a disponibilidade e integração de dados para que possam ser consumidos por novos sistemas que beneficiem o setor público. Os custos seriam flexíveis de acordo com a demanda de recursos necessários para os sistemas integrados.

Filosofia e Computação: interações contemporâneas (2017 - 2020)

CAPES-COFECUB 877/2017. O projeto está organizado em torno de questões filosóficas e epistemológicas sobre a ciência da computação e o processamento de informações (computação teórica). As disciplinas mobilizadas por esse programa interdisciplinar de pesquisa são, principalmente, a Filosofia (epistemologia e filosofia da informática), a Ciência da Computação Teórica e a Matemática.

Sistemas multiagentes e verificação formal: um framework para a verificação de propriedades (2016 - 2017 / coordinator)

FAPERJ E-26/010.000449/2016. Sistemas multiagentes são compostos por diversos agentes nos quais o objetivo de alguns depende do objetivo de outros. Os cenários são os mais plurais o possível: os agentes podem ser diferentes tanto em função quanto em arquitetura e sua interação é afetada pelo meio em que estão inseridos. Verificar propriedades como sobrevida, ausência de deadlocks e comunicação é essencial para se assegurar que esses sistemas cumprirão seus objetivos. Para tal, esse projeto propõe a construção de um arcabouço teórico e implementado baseado em lógica e Redes de Petri para auxiliar não só a formalização mas também efetuar inferências sob o modelo construído.

UFFeScience: Apoio Computacional a Experimentos de Larga Escala para Desenho de Novas Drogas para Tratamento de Doenças Tropicais Negligenciadas (2016 - 2019)

FAPERJ E-26/010.001670/2016. O termo "Doenças Tropicais Negligenciadas" (daqui em diante referenciado apenas como DTN) se refere a um grupo de doenças tropicais endêmicas que afetam em especial habitantes da Ásia, África e da América Latina. Algumas dessas DTN são responsáveis por altas taxas de mortalidade nessas regiões. Assim, para a população desses países, a descoberta de novas drogas que possam ser usadas como tratamento para as DTN é uma prioridade. Em especial no cenário brasileiro, e mais especificamente no estado do Rio de Janeiro, diversas DTN atingem parte da população, como por exemplo, a Dengue. Embora o Brasil tenha avançado significativamente na última década em vários campos da ciência, as pesquisas em áreas multidisciplinares como a bioinformática ainda estão em amadurecimento, e estas desempenham um papel fundamental para o desenvolvimento do país e do estado e para a descoberta de novas drogas para o tratamento das DTN. Diversas pesquisas de sucesso no ramo da bioinformática têm proposto protocolos in-silica (baseado em simulações computacionais) que utilizam análises filogenéticas/filogenônicas e mais recentemente as análises farmacofilogenônicas. Esses protocolos normalmente envolvem um conjunto de programas que executam simulações científicas e que são encadeados formando um fluxo coerente de atividades, ao qual denominamos workflow. Em um mesmo experimento de bioinformática para descoberta de novas drogas para DTN é comum que tenhamos mais de um workflow e que este mesmo workflow seja executado diversas vezes, variando-se dados de entrada e parametrização de configuração, a fim de confirmar ou refutar uma determinada hipótese. Entretanto, gerenciar um experimento nesse contexto não é uma tarefa trivial. Cada execução de um workflow pode consumir e produzir um grande volume de dados, o que comumente requer Processamento de Alto Desempenho (PAD) aliada a técnicas de paralelismo para produzir resultados em tempo hábil. A demanda por técnicas de gerência de experimentos em ambientes de PAD vem crescendo a cada ano, ao mesmo tempo em que surgem novos ambientes como as nuvens de computadores (que podem ser multi-site e federadas) e as unidades de processamento gráfico de propósito geral (GPGPUs). Um dos maiores desafios na gerência de experimentos científicos nesses ambientes reside na distribuição das execuções das atividades dos workflows nos recursos de forma eficiente. Essas execuções podem ser distribuídas em mais de um ambiente (cluster local, nuvem e GPGPU) e essa heterogeneidade insere uma complexidade adicional (e grande) no processo. Além disso, devemos nos preocupar com a gerência de metadados e com a análise dos resultados obtidos. Diversas pesquisas na área de mineração de dados e aprendizado de máquina têm sido propostas com foco na análise de grandes volumes de dados. Entretanto, os dados biológicos produzidos por esses experimentos não podem ser representados como tuplas chave-valor, como acontece tradicionalmente em algoritmos de mineração de dados (e.g. K-means). Dados biológicos são normalmente multi-relacionados, o que demanda técnicas de aprendizado de máquina mais complexas como a mineração de dados multi-relacional (MDMR). Uma vez que essas técnicas possam ser aplicadas/adaptadas no contexto de experimentos de bioinformática para descoberta de novas drogas podemos descobrir novos padrões de sequências, funções de genes e interações proteína-proteína que alavanquem investigações na terapia de DTN. O objetivo principal deste projeto de pesquisa está no desenvolvimento de novas técnicas de gerência de experimentos científicos baseados em simulação com o foco no apoio à descoberta de novas drogas para o tratamento das DTN.

Logic and Information (2014 - 2016)

CAPES 4804-14-7. This project aims to propose an improvement on a long-term already existing collaboration between INRIA, the brazilians and the argentin named team. We already have a CAPES-COFECUB cooperation (n. 690/10, namely "Teorias lógicas contemporâneas e a filosofia da linguagem: questões epistemológicas e semânticas") that leaded to many students interchange and technical visits of Professors, including the organisation of some workshops (the last one was the II Workshop on Logic and Semantics, at UERJ, Ilha Grande-RJ, Brazil - II Logic and Semantics). Prof. Gilles Dowek is also a Co-Advisor with Prof. Edward Hermann Haeusler of a brazilian Ph.D. Candidate in this project (and a former one also in this project, these two candidates finalised recently a sandwich doctorate - similar to stage doctorale - at INRIA). Prof. Gilles Dowek also collaborates with other members of this team and is supervising a post-doc project of another member. Since 2011 members of the team presents seminars in the Deducteam group, also coordinated by Prof. Gilles Dowek (more information in http://www.cri.ensmp.fr/people/hermant/deducteam/seminars.html), and since 2009 for the former group of Prof. Gilles Dowek at Laboratoire d'Informatique de l'École polytechnique (LIX). Among our collaboration we propose the development of some subprojects as specific goals. We propose the continuation of an ongoing joint work to propose a resolution based system for automatic theorem proving in some modal logics. The project also presents a subproject for reasoning about model-driven engineering discipline models defining a metamodel (the description of the syntax of a modeling language). Another subproject proposes two tasks regarding information extraction using logical background. The first one regards how to extract, process and interoperate data and the last one uses counterfactuals to reason about the future. It is important to notice that the results of the subprojects are interchangeable. More specifically we proposes a joint research with Deducteam about proof-compression, and developments in about verifying properties and extracting data about programs properties.

Teoria das Categorias e Teoria da Prova: Uma interação via Computação (2014 - 2017)

CNPq 442127/2014-6. Este projeto de pesquisa investiga como a Teoria da Prova e a Teoria das Categorias podem contribuir como base teórica para a fundamentação de Linguagens e Abordagens Lógicas e Semânticas. Seus objetivos globais são: (i) Investigar como técnicas e ferramentas da Teoria das Categorias podem ser usadas no processo de especificação semântica de modelos e sistemas (ii) Investigar como o uso de conceitos, técnicas e abordagens em Teoria da Prova podem ser usados na fundamentação de Linguagens e abordagens lógicas para a representação de conhecimento e modelos de sistemas (provavelmente com o uso de Ontologias Formais) (iii) Relacionar os ítens i e ii acima através de morfismos composicionais (Funtores) e associar uma semântica computável a estes morfismos. Os objetivos gerais são bastante amplos e ambiciosos. Vamos então passar aos objetivos específicos. Destacam-se: (i) A elaboração de sistemas dedutivos mais estruturados, que facilitam a geração de explicação de teoremas. (ii) Estender a pesquisa já iniciada e relatada por Lew & Haeusler no que diz respeito a obtenção de esquemas heurísticos para obtenção de provas curtas (tamanho polinomial em relação a apresentação da teoria) para lógicas já conhecidas da comunidade de representação do conhecimento (iii) Definição de novas lógicas mais adequadas a certos domínios específicos, como a representação de conhecimento legal, onde trabalhos anteriores em devem ser considerados (iv) Aplicar a álgebra de operações de composição e refinamento de ontologias, e seus respectivos algoritmos, como descrito por Kelsen, de forma efetiva a contribuir para a construção e validação composicional de ontologias; (v) Estudar a existência de Categorias com noções internas de finitude não padrão, de forma a incorpora-las em modelos computacionais para estudo teórico de hipercomputação.

Verificação de modelos de software com Lógica Dinâmica e Redes de Petri (2014 - 2017 / coordinator)

CNPq 441952/2014-3. Lógica Proposicional Dinâmica (PDL) é um sistema lógico multi-modal utilizada para especificar e verificar propriedades em programas sequenciais. Redes de Petri são um formalismo largamente utilizado na especificação de sistemas concorrentes e possuem uma interpretação gráfica bastante intuitiva. Neste trabalho apresentam-se aplicações de extensões da Lógica Proposicional Dinâmica onde os programas são substituídos por Redes de Petri Estocásticas de forma a efetuar a verificação formal de propriedades em software. O objetivo é converter automaticamente especificações UML em Redes de Petri Estocásticas para efetuar inferências e certificar propriedades.

Certificação de software através de Lógica Dinâmica e Redes de Petri (2014 - 2017)

FAPERJ 210.723/2014. Lógica Proposicional Dinâmica (PDL) é um sistema lógico multi-modal utilizada para especificar e verificar propriedades em programas sequenciais. Redes de Petri são um formalismo largamente utilizado na especificação de sistemas concorrentes e possuem uma interpretação gráfica bastante intuitiva. Neste trabalho apresentam-se aplicações de extensões da Lógica Proposicional Dinâmica onde os programas são substituídos por Redes de Petri Estocásticas de forma a efetuar a verificação formal de propriedades em software.

Lógica intuicionista como base para ontologias jurídicas (2012 - 2013)

CNPq 483460/2011-7. Este projeto visa investigar a eficiência da lógica descritiva intuicionista como alternativa à ALC clássica, com foco no domínio das ontologias jurídicas. Assim, espera-se promover a consolidação de conhecimentos de teoria da prova, focado na prova automática de teoremas. Além dos estudos sobre lógica descritiva, propõe-se o desenvolvimento de um ferramental para a prova automática de teoremas através de tableaux e dedução natural. Esse mesmo ferramental será adequado de forma que possa ser utilizado no ensino de lógica em cursos de graduação e pós-graduação. Por fim, trabalhar-se-á num módulo do provador para explicação em termos jurídicos.