Português English
Contato

Grupos de Pesquisa | Fundamentos da Computação e Métodos Formais

O grupo de pesquisa Fundamentos da Computação e Métodos formais tem atuado na pesquisa e desenvolvimento de técnicas para garantir correção no desenvolvimento de software, tendo contribuído com diversas áreas dentro da ciência da computação. Para garantir que o desenvolvimento de software é realmente uma solução para o problema proposto, deve-se: construir um modelo de solução (especificação) utilizando uma linguagem formal; realizar provas matemáticas que garantem que este modelo possui as propriedades requisitadas (verificação); analisar se a solução proposta é aceitável do ponto de vista de desempenho, indicando quais as melhores estratégias para implementação a serem seguidas; validar o modelo através de simulações; realizar o desenvolvimento do software podendo-se provar que a implementação está correta (geração de código correto).

Pesquisadores Membros do Grupo

Temas de pesquisa correntes

  • Algoritmos e otimização: Projeto de algoritmos de memória externa, e algoritmos baseados em streams de dados, necessários para processar grandes volumes de dados. Modelagem matemática de problemas de otimização combinatória e desenvolvimento de algoritmos eficientes (ótimos e heurísticos) para resolução de tais problemas
  • Verificação e teste de software: Estudo de técnicas para verificação de correção e de propriedades funcionais e técnicas de validação de software
  • Linguagens de especificação e projeto de software: Investigação sobre linguagens adequadas às várias fases de desenvolvimento de software e diversas áreas de aplicação (por exemplo, aplicações de código móvel, banco de dados, sistemas reativos). Nesta linha também são investigadas maneiras de transformar programas/especificações preservando seu comportamento
  • Especificação e gerência do processo de software: Estudo, desenvolvimento e avaliação de tecnologias e métodos para especificação, planejamento, e gerência de projetos de software orientados a processo
  • Métodos analíticos e de simulação de sistemas complexos: Análise quantitativa de sistemas complexos estocásticos e deterministicos no contexto biológico, físico e social
  • Análise e modelagem do webgraph: Elaboração de modelos computacionais e analíticos para modelar a evolução temporal da rede web. Esses modelos servem como base, por exemplo, para testes de correção e eficiência de novos algoritmos que devem executar sobre o webgraph
  • Lógica aplicada à computação: Uso de lógica para especificação, verificação e estudo de propriedades de sistemas computacionais
  • Computação cognitiva: Definição de modelos computacionais para integração de raciocínio e aprendizagem de máquina
  • Computação natural: Construção de modelos para computação inspirados na natureza e modelagem de sistemas complexos
  • Especificação e verificação de sistemas embarcados: Uso de métodos formais no projeto de software embarcado
  • Complexidade computacional: Classificar problemas computacionais de acordo com sua dificuldade inerente, e relacionar essas classes entre si.

Projetos de Pesquisa Recentes na Área

  • AC-RS: Desenvolvimento de um Núcleo de Certificação Digital no Estado do Rio Grande do Sul. Participantes: UFRGS / Procergs / Banrisul / ACRS. Financiamento: ITI. Iniciado em 2006
  • PLATUS: Desenvolvimento formal e simulação de sistemas reativos (2004-2007). UFRGS. Financiamento: CNPq
  • IQ-Mobile: Improving the Quality of Open Systems with Code Mobility through Rigorous Development (2001-2004). UFRGS/PUCRS/CNR(Itália)/Universidade de Pisa (Itália). Financiamento: CNPq/CNR (Itália)
  • DACHIA: Modeling, Analysis and Development of an Approach for the Construction of High-Quality Internet Applications based on Visual Languages and Formal Methods (2003-2004). UFRGS/PUCRS/TU Berlin (Alemanha)/MSB (Alemanha). Financiamento: CNPq/DLR (Alemanha)
  • Form-X: Integração de dados (2005-2007) Fundamentos de Linguagens de Consulta no Contexto de Integração de Dados. Financiamento: CNPq/FAPERGS
  • Caracterização de Estratégias de Controle em Sistemas Multiagentes Heterogêneos (2005-2007). Financiamento: CAPES-GRICES

Resultados de Pesquisa Recentes

  • Técnicas e ferramenta de verificação para sistemas baseados em objetos, incluindo sistemas de tempo real
  • Técnicas de especificação para sistemas concorrentes e distribuídos orientados a objetos
  • Geração de grafos de grande dimensão construídos a partir da estrutura de ligação dos artigos da Wikipédia
  • Ambiente Prosoft-APSEE de apoio a gerência e desenvolvimento de projetos de software centrado a processos. O Prosfot-APSEE está atualmente evoluindo para uma versão em software livre chamada WebApsee)
  • Técnicas e ferramenta de especificação e verificação para sistemas com código móvel
  • Abordagem computacional para modelar a evolução do webgraph
  • Três patentes de algoritmos: Method and Apparatus for Providing a Survivable Network Design; Method and Apparatus for Updating Dynamic Shortest Path Graphs; Method and Apparatus for Providing Composite Link Assignment in Network Design