área de pesquisa
- Verification of vehicular networks using probabilistic model checking
- An Algebraic Framework for Quantitative Information Flow
- A Methodology based on Timed Petri Net for Embedded Hard Real Time Software Synthesis
- A Methodology to Apply Formal Verification to UML-based Software
- A Model-driven approach to formal refactoring
- A Petri Net Based Estimator for Hardware/Software Codesign
- A rigorous methodology for developing GUI- based DSL formal tools
- A trusted execution environment-based architecture for cloud/fog-based IOT applications
- Abordagem para Geração Automática de Código para Framework de Automação de Testes
- Abordagem Relacional de Gramática de Grafos
- Abstraction of infinite and communicating CSPZ processes
- Adilson Luiz Bonifácio
- Adriano Xavier Carvalho
- Alexandre Cabral Mota
- Algebraic Formal Methods for Invariant Generation
- Aline Maria Santos Andrade
- Alocação de Redes Virtuais Baseada em Otimização de Restrição Distribuída
- Alvaro Heiji Miyazawa
- Ana Paula Luedtke Ferreira
- Angelo Perkusich
- Análise de Controle de Concorrência e Escalonamento de Transações em Bancos de Dados em Tempo-Real Usando Redes de Petri
- APSEE-Global: Um modelo de gerência de processos distribuídos
- Arquitetura para Integração Entre Modelos em Redes de Petri Coloridas e Modelos em Realidade Virtual: Uma Abordagem para Subestações Elétricas
- Assessment to support the planning of sustainable data centers with high availability.
- Avaliação de dependabilidade de sistemas com mecanismos tolerantes a falha: desenvolvimento de um método híbrido baseado em EDSPN e diagrama de blocos
- Avaliação de desempenho de processos de testes de software
- Avaliação de Desempenho e Consumo de Energia de Aplicações Embarcadas: Uma Estratégia Baseada em Modelos da Arquitetura de Hardware e no Código da Aplicação
- Avaliação e Modelagem de Dependabilidade de Data Centers
- Avaliação Quantitativa de Modelos em Gramática de Grafos Baseada em Objetos
- Avaliação Top-Down de Consultas de Caminhos Livres-de-Contexto em Grafos
- Bruno Ferreira
- BTS: Uma ferramenta de suporte ao desenvolvimento de sistemas confiáveis baseados em componentes
- Carlos Andreazza Rego Andrade
- Carlos Bazilio Martins
- Claudia Fernanda Oliveira Kiermes Tavares
- Claudio Ricardo Vieira Carvilhe
- Cláudia Maria Fernandes Araújo Ribeiro
- Coloured Petri Nets-Based Modeling and Validation of Insulin Infusion Pump Systems
- Concorrência, redes de petri e teoria da informação: aspectos comuns.
- CONSTRUCTIVE EXTENSIBILITY OF TRUSTWORTHY COMPONENT-BASED SYSTEMS
- Cristiano Bertolini
- César Augusto Lins de Oliveira
- Daniel Aguiar da Silva
- Diego Henrique Oliveira de Souza
- Diego Machado Dias
- Efficient and Mechanised Analysis of Infinite CSPz Specifications: Strategy and Tool Support
- Energy Consumption and Execution Time Estimation of Embedded System Applications.
- Especificação e verificação sistemática, formal e modular de sistemas embarcados.
- Especificações Formais Orientadas a Objetos: Aplicação no Desenvolvimento de um Sistema para Processamento do Eletrocardiograma de Esforço
- Estimativa do Consumo Energia devido ao Software: Uma Abordagem baseada em Redes de Petri Colorida
- Evaluation of GUI Testing Techniques for System Crashing: From Real to Model-based Controlled Experiments
- Exploração multiobjetivo do espaço de projeto de sistemas embarcados de tempo-real não críticos
- Extração de propriedades a partir dos diagramas de estados e de seqüência
- Fabiano Costa Carvalho
- Fernando Kauffmann Barbosa
- Fernando Luís Dotti
- Formal Specification of the ARINC 653 Architecture Using Circus
- Formal Techniques for the Specification and Verification of Protocols
- Formally verified compilation with the B method
- Frederico Jorge Ribeiro Barboza
- Gabriel Quadros Silva
- Geração Automática de Interface para Incorporação de IP-Cores em Ambientes SoC
- Geração Automática de Testes de Conformidade para Programas de Controlodares Lógicos Programáveis
- Geração de conjuntos de teste para sistemas reativos, de tempo-real, e com transformações de contexto.
- Geração e execução automática de testes para programas de controladores lógicos programáveis para sistemas instrumentados de segurança.
- Geração parcial de código Java a partir de especificações formais Z.
- Gerenciamento dinâmico de energia em processadores com cargas de trabalho variantes no tempo.
- Gerenciamento integrado de energia e controle de topologia em redes de sensores sem fio.
- Glaucia Boudoux Peres
- Gleifer Vaz Alves
- Gustavo Henrique Porto de Carvalho
- Gustavo Rau de Almeida Callou
- Haniel Moreira Barbosa
- Identificação de Nomes Ativos em Agentes-pi Baseada em Tipos
- ISPN: modelagem e avaliação estocástica intervalar
- Jandson Santos Ribeiro Santos
- JMSCAPACITY ? Um Toolkit para Auxiliar no Planejamento de Capacidade de Middlware Orientado a Mensagem
- Joker: An Animator for Formal Languages
- Jorge Cesar Abrantes de Figueiredo
- Jose Carlos dos Santos Junior
- José Amancio Macedo Santos
- José Cavalcante Reis Neto
- José Dihego da Silva Oliveira
- João Batista de Souza Neto
- Leonardo Reis Lucena
- Letícia Gindri
- Local Livelock Analysis for Component-Based Models
- Luciana Brasil Rebelo dos Santos
- M étodos Formais Alg ébricos para Gera ção de Invariantes
- Marcelo Fagundes Felix
- Marco Antonio de Castro Barbosa
- Maria Ligia Barbosa Perkusich
- Mecanismos de Interação para um Modelo de Redes de Petri Orientada a Objetos
- Model checking CSPZ: Techniques to overcome state explosion
- MODEL CHECKING PROBABILÍSTICO PARA APOIAR A MITIGAÇÃO DE EVENTO DE FALTA ÚNICA EM FIELD PROGRAMMABLE GATE ARRAYS (FPGAS)
- Model-Checking Circus with FDR using Circus2CSP
- Modelagem de Políticas de Estoque: uma Abordagem Baseada em Redes de Petri
- Modelagem e Análise de Especificações de Sistemas Embarcados Críticos com Restrições de Energia.
- Modelagem e análise de mecanismos de tratamento de interrupções em infraestruturas computacionais dos sistemas distribuídos
- Modelagem e Avaliação de Desempenho Operacional e Ambiental em Cadeias de Suprimentos Verdes
- Modelo de Falha Para Sistemas de Tempo Real
- Modelos para planejamento de redes convergentes considerando a integração de aspectos de infraestrutura e de negócios
- Mutação de Transformações para Teste de Programas Spark
- Mário Sérgio Ferreira Alvim Júnior
- New techniques for instantiation and proof production in SMT solving
- Parallelizing Java Programs using Transformation Laws
- Paulo Salem da Silva
- Processo Automatizado de Identificação de Pontos de Teste
- Prova Automática de Satisfatibilidade Módulo Teoria Aplicada ao Método B.
- Raul Fernandes Herbster
- Redes de Petri Orientadas a Objetos
- Sidney de Carvalho Nogueira
- Simone André da Costa Cavalheiro
- Simulação Automática e Gerador de Espaço de Estados de Modelos em RPOO
- Singularity: Um Método para Geração Automática de Casos de Testes Unitários baseado em Contraexemplos de Verificador de Modelos para Aplicações em C++
- Sistema de Reescrita de Termos para Intervalos: Em Direção a Um Modelo Formal para a Computação Intervalar
- Software Reliability Group (SRG)
- Software Synthesis for Energy-Constrained Hard Real-Time Embedded System
- Stephenson de Sousa Lima Galvão
- Suporte à análise e verificação de modelos RPOO.
- Taciano de Morais Silva
- THIAGO CARVALHO DE SOUSA
- Um ambiente de suporte à modelagem hierárquica por Redes de Petri para sistemas de produção
- Um estudo empírico sobre geração de testes com BETA: avaliação e aperfeiçoamento
- Um Metodo Baseado em Redes de Petri para a Modelagem de Bancos de Dados para Aplicações em Tempo-Real
- Um Metodo para o Desenvolvimento e Certificação de Software de Sistemas Embarcados Baseado em Redes de Petri Coloridas e Casos de Garantia
- Um protocolo para gerência de handoff em redes pessoais sem fio para aplicações de tempo real.
- Uma abordagem baseada em modelos para suporte à validação de sistemas médicos físico-cibernéticos.
- Uma Abordagem de Dois Nı́veis Baseada em Verificação de Modelos para Auxiliar na Análise de Conformidade Arquitetural de Software
- Uma Abordagem para Construção de Modelos de Dispositivos Médicos para Testes de Sistemas Médicos Físico-Cibernéticos
- Uma abordagem para construção de modelos de dispositivos médicos para testes em sistemas médicos físico-cibernéticos
- Uma Abordagem para Melhoria de Workflow Baseada em Redes de Petri Estocásticas Generalizadas
- Uma Biblioteca de Padrões de Especificação em Event-B para Mecanismos de Troca de Mensagens em Sistema Distribuídos
- Un système de types pour la programmation par réécriture embarquée
- Validando AJCSP com o uso de JPF por meio de leis algébricas CSP
- Validação Formal de Modelos de Manufatura Flexível com Lógica Dinâmica: o uso de Petri-PDL
- Validação visual de programas Ladder baseada em modelos.
- Vander Ramos Alves
- Verificador de modelos semanticamente correto
- Verification of behaviourist multi-agent systems by means of formally guided simulations
- Verificação automática de programas a partir da monitoração de múltiplas execuções de código.
- Verificação Automática de Programas pela Monitoração da Execução de Código: um Estudo de Caso de sua Aplicação de um Protocolo de Controle de Fluxo Adaptativo
- Verificação Formal da Função de Controle de Acesso ao Meio do Protocolo IEEE 802.11 e Investigação da sua Aplicabilidade em Sistemas de Tempo-Real
- Viny Cesar Pereira
- WPTrans: Um Assistente para Verificação de Programas em Frama-C.