Alexandre Cabral Mota
Alexandre Mota é Professor Titular do Centro de Informática (CIn) da UFPE e bolsista de Produtividade em Pesquisa do CNPq (nível PQ-C a partir de 2025) desde 2018, tendo acumulado sólida experiência como bolsista de Produtividade em Desenvolvimento Tecnológico (DT-2) entre 2011 e 2018. Sua principal área de expertise reside em Métodos Formais, aplicando a matemática ao desenvolvimento, verificação e síntese de sistemas complexos, com destaque para sua atuação em Blockchain após realizar Pós-Doutorado Empresarial na Lindy Labs (Portugal) voltado a contratos inteligentes em Solidity e em Inteligência Artificial, onde coordena o CRIAR (Centro de Inovação em Robótica e Inteligência Artificial Responsável). Ao longo de sua trajetória, tem se destacado pela liderança na integração entre PDI e o setor produtivo, coordenando inovação e pesquisa nos convênios CIn-Motorola (Software Services e LPX). Também participou de projetos estratégicos de grande porte com instituições como Embraer e o consórcio europeu COMPASS. Atualmente, suas pesquisas exploram a intersecção de Métodos Formais com o uso de Large Language Models (LLMs) para a segurança de software e automação de testes, consolidando uma atuação que combina excelência técnica, inovação e liderança multidisciplinar de impacto.
Informações coletadas do Lattes em 25/05/2026
Acadêmico
Formação acadêmica
Doutorado em Ciências da Computação
1998 - 2001
Universidade Federal de Pernambuco
Título: Model Checking CSPz: Techniques to Overcome State Explosion
, Ano de obtenção: 2001. Augusto Cézar Alves Sampaio. Coorientador: Paulo Henrique Monteiro Borba. Bolsista do(a): Conselho Nacional de Desenvolvimento Científico e Tecnológico, CNPq, Brasil. Palavras-chave: Model checking; Abstract Interpretation; Data Independence; Z Data Refinement.Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Metodologia e Técnicas da Computação / Especialidade: Métodos Formais. Setores de atividade: Aeronáutica e Espaço; Desenvolvimento de Programas (Software).
Pós-doutorado
2022 - 2023
Pós-Doutorado. , Lindy Labs (Internet), LINDY LABS, Portugal.
Idiomas
Inglês
Compreende Bem, Fala Razoavelmente, Lê Bem, Escreve Bem.
Espanhol
Lê Razoavelmente.
Francês
Lê Razoavelmente.
Áreas de atuação
Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Metodologia e Técnicas da Computação/Especialidade: Métodos Formais.
Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Metodologia e Técnicas da Computação/Especialidade: Engenharia de Software.
Organização de eventos
MOTA, A. ; MOTA, A. ; Membro do Comitê de Programa do FM. 2025. (Congresso).
MOTA, A. ; MOTA, A. ; Membro do Comitê de Programa do SBMF. 2025. (Congresso).
MOTA, A. ; MOTA, A. ; Membro do Comitê de Programa do ICST. 2022. (Congresso).
MOTA, A. ; MOTA, A. ; Membro do Comitê de Programa do ICST. 2021. (Congresso).
MOTA, A. ; MOURA, A. . Simpósio Brasileiro de Métodos Formais. 2004. (Congresso).
Participação em eventos
Brazilian Symposium on Formal Methods.Keynote Speaker. 2018. (Simpósio).
Congresso da Sociedade Brasileira de Computação. Congresso da Sociedade Brasileira de Computação. 2006. (Congresso).
Participação em bancas
Nascimento, A.; PRUDÊNCIO, R.;MOTA, A.. Explicando um classificador de requisições de mudança com métodos de XAI. 2026. Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.
NOGUEIRA, S.Carvalho, G.MOTA, A.. Investigando a corretude de um sistema robótico via RoboChart: Um sistema de distribuição de medicamentos do mundo real. 2025. Dissertação (Mestrado em Programa de Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.
MOTA, A.; Bonifácio, R.;SAMPAIO, A.. Generating formal smart-contract specifications from natural-language requirements supported by LLM. 2025. Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.
JESUS, J.;Carvalho, G.MOTA, A.. Comparing Autonomous Vacuum Cleaners Based on Coverage Path Planning of Grid-based Maps with Model-Checking. 2025. Dissertação (Mestrado em Programa de Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.
MOTA, A.; PRUDÊNCIO, R.; ALMEIDA, T. A.. CR Analysis: Classificação de Change Requests em um Ambiente de Fluxo de Dados. 2024. Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.
Farias, M.; MELLO, C. A. B.;MOTA, A.. Construção de aplicação web para hospedagem de algoritmo de avaliação automática da qualidade de imagens utilizando o Docker. 2024. Dissertação (Mestrado em Programa de Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.
IYODA, j.;NOGUEIRA, S.MOTA, A.. Formalização da Análise de Safety Estendendo STPA com CSP: Metodologia e Estudos de Caso. 2024. Dissertação (Mestrado em Programa de Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.
MOTA, A.; BARROS, F.; Nascimento, A.. Sistema de Recomendação de Desenvolvedores Especialistas para Projetos de Engenharia de Software: um Estudo de Caso. 2023. Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.
MOTA, A.; PRUDÊNCIO, R.; PARENTE, R. R.. Aprendizagem de Máquina na Engenharia de Software: Uma Abordagem Técnica para Análise de Defeitos Escapados. 2023. Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.
MOTA, A.; Greve, F.;SAMPAIO, A.. Specification is Law: Safe Creation and Upgrade of Ethereum Smart Contracts. 2022. Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.
MOTA, A.; Miranda, B.;Ribeiro, M.. Uma infraestrutura assistida por robô para detecção de perda de dados em Aplicativos Android. 2022. Dissertação (Mestrado em Programa de Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.
MOTA, A.; Nascimento, A.; PRUDÊNCIO, R.. A Machine Learning Approach to Escaped Defect Analysis. 2022. Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.
CARVALHO, T. C.; DIAS, K. L.;MOTA, A.. Uma Metodologia e Sistema para Teste de Conformidade de Rádios Cognitivos. 2021. Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.
MOTA, A.; MELLO, R. F. L.; BARROS, FLÁVIA. Um processo para construção de Tesauros de Domínio Específico no Contexto de uma Empresa de Teste de Software. 2021. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
Alves, E.;MACHADO, P.; ANDRADE, W.;MOTA, A.. Priorização de casos de teste para reduzir o espalhamento de casos. 2020. Dissertação (Mestrado em Ciência da Computação) - Universidade Federal de Campina Grande.
Amora, M.; Paula Jr., I.;MOTA, A.. Predição de Defeitos Just-in-Time em Software Utilizando Inteligência Artificial. 2020. Dissertação (Mestrado em Engenharia Elétrica e de Computação) - Universidade Federal do Ceará.
F. Barros; ALBERTINS, L.;MOTA, A.. DRL TC Classifier: Classificação de Casos de Teste para Automação de Testes de Dispositivos Móveis. 2020. Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.
SAMPAIO, A. C. A.; ALBERTINS, L.;MOTA, A.. AETing: An automated exploratory testing strategy based on code evolution coverage. 2020. Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.
MOTA, A.SAMPAIO, A.NOGUEIRA, S.. Auto Test Generator: a Framework to Generate Test Cases from Requirements in Natural Language. 2019. Dissertação (Mestrado em Programa de Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.
MOTA, A.; IYODA, j.; ALBERTINS, L.. HSP: A Hybrid Selection and Prioritisation of Regression Test Cases based on Information Retrieval and Code Coverage applied on an Industrial Case Study. 2019. Dissertação (Mestrado em Programa de Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.
MOTA, A.; ANDRADE, W.; IYODA, j.. Teste de gestos: Uma análise da rotação retrato e paisagem. 2018. Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.
MOTA, A.Coelho, R.; IYODA, j.. Aiding Exploratory Testing with Pruned GUI Models. 2017. Dissertação (Mestrado em Programa de Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.
MOTA, A.; ANDRADE, W.; Massoni, T.;FARIAS, A.. Listas usadas como conjuntos: Um estudo através de ferramenta de reescrita. 2017. Dissertação (Mestrado em Ciência da Computação) - Universidade Federal de Campina Grande.
MOTA, A.; IYODA, j.; ALBERTINS, L.. FREVoz: Um framework para automação de testes de voz. 2017. Dissertação (Mestrado em Programa de Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.
MOTA, A.; CASTELLETTI, C. H. M.; Garrozi, C.. HealthDrones - Navegação de VANTs autônomos baseada em autômatos celulares. 2017. Dissertação (Mestrado em Informática Aplicada) - Universidade Federal Rural de Pernambuco.
SOUSA, E.;MOTA, A.; TAVARES, E. A. G.. Avaliação de Qualidade de Experiência e Consumo de Energia em Transmissão Adaptativa de Vídeos em Dispositivos Móveis. 2016. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
MOTA, A.NOGUEIRA, S.; IYODA, j.. FINDOS - Uma ferramenta para identificação automática de unidades de rastreamento. 2016. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
MOTTA, L.; Gheyi, R.;MOTA, A.. Program synthesis from denotational semantics. 2016. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
SAMPAIO, A.NOGUEIRA, S.MOTA, A.. Um verificador de modelos para um subconjunto de Circus em K. 2016. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
IYODA, j.; Menezes, Luis;MOTA, A.. Probabilistic Analysis Applied to Robots. 2016. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
MOTA, A.; DURAN, A.; ANDRADE, A.. Uso de Sistemas de Transições Modais de Kripke para Representação de Comportamento Parcial durante o Desenvolvimento de Software. 2016. Dissertação (Mestrado em Ciência da Computação) - Universidade Federal da Bahia.
Alves, V.;MOTA, A.; Rincon, M.. Estratégias Comutativas para Análise de Confiabilidade em Linha de Produtos de Software. 2016. Dissertação (Mestrado em Ciência da Computação) - Universidade de Brasília.
MOTA, A.; AMORIM, M.; Pereira, F.. Techniques to Facilitate Probabilistic Software Analysis of Real-World Programs. 2015. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
MOTA, A.; LIMA, R.; FIDALGO, R.. Um catálogo de regras para validações estruturais de diagramas EER. 2015. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
MOTA, A.CORNÉLIO, M.; Massoni, T.. Evolução arquitetural de um Web service: transformação de código e avaliação de arquitetura. 2015. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
MOTA, A.SAMPAIO, A.FARIAS, A.. A Refinement based Strategy for Locally Verifying Networks of CSP Processes. 2014. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
IYODA, j.;FARIAS, A.MOTA, A.. Gerando Modelos SCADE a partir de Especificações Descritas em SCR. 2013. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
CORNÉLIO, M.FARIAS, A.MOTA, A.. A Rigorous Methodology for Developing GUI-based DSL Formal Tools. 2013. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
MOTA, A.; MOREIRA, A.; OLIVEIRA, M.. BTS: Uma ferramenta de suporte ao desenvolvimento sistemático de sistemas confiáveis baseados em componentes. 2013. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.
FARIAS, A.SAMPAIO, A.MOTA, A.. Estratégia sistemática para identificar falhas em componentes de hardware usando anotações HW em comportamento nominal. 2012. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
MOTA, A.; Gheyi, R.; IYODA, j.. Behavioural Preservation in Fault Tolerant Patterns. 2012. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
OLIVEIRA, M.; Kreutz, M.;MOTA, A.. Geração automática de hardware a partir de especificações formais: Estendendo uma abordagem de tradução. 2012. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.
MOTA, A.; ALENCAR, F.; FIDALGO, R.. Um Metamodelo e uma Ferramenta CASE para o Modelo EER. 2012. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
MOTA, A.Coelho, R.; AMORIM, M.. Rabbit: A novel approach to find data-races during state-space exploration. 2012. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
MOTA, A.; OLIVEIRA, M.; DÉHARBE, D.. Formal Verification of PLC programs using the B Method. 2012. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
MOTA, A.; Menezes, Luis; IYODA, j.. Extração Automática de Modelos CSP a partir de Casos de Uso. 2011. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
MOTA, A.; OLIVEIRA, M.;SAMPAIO, A.. Algebraic Laws for Process Subtyping. 2011. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
MOTA, A.Coelho, R.LIMA, R.. AJCSP: um compilador baseado em AspectJ para modularizar a programação concorrente em programas Java. 2011. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
MOTA, A.; Leite, J.; OLIVEIRA, M.. Joker: Um Framerwork de Animação para Especificações Formais. 2011. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.
MOTA, A.Coelho, R.; Meira, S.. A Regression Testing Approach for Software Product Lines Architectures. 2010. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
MOTA, A.; Neves, A.; BARROS, F.. ucsCNL - A Controlled Natural Language for Use Case Specifications. 2010. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
Droguett, E.; IYODA, j.;MOTA, A.. Systematic Model-Based Safety Assessment via Probabilistic Model Checking. 2010. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
FERRAZ, C.; IYODA, j.;MOTA, A.. Verificando a corretude de geradores automáticos de código. 2010. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
CORNÉLIO, M.; IYODA, j.;MOTA, A.. A Black-box Testing Technique for the Detection of Crashes Based on Automated Test Scenarios. 2009. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
GUSMÃO, C.; VASCONCELOS, A.;MOTA, A.. Uma Abordagem de Implantação de Testes Baseada em Metodologias Ágeis. 2008. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
CORNÉLIO, M.SAMPAIO, A.MOTA, A.. Mapeando CSP em UML-RT. 2008. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
MACHADO, P.; PRUDÊNCIO, R.;MOTA, A.. EvolUniT: Geração e Evolução de Testes de Unidade em Java Utilizando Algoritmos Genéticos. 2008. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
CORNÉLIO, M.SAMPAIO, A.MOTA, A.. Multi-sincronização em Message Sequence Charts. 2008. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
VASCONCELOS, A.; ALBUQUERQUE, J.;MOTA, A.. Adaptação do Processo de Desenvolvimento de Software para Análise de Cobertura de Código. 2007. Dissertação (Mestrado em Ciência da Comutação) - Centro de Informática.
VASCONCELOS, A.; SOARES, S.;MOTA, A.. Modelling and Integrating Formal models: From Test Cases and Requirement Models. 2007. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
MOTA, A.. Abordagem para Geração Automática de Código para Framework de Automação de Testes. 2007. Dissertação (Mestrado em Ciência da Comutação) - Centro de Informática.
MOTA, A.MACHADO, P.; GUERRERO, D.. Geração de Objetivos de Teste para Sistemas Reativos baseada na Técnica de Verificação de Modelos CTL. 2006. Dissertação (Mestrado em Informática) - Universidade Federal de Campina Grande.
MOTA, A.; MACEDO, H.; BARROS, F.. SpecNL: Uma Ferramenta para Gerar Descrições em Linguagem Natural a partir de Especificações de Casos de Teste. 2006. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
SAMPAIO, A.CORNÉLIO, M.MOTA, A.. Verificação de Modelos para um Subconjunto de JCSP. 2006. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
MOTA, A.BORBA, P.; CHAVEZ, C.. Deriving Refactoring for AspectJ. 2005. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
MOTA, A.MACHADO, P.; GUERRERO, D.; FIGUEIREDO, J.. Geração Automática de Casos de Teste para Sistemas baseados em Agentes Móveis. 2005. Dissertação (Mestrado em Informática) - Universidade Federal de Campina Grande.
MOTA, A.; FIGUEIREDO, J.; GUERRERO, D.. Modelagem de Sistemas com Restrições Temporais em Redes de Petri Orientadas a Objetos. 2005. Dissertação (Mestrado em Ciência da Computação) - Universidade Federal de Campina Grande.
MOTA, A.MACHADO, P.; PERKUSICH, A.; FIGUEIREDO, J.; GUERRERO, D.. Verificação de Modelos em Redes de Petri Orientadas a Objetos. 2004. Dissertação (Mestrado em Informática) - Universidade Federal de Campina Grande.
MOTA, A.SAMPAIO, A.; DÉHARBE, D.. Uma Estratégia para Composição Formal de Frameworks. 2004. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
MOTA, A.; Miranda, B.; IYODA, j.; SOUZA, S. R. S.;ARANHA, E.. Sound Test Case Generation for Concurrent Features Combining Test Cases for Individual Features. 2024. Tese (Doutorado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.
MOTA, A.; ROSA, N.; MELLO, C. A. B.; OLIVEIRA, M.; SIMAO, A. S.. A framework for testing cyber-physical systems: input generation and causal analysis. 2023. Tese (Doutorado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.
ZANCHETTIN, C.; BARBOSA, L. A.;MOTA, A.; CANUTO, A.; LORENA, A. C.. FILTRAGEM ROBUSTA DE RUÍDO DE RÓTULO PARA PREVISÃO DE DEFEITOS DE SOFTWARE. 2022. Tese (Doutorado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.
BARONE, D.;MOTA, A.; Rodrigues, G.; ISHIKAWA, E.. Command and Control Agility: a Software Product Line Approach. 2022. Tese (Doutorado em Informática) - Universidade de Brasília.
MELO, A.; OLIVEIRA, M.;MOTA, A.; IYODA, JULIANO;CORNÉLIO, M.. Safe and Constructive Design with UML components. 2022. Tese (Doutorado em Programa de Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.
MOTA, A.; SANTOS, A.; LETTNIN, D.; VARGAS, F.; MEDEIROS, V.. Técnica baseada em contratos para a validação da comunicação de alto nível entre software e hardware. 2018. Tese (Doutorado em Programa de Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.
MOTA, A.; Musicante, M.; COSTA, U.; GOMES, B.. Uma estratégia para validar a geração de códigos de Circus para Java. 2018. Tese (Doutorado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.
MOTA, A.; Rubira, C.; Bonifácio, R.; Rodrigues, G.. Feature-Family-based Reliability Analysis of Software Product Lines. 2017. Tese (Doutorado em Informática) - Universidade de Brasília.
IYODA, j.; OLIVEIRA, A.;MOTA, A.; POZO, A.; CANUTO, A.. Seleção Multiobjetivo de casos de teste utilizando Técnicas de busca híbridas. 2016. Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco.
BORBA, P.; ROSA, N.; BRAGA, C.; RIBEIRO, L.;MOTA, A.. Constructive Extensibility of Trustworthy Componente-based Systems. 2016. Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco.
BORBA, P.; TEIXEIRA, L.; OLIVEIRA, M.; SANTIAGO JUNIOR, V.;MOTA, A.. Formalisation of SysML Design Models and an Analysis Strategy using Refinement. 2016. Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco.
Musicante, M.; DÉHARBE, D.; OLIVEIRA, M.;MOTA, A.; GOMES, B.. Método B e a síntese verificada para código de montagem. 2016. Tese (Doutorado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.
MOTA, A.; Droguett, E.; MOURA, M.; CAVALCANTE, C.; GALVINCIO, J.. A Novel q-Exponential based Stress-Strength Reliability model and Applications to Fatigue Life with Extreme Values. 2016. Tese (Doutorado em Engenharia de Produção) - Universidade Federal de Pernambuco.
MOREIRA, A.;MOTA, A.; Musicante, M.; RIBEIRO, L.; OLIVEIRA, M.. Livelock Analysis for Component-based Systems. 2016. Tese (Doutorado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.
MOREIRA, A.; LEUSCHEL, M.; OLIVEIRA, M.;MOTA, A.MACHADO, P.. BETA: uma abordagem de testes baseada em B. 2016. Tese (Doutorado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.
MOTA, A.; ABRANTES, J.;MACHADO, P.FARIAS, A.. Towards a Test Generation Approach for Compositional Real-Time Systems. 2015. Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco.
MOTA, A.CORNÉLIO, M.; Massoni, T.;BORBA, P.; Gheyi, R.. Algebraic Laws for Object Oriented Programming with References. 2015. Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco.
MOTA, A.FARIAS, A.; ABRANTES, J.; CHAVEZ, C.;MACHADO, P.. Towards a test generation approach for compositional real-time systems. 2015. Tese (Doutorado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Campina Grande.
MOTA, A.. Techniques to Facilitate Probabilistic Software Analysis of Real-world Programs. 2015. Tese (Doutorado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.
Brelaz, Jaelson;MOTA, A.; CASTOR, F.; Braga, R.; Vivacqua, C.. Gerenciando Variações de Linhas de Produtos em Cenários de Casos de Uso. 2010. Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco.
MELO, A.; OLIVEIRA, M.; IYODA, j.;MOTA, A.SAMPAIO, A.. A Model-Driven Approach to Formal Refactoring. 2008. Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco.
MOTA, A.. A Refinement Theory for Alloy. 2007. Tese (Doutorado em Ciência da Computação) - Centro de Informática.
MOTA, A.; MACIEL, P.; ROSA, N.; WOODCOCK, J.. A Framework for Specification and Validation of Real Time Systems Using Circus Action. 2006. Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco.
MOTA, A.; FIGUEIREDO, J.; GUERRERO, D.; PERKUSICH, A.. Especificação e Verificação Sistemática, Formal e Modular de Sistemas Embarcados. 2006. Tese (Doutorado em Engenharia Elétrica) - Universidade Federal de Campina Grande.
Coelho, I.; Cavalcanti, G.;MOTA, A.. Gas Estimation for Ethereum Smart Contracts. 2025. Exame de qualificação (Doutorando em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.
ZANCHETTIN, C.; BRITTO JUNIOR, A. S.;MOTA, A.. Visual Sketch Coding: Conversão Automática de Esboços para Codificação de Programas. 2023. Exame de qualificação (Doutorando em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.
MOTA, A.; Miranda, B.; SOUZA, S. R. S.. Sound Test Case Generation for Concurrent Features Combining Test Cases for Individual Features. 2023. Exame de qualificação (Doutorando em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.
MOTA, A.; TEIXEIRA FILHO, J. G. A.; CUNHA, J. A. O. G.. Desastre em Projetos de Software: Construindo uma Teoria. 2019. Exame de qualificação (Doutorando em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.
Lima, M.; LETTNIN, D.;MOTA, A.. Comunicação confiável entre Device Drivers e Dispositivos de Plataformas embarcadas através da Validação de Propriedades Descritas em Contratos. 2016. Exame de qualificação (Doutorando em Ciências da Computação) - Universidade Federal de Pernambuco.
MOTA, A.; DÉHARBE, D.; OLIVEIRA, M.; Musicante, M.. Método B e a síntese verificada para código de montagem. 2015. Exame de qualificação (Doutorando em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.
BORBA, P.MOTA, A.; OLIVEIRA, M.. Formalisation of SysML Design Models and an Analysis Strategy using Refinement. 2015. Exame de qualificação (Doutorando em Ciências da Computação) - Universidade Federal de Pernambuco.
BORBA, P.MOTA, A.; BRAGA, C.. Constructive Extensibility of Trustworthy Component-based Systems. 2015. Exame de qualificação (Doutorando em Ciências da Computação) - Universidade Federal de Pernambuco.
Rubira, C.; Bonifácio, R.;MOTA, A.. Evolução de Linhas de Produtos de Software Dinâmicas, Abertas, e Cientes de Confiabilidade. 2014. Exame de qualificação (Doutorando em Informática) - Universidade de Brasília.
MOTA, A.; Alves, V.; Rubira, C.; Rodrigues, G.. Uma abordagem sensível ao histórico de linhas de produtos de software para a verificação de confiabilidade. 2014. Exame de qualificação (Doutorando em Ciências da Informação) - Universidade de Brasília.
MOTA, A.CORNÉLIO, M.; OLIVEIRA, M.. Formalisation of SysML Design Models and an Analysis Strategy using Refinement. 2014. Exame de qualificação (Doutorando em Ciências da Computação) - Universidade Federal de Pernambuco.
MOTA, A.BORBA, P.; MELO, A.. A Refinement Theory for Alloy. 2006. Exame de qualificação (Doutorando em Ciências da Computação) - Universidade Federal de Pernambuco.
MOTA, A.SAMPAIO, A.; HAEUSLER, E.. A Model-Driven Approach to Program Refactoring. 2005. Exame de qualificação (Doutorando em Ciências da Computação) - Universidade Federal de Pernambuco.
MOTA, A.; ABRANTES, J.; GUERRERO, D.; PERKUSICH, A.. Síntese e Adaptação de Modelos de Redes de Petri Coloridas. 2004. Exame de qualificação (Doutorando em Engenharia Elétrica) - Universidade Federal de Campina Grande.
MOTA, A.; FIGUEIREDO, J.; SOUZA, B.; PERKUSICH, A.; TURNELL, M.. Métodos Formais no Projeto de Interfaces para Sistemas Industriais Críticos. 2004. Exame de qualificação (Doutorando em Engenharia Elétrica) - Universidade Federal de Campina Grande.
MOTA, A.CORNÉLIO, M.. Aplicando regras de programação para refatoração de programas em Dafny: uma linguagem imperativa com especificação nativa. 2015. Trabalho de Conclusão de Curso (Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.
MOTA, A.BORBA, P.. Transformação de programas Java seqüenciais em concorrentes. 2005. Trabalho de Conclusão de Curso (Graduação em Ciência da Computação) - Fundação Ford.
MOTA, A.BORBA, P.. Ferramentas para Construção de Linha de Produtos no ECLIPSE. 2005. Trabalho de Conclusão de Curso (Graduação em Ciência da Computação) - Fundação Ford.
MOTA, A.SAMPAIO, A.. Repositório de Design Patterns para Desenvolvedores. 2005. Trabalho de Conclusão de Curso (Graduação em Ciência da Computação) - Fundação Ford.
MOTA, A.; VASCONCELOS, A.. Mapeamento do modelo de Melhoria do Processo de Software Brasileiro (MPS-Br) para empresas que utilizam metodologia Extreme Programming (XP) como metodologia de desenvolvimento. 2005. Trabalho de Conclusão de Curso (Graduação em Ciência da Computação) - Fundação Ford.
MOTA, A.SAMPAIO, A.. Refine: Procedimentos e Recursão. 2003. Trabalho de Conclusão de Curso (Graduação em Ciências da Computação) - Universidade Federal de Pernambuco.
MOTA, A.; GOMES, A.. Especificação de Sistemas Colaborativos usando Teoria da Atividade. 2003. Trabalho de Conclusão de Curso (Graduação em Ciências da Computação) - Universidade Federal de Pernambuco.
MOTA, A.; VASCONCELOS, A.. ProcessDirection: Uma Ferramenta para Direcionar Processos de Desenvolvimento de Software. 2003. Trabalho de Conclusão de Curso (Graduação em Ciências da Computação) - Universidade Federal de Pernambuco.
MOTA, A.SAMPAIO, A.. Geração Automática de Java Assertions a partir de Especificações Z. 2002. Trabalho de Conclusão de Curso (Graduação em Ciências da Computação) - Universidade Federal de Pernambuco.
MOTA, A.; ROSA, N.; OLIVEIRA, M.; Souza, A.. Banca de Avaliação da Promoção à Classe de Titular da Carreira do Magistério EBTT. 2026. Instituto Federal da Bahia.
MOTA, A.CORNÉLIO, M.; SOARES, S.. Concurso para professor auxiliar. 2006. Universidade de Pernambuco.
MOTA, A.. Concurso para professor auxiliar. 2003. Universidade de Pernambuco.
MOTA, A.. 67a Reunião da SBPC. 2015. Instituto Ciência Hoje/SBPC.
MOTA, A.. 66a Reunião Anual da SBPC. 2014. Sociedade Brasileira para o Progresso da Ciência - São Paulo.
MOTA, A.. 65a Reunião Anual da SBPC. 2013. Sociedade Brasileira para o Progresso da Ciência - São Paulo.
MOTA, A.. 64a Reunião Anual da SBPC. 2012. Sociedade Brasileira para o Progresso da Ciência - São Paulo.
MOTA, A.; SANTOS, A.; CAVALCANTE, S.. Imagine Cup - Etapa Regional. 2005. Microsoft Brasil.
MOTA, A.. Processo de Avaliação de Projetos do Programa Institucional de Iniciação Científica (2003/2004) - PIBIC/CNPq/UFPE. 2003. Universidade Federal de Pernambuco.
Orientou
Início: 2018; Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco;
Abordagem Experimental para Comprovação de Otimização de Gás em Contratos Inteligentes Solidity; Início: 2025; Iniciação científica (Graduando em Sistemas de Informação) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; (Orientador);
Verificação de Contratos Inteligentes usando Model Checking (Co-orientador); Início: 2024; Iniciação científica (Graduando em Ciência da Computação) - Universidade Federal de Pernambuco; (Orientador);
Manutenção automática de casos de testes automatizados; Início: 2022; Iniciação científica (Graduando em Ciência da Computação) - Universidade Federal de Pernambuco, Fundação de Apoio ao Desenvolvimento da Universidade Federal de Pernambuco; (Orientador);
Investigando a corretude de um sistema robótico via RoboChart: Um sistema de distribuição de medicamentos do mundo real; 2023; Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco, ; Orientador: Alexandre Cabral Mota;
Assessor Models with Reject Option for soccer result prediction; 2022; Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco, ; Coorientador: Alexandre Cabral Mota;
Comparing Autonomous Vacuum Cleaners Based on Coverage Path Planning of Grid-based Maps with Model-Checking; 2021; Dissertação (Mestrado em Programa de Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco, ; Orientador: Alexandre Cabral Mota;
Formalização da Análise de Safety estendendo STPA com CSP: Metodologia e Estudos de Caso; 2021; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, ; Orientador: Alexandre Cabral Mota;
HSP: A Hybrid Selection and Prioritisation of Regression Test Cases based on Information Retrieval and Code Coverage applied on an Industrial Case Study; 2019; Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco, ; Orientador: Alexandre Cabral Mota;
Testes de smartfones; 2018; Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco, ; Orientador: Alexandre Cabral Mota;
Aiding Exploratory Testing with Pruned GUI Models; 2017; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, ; Orientador: Alexandre Cabral Mota;
Probabilistic Analysis Applied to Robots; 2016; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, ; Orientador: Alexandre Cabral Mota;
Uso do framework K na construção de um verificador de modelos correto; 2016; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; Orientador: Alexandre Cabral Mota;
Program Synthesis from Denotational Semantics; 2016; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, ; Orientador: Alexandre Cabral Mota;
Transformação sistemática entre modelos Scade e SCR; 2016; Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco, ; Coorientador: Alexandre Cabral Mota;
A Rigorous Methodology for Developing GUI-based DSL Formal Tools; 2015; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; Orientador: Alexandre Cabral Mota;
Gerando Modelos SCADE a partir de Especificações Descritas em SCR; 2015; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, ; Orientador: Alexandre Cabral Mota;
Derivando lógicas de falhas a partir de modelos nominais; 2014; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, ; Orientador: Alexandre Cabral Mota;
Systematic Model-Based Safety Assessment of Aircraft Systems via Probabilistic Model Checking; 2010; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; Orientador: Alexandre Cabral Mota;
Verificando a corretude de geradores automáticos de código; 2010; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, ; Orientador: Alexandre Cabral Mota;
Design and Formal Verification of Fly-by-Wire Flight Control Systems; 2009; Dissertação (Mestrado em Ciência da Comutação) - Universidade Federal de Pernambuco, SOFTEX; Orientador: Alexandre Cabral Mota;
A Black-box Testing Technique for the Detection of Crashes Based on Automated Test Scenarios; 2009; Dissertação (Mestrado em Ciência da Comutação) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Alexandre Cabral Mota;
Processo Automatizado de Identificação de Pontos de Teste; 2008; 0 f; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; Orientador: Alexandre Cabral Mota;
Parallelizing Java Programs using Transformation Laws; 2008; 0 f; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Alexandre Cabral Mota;
Modelling and Integrating Formal models: From Test Cases and Requirement Models; 2007; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; Orientador: Alexandre Cabral Mota;
Abordagem para Geração Automática de Código para Framework de Automação de Testes; 2007; Dissertação (Mestrado em Ciência da Comutação) - Centro de Informática, ; Orientador: Alexandre Cabral Mota;
Verificação de Modelos para um Subconjunto JCSP; 2006; 100 f; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, ; Orientador: Alexandre Cabral Mota;
Geração Automática de Modelos UML-RT a partir de Especificações CSP; 2006; Dissertação (Mestrado em Ciência da Comutação) - Centro de Informática, ; Coorientador: Alexandre Cabral Mota;
Geração Automática de Casos de Teste a Partir de Especificações CSP; 2006; Dissertação (Mestrado em Ciência da Comutação) - Centro de Informática, ; Coorientador: Alexandre Cabral Mota;
Geração Automática de Casos de Teste a Partir de Especificações CSP; 2006; Dissertação (Mestrado em Programa de Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Coorientador: Alexandre Cabral Mota;
Rigorous Development with UML-RT; 2005; 107 f; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Coorientador: Alexandre Cabral Mota;
Efficient and Mechanised Analysis of Infinite CSPz Specifications: Strategy and Tool Support; 2003; Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Coorientador: Alexandre Cabral Mota;
Validating Transformations of OO programs using the Alloy Analyzer; 2017; Tese (Doutorado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco, ; Coorientador: Alexandre Cabral Mota;
An Algebra of Temporal Faults; 2017; Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco; Orientador: Alexandre Cabral Mota;
Síntese de software; 2015; Tese (Doutorado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco, ; Coorientador: Alexandre Cabral Mota;
Test Generation and Compositional Conformance Verification from Input-Output CSP Models; 2012; Tese (Doutorado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Coorientador: Alexandre Cabral Mota;
Evaluation of GUI Testing Techniques for System Crashing: From Real to Model-based Controlled Experiments; 2010; 0 f; Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Alexandre Cabral Mota;
Abstraction of Infinite and Communicating CSPz Processes; 2009; 0 f; Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco, ; Orientador: Alexandre Cabral Mota;
Do PDS-BC para o PDLPS-BC: Linhas de Produto de Software no BACEN; 2006; Monografia; (Aperfeiçoamento/Especialização em Gestão da Tecnologia da Informação) - Centro de Informática; Orientador: Alexandre Cabral Mota;
Utilização de MDA para geração automática de artefatos do PDS-BC; 2006; Monografia; (Aperfeiçoamento/Especialização em Gestão da Tecnologia da Informação) - Centro de Informática; Orientador: Alexandre Cabral Mota;
GUIA PARA ESPECIFICAÇÃO DE REQUISITOS; 2006; Monografia; (Aperfeiçoamento/Especialização em Gestão da Tecnologia da Informação) - Centro de Informática; Orientador: Alexandre Cabral Mota;
AUTOMATIC EXTRACTION OF MOBILE BEHAVIOUR FOR UNIFIED PROCESSING OF INDEPENDENT PHONE MODELS; 2005; 61 f; Monografia; (Aperfeiçoamento/Especialização em Curso de Imersão Em Testes) - Convênio Cin Motorola; Orientador: Alexandre Cabral Mota;
1; 5 periódicos e 6 artigos de conferência publicados de 2018 a 2021 (com 3 artigos de periódicos aceitos para publicação);; 2017; Trabalho de Conclusão de Curso; (Graduação em Ciência da Computação) - Universidade Federal de Pernambuco; Orientador: Alexandre Cabral Mota;
Uma ferramenta para geração de modelos Prism a partir de modelos Simulink; 2010; Trabalho de Conclusão de Curso; (Graduação em Ciência da Computação) - Universidade Federal de Pernambuco; Orientador: Alexandre Cabral Mota;
Automatic Z Data Refinement; 2006; Trabalho de Conclusão de Curso; (Graduação em Ciência da Computação) - Centro de Informática; Orientador: Alexandre Cabral Mota;
FormalDev: Tool support for generating UML-RT diagrams from CSP specifications; 2006; Trabalho de Conclusão de Curso; (Graduação em Ciência da Computação) - Centro de Informática; Orientador: Alexandre Cabral Mota;
Verificando Refatorações Automaticamente; 2006; Trabalho de Conclusão de Curso; (Graduação em Ciência da Computação) - Centro de Informática; Orientador: Alexandre Cabral Mota;
Transformação de programas Java seqüenciais em concorrentes; 2005; 67 f; Trabalho de Conclusão de Curso; (Graduação em Ciência da Computação) - Fundação Ford; Orientador: Alexandre Cabral Mota;
Repositório de Design Patterns para Desenvolvedores; 2005; 124 f; Trabalho de Conclusão de Curso; (Graduação em Ciência da Computação) - Fundação Ford; Orientador: Alexandre Cabral Mota;
Integrando UML e Métodos Formais; 2004; 95 f; Trabalho de Conclusão de Curso; (Graduação em Ciências da Computação) - Universidade Federal de Pernambuco; Orientador: Alexandre Cabral Mota;
AETing++: Automated systematic exploratory testing; 2020; Iniciação Científica; (Graduando em Ciência da Computação) - Universidade Federal de Pernambuco, Fundação de Apoio ao Desenvolvimento da Universidade Federal de Pernambuco; Orientador: Alexandre Cabral Mota;
Análise e Execução de iRobot Create a partir de Análises em CSP e PRISM; 2017; Iniciação Científica; (Graduando em Engenharia da Computação) - Universidade Federal de Pernambuco; Orientador: Alexandre Cabral Mota;
Desenvolvimento de verificador de modelos em K; 2016; Iniciação Científica; (Graduando em Ciência da Computação) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico; Orientador: Alexandre Cabral Mota;
Determinação e Monitoramento de Cobertura de Código Android para Componentes; 2016; Iniciação Científica; (Graduando em Ciência da Computação) - Universidade Federal de Pernambuco; Orientador: Alexandre Cabral Mota;
Determinação e Monitoramento de Cobertura de Código Android para Plataforma; 2016; Iniciação Científica; (Graduando em Ciência da Computação) - Universidade Federal de Pernambuco; Orientador: Alexandre Cabral Mota;
Produções bibliográficas
-
Mota, Alexandre ; VILLARIM, MANOEL ; IYODA, JULIANO ; CORNÉLIO, MÁRCIO . Comparative Analysis of Hoare Logic-Based Formal Verification Tools for Solidity Smart Contracts. JOURNAL OF SOFTWARE ENGINEERING RESEARCH AND DEVELOPMENT , v. 13, p. 277-293, 2025.
-
CORREIA, ALEXANDRE R. S. ; IYODA, JULIANO M. ; MOTA, ALEXANDRE C. . The effect of distance metrics in a general purpose synthesizer of imperative programs: A second empirical study using enlarged search spaces. SOFTWARE-PRACTICE & EXPERIENCE , v. 54, p. 528-540, 2024.
-
REIS, JACINTO ; Mota, Alexandre . Improving Android app exploratory testing with UI test cases using code change analysis. INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING (PRINT) , v. 1, p. 1, 2024.
-
Magalhães, C. ; MOTA, A. ; MOTA, A. ; Momenté, L. . UI Test case prioritization on an industrial setting: A search for the best criteria. SOFTWARE QUALITY JOURNAL (ONLINE) , v. 1, p. 1, 2021.
-
CORREIA, ALEXANDRE R. S. ; IYODA, JULIANO M. ; MOTA, ALEXANDRE C. . The effect of distance metrics in a general purpose synthesizer: An empirical study on integer domain imperative programs. SOFTWARE: PRACTICE AND EXPERIENCE , v. 1, p. 1-35, 2021.
-
CORREIA, ALEXANDRE ; IYODA, JULIANO ; Mota, Alexandre . A family of multi-concept program synthesisers in Alloy-. SCIENCE OF COMPUTER PROGRAMMING , v. 201, p. 102536, 2021.
-
MAGALHÃES, CLAUDIO ; ANDRADE, JOÃO ; PERRUSI, LUCAS ; Mota, Alexandre ; BARROS, FLÁVIA ; MAIA, ELIOT . HSP: A hybrid selection and prioritisation of regression test cases based on information retrieval and code coverage applied on an industrial case study. JOURNAL OF SYSTEMS AND SOFTWARE , v. 159, p. 110430, 2020.
-
CORREIA, ALEXANDRE ; IYODA, JULIANO ; Mota, Alexandre . Combining model finder and genetic programming into a general purpose automatic program synthesizer. INFORMATION PROCESSING LETTERS , v. 154, p. 105866, 2020.
-
REIS, J. ; MOTA, A. ; MOTA, A. . Aiding exploratory testing with pruned GUI models. INFORMATION PROCESSING LETTERS , v. 133, p. 49-55, 2018.
-
OLIVEIRA, M. V. M. ; ANTONINO, P. ; RAMOS, R. ; SAMPAIO, A. C. A. ; MOTA, A. ; ROSCOE, A. W. . Rigorous development of component-based systems using component metadata and patterns. Formal Aspects of Computing , v. 1, p. 1-68, 2016.
-
Mota, Alexandre ; IYODA, JULIANO ; MARANHÃO, HEITOR . Program Synthesis by Model Finding. Information Processing Letters (Print) , v. 1, p. 1, 2016.
-
Didier, André ; Mota, Alexandre . An algebra of temporal faults. Information Systems Frontiers (Print) , v. 1, p. 1, 2016.
-
MOTA, A. ; FARIAS, A. ; WOODCOCK, J. ; LARSEN, P. G. . Model checking CML: tool development and industrial applications. Formal Aspects of Computing , v. 27, p. 975-1001, 2015.
-
CARVALHO, GUSTAVO ; Digo Falcão ; F. Barros ; SAMPAIO, A. C. A. ; MOTA, A. ; MOTTA, LEONARDO ; BLACKBURN, MARK . NAT2TEST$_{SCR}$: Test case generation from natural language requirements based on SCR specifications. Science of Computer Programming (Print) , v. 95, p. 275-297, 2014.
-
SAMPAIO, A. C. A. ; Nogueira, Sidney ; MOTA, A. ; ISOBE, YOSHINAO . Sound and mechanised compositional verification of input-output conformance. Software Testing, Verification & Reliability , v. 24, p. 289-319, 2014.
-
MOTA, A. ; REBÊLO, Henrique ; LIMA, R. M. F. ; KULESZA, U. ; RIBEIRO, Márcio ; Yuanfang Cai ; COELHO, R. S. ; SANT`ANNA, Cláudio . QUANTIFYING THE EFFECTS OF ASPECTUAL DECOMPOSITIONS ON DESIGN BY CONTRACT MODULARIZATION: A MAINTENANCE STUDY. International Journal of Software Engineering and Knowledge Engineering , v. 23, p. 913-941, 2013.
-
REBÊLO, Henrique ; LIMA, RICARDO ; LEAVENS, GARY T. ; CORNÉLIO, MÁRCIO ; Mota, Alexandre ; OLIVEIRA, CÉSAR . Optimizing generated aspect-oriented assertion checking code for JML using program transformations: An empirical study. Science of Computer Programming (Print) , v. 78, p. 1137-1156, 2013.
-
Gomes, Adriano ; MOTA, A. ; SAMPAIO, A. C. A. ; Ferri, Felipe ; Watanabe, Edson . Constructive model-based analysis for safety assessment. International Journal on Software Tools for Technology Transfer (Internet) , v. 1, p. 1-30, 2012.
-
NOGUEIRA, SIDNEY ; Sampaio, Augusto ; Mota, Alexandre . Test generation from state based use case models. Formal Aspects of Computing , v. 26, p. 441-490, 2012.
-
BARBOSA, R. ; COSTA, A. ; TEDESCO, P. ; MOTA, A. ; MOTA, A. . Usando CSP, RSL e o Modelo PopOrg na Especificação Formal de Organizações de SMAs. Revista de Informática Teórica e Aplicada (Impresso) , v. 13, p. 389-411, 2011.
-
Ramos, Rodrigo ; Sampaio, Augusto ; Mota, Alexandre . Conformance notions for the coordination of interaction components. Science of Computer Programming (Print) , v. 75, p. 350-373, 2010.
-
Duarte, Rafael ; Mota, Alexandre ; Sampaio, Augusto . Introducing concurrency in sequential Java via laws. Information Processing Letters (Print) , v. 111, p. 129-134, 2010.
-
Didier, André ; Farias, Adalberto ; Mota, Alexandre . Checking Z Data Refinements Using Traces Refinement. Electronic Notes in Theoretical Computer Science , v. 240, p. 129-148, 2009.
-
MOTA, A. ; FARIAS, A. ; SAMPAIO, A. . Compositional abstraction ofCSP Z processes. Journal of the Brazilian Computer Society (Impresso) , v. 14, p. 23-44, 2008.
-
SOUZA, C. ; PERES, G. ; MOTA, A. . Unificando Modelos de Casos de Teste e de Requisitos. Revista IEEE América Latina , v. 6, p. 267-274, 2008.
-
BERTOLINI, C. ; MOTA, A. . Uma Estratégia para teste de Conformidade Automático em Sistemas Embarcados (Qualis C). Revista IEEE América Latina , v. 6, p. 290-297, 2008.
-
FEITOSA, CLELIO ; PERES, GLAUCIA ; Mota, Alexandre . IDEAS05: Unifying Models of Test Cases and Requirements. Revista IEEE América Latina , v. 6, p. 267-274, 2008.
-
FERREIRA, PATRÍCIA ; Sampaio, Augusto ; Mota, Alexandre . Viewing CSP Specifications with UML-RT Diagrams. Electronic Notes in Theoretical Computer Science , v. 195, p. 57-74, 2008.
-
BORGES, R. ; MOTA, A. . Integrating UML and Formal Methods. Electronic Notes in Theoretical Computer Science , v. 184, p. 97-112, 2007.
-
MACHADO, P. ; SILVA, D. ; MOTA, A. . Towards Property Oriented Testing. Electronic Notes in Theoretical Computer Science , v. 184, p. 3-19, 2007.
-
SAMPAIO, A. ; MOTA, A. ; RAMOS, R. . Class and Capsule Refinement in UML for Real Time. Electronic Notes in Theoretical Computer Science , Campina Grande, Brazil, v. 95, p. 23-51, 2004.
-
MOTA, A. ; SAMPAIO, A. . Model-checking CSP-Z: strategy, tool support and industrial application. Science of Computer Programming (Print) , v. 40, p. 59-96, 2001.
-
Woodcock, Jim ; Foster, Simon ; Mota, Alexandre ; Ye, Kangfeng . RoboStar Technology: Modelling Uncertainty in RoboChart Using Probability. Software Engineering for Robotics. 1ed.: Springer International Publishing, 2021, v. , p. 413-465.
-
Woodcock, Jim ; Cavalcanti, Ana ; Foster, Simon ; Mota, Alexandre ; Ye, Kangfeng . Probabilistic Semantics for RoboChart. Probabilistic Semantics for RoboChart. 1ed.: Springer International Publishing, 2019, v. , p. 80-105.
-
SILVA, ROBSON ; Mota, Alexandre ; STARR, RODRIGO RIZZI . Formal MDE-Based Tool Development. Advances in Intelligent Systems and Computing. 1ed.: Springer International Publishing, 2014, v. , p. 105-125.
-
CARVALHO, GUSTAVO ; Sampaio, Augusto ; MOTA, A. ; MOTA, A. ; BARROS, FLÁVIA . NAT2TEST: from Natural Language Requirements to Test Cases. Aerospace America Magazine, p. 45 - 45.
-
DA COSTA, DANIEL C. ; PRUDÊNCIO, RICARDO ; Mota, Alexandre . Assessor Models with a Reject Option for Soccer Result Prediction. In: 2023 International Conference on Machine Learning and Applications (ICMLA), 2023, Jacksonville. 2023 International Conference on Machine Learning and Applications (ICMLA), 2023. p. 1200.
-
NASCIMENTO, LIDIA PERSIDE GOMES ; PRUDÊNCIO, RICARDO BASTOS CAVALCANTE ; MOTA, ALEXANDRE CABRAL ; FILHO, AUDIR DE ARAUJO PAIVA ; CRUZ, PEDRO HENRIQUE ALVES ; OLIVEIRA, DANIEL CARDOSO COELHO ALVES DE ; MOREIRA, PEDRO RONCOLI SARMET . Machine Learning Techniques for Escaped Defect Analysis in Software Testing. In: SAST 2023: 8th Brazilian Symposium on Systematic and Automated Software Testing, 2023, Campo Grande. 8th Brazilian Symposium on Systematic and Automated Software Testing. New York: ACM, 2023. p. 47.
-
Lima, C. ; F. Barros ; MOTA, A. ; MOTA, A. ; Santos, I. . SPt: a text mining process to extract relevant areas from SW documents to exploratory tests. In: Brazilian Conference on Intelligent Systems, 2018, São Paulo. 7th Brazilian Conference on Intelligent Systems (BRACIS), 2018. v. 1. p. 1.
-
Araújo, R. ; MOTA, A. ; MOTA, A. ; NOGUEIRA, S. . Analyzing Cleaning Robots using Probabilistic Model Checking. In: Theory and Application of Reuse, Integration, and Data Science (Book Chapter), 2018, Springer International Publish. Theory and Application of Reuse, Integration, and Data Science, 2018. v. 838.
-
MOTA, A. ; MOTA, A. ; The Pragmatic Dimension of Formal Methods: Towards Building a Sound Synthesiser. In: Brazilian Symposium on Formal Methods (DOI: 10.1007/978-3-030-03044-5), 2018, Salvador. Lecture Notes in Computer Science. Switzerland: Springer International Publishing, 2018. v. 11254. p. 1-4.
-
CONSERVA FILHO, M. ; Marinho, R. ; MOTA, A. ; MOTA, A. ; Woodcock, Jim . Analysing RoboChart with Probabilities. In: Brazilian Symposium on Formal Methods, 2018. Lecture Notes in Computer Science, 2018. v. 11254. p. 198-214.
-
ARAUJO, RAFAEL PEREIRA DE ; MOTA, ALEXANDRE CABRAL ; NOGUEIRA, SIDNEY DE CARVALHO . Probabilistic Analysis Applied to Cleaning Robots. In: 2017 IEEE International Conference on Information Reuse and Integration (IRI), 2017, San Diego. 2017 IEEE International Conference on Information Reuse and Integration (IRI), 2017. p. 275.
-
MAGALHÃES, CLAUDIO ; ANDRADE, JOÃO ; PERRUSI, LUCAS ; Mota, Alexandre . Evaluating an Automatic Text-based Test Case Selection using a Non-Instrumented Code Coverage Analysis. In: the 2nd Brazilian Symposium, 2017, Fortaleza. Proceedings of the 2nd Brazilian Symposium on Systematic and Automated Software Testing - SAST. New York: ACM Press, 2017. p. 1.
-
MAGALHÃES, CLÁUDIO ; BARROS, FLÁVIA ; Mota, Alexandre ; MAIA, ELIOT . Automatic Selection of Test Cases for Regression Testing. In: the 1st Brazilian Symposium, 2016, Maringa. Proceedings of the 1st Brazilian Symposium on Systematic and Automated Software Testing - SAST. New York: ACM Press, 2016. p. 1.
-
Dias, T. ; Sampaio, Augusto ; MOTA, A. ; MOTA, A. . Verifying Transformations of Java Programs Using Alloy. In: Brazilian Symposium on Formal Methods, 2016. Lecture Notes in Computer Science, 2016. v. 9526. p. 110-126.
-
Barza, Sérgio ; CARVALHO, GUSTAVO ; IYODA, j. ; Sampaio, Augusto ; MOTA, A. ; MOTA, A. ; BARROS, FLÁVIA . Model Checking Requirements. In: Brazilian Symposium on Formal Methods, 2016. Lecture Notes in Computer Science, 2016. v. 10090. p. 217-234.
-
NOGUEIRA, SIDNEY ; Falcão, Taciana Pontual ; MOTA, A. ; MOTA, A. ; Oliveira, Emanuel ; Pereira, Iverson . An Approach for Verifying Educational Robots. In: Brazilian Symposium on Formal Methods, 2016. Lecture Notes in Computer Science, 2016. v. 10090. p. 59-77.
-
DIDIER, ANDRE LUIS RIBEIRO ; Mota, Alexandre . A Lattice-Based Representation of Temporal Failures. In: 2015 IEEE International Conference on Information Reuse and Integration (IRI), 2015, San Francisco. 2015 IEEE International Conference on Information Reuse and Integration, 2015. p. 295.
-
MOTA, A. ; MOTA, A. ; Farias, Adalberto ; DIDIER, ANDRE ; Woodcock, Jim . Rapid Prototyping of a Semantically Well Founded Circus Model Checker. In: Software Engineering and Formal Methods (SEFM 2014), 2014. Lecture Notes in Computer Science, 2014. v. 8702. p. 235-249.
-
ANDREWS, ZOE ; PAYNE, RICHARD ; ROMANOVSKY, ALEXANDER ; DIDIER, ANDRE ; Mota, Alexandre . Model-based development of fault tolerant systems of systems. In: 2013 7th Annual IEEE Systems Conference (SysCon), 2013, Orlando. 2013 IEEE International Systems Conference (SysCon). p. 356.
-
SILVA, ROBSON ; Mota, Alexandre ; STARR, RODRIGO RIZZI . Creating GUI-based DSL formal tools. In: 2013 IEEE 14th International Conference on Information Reuse & Integration (IRI), 2013, San Francisco. 2013 IEEE 14th International Conference on Information Reuse & Integration (IRI). p. 520-527.
-
Cavalcanti, Ana ; MOTA, A. ; MOTA, A. ; Woodcock, Jim . Simulink Timed Models for Program Verification. In: Theories of Programming and Formal Methods, 2013. Lecture Notes in Computer Science, 2013. v. 8051. p. 82-99.
-
CARVALHO, GUSTAVO ; Sampaio, Augusto ; MOTA, A. ; MOTA, A. . A CSP Timed Input-Output Relation and a Strategy for Mechanised Conformance Verification. In: International Conference on Formal Engineering Methods (ICFEM 2013), 2013. Lecture Notes in Computer Science, 2013. v. 8144. p. 148-164.
-
CARVALHO, GUSTAVO ; FALCÃO, DIOGO ; MOTA, A. ; MOTA, A. ; Sampaio, Augusto . A Process Algebra Based Strategy for Generating Test Vectors from SCR Specifications. In: Brazilian Symposium on Formal Methods, 2012. Lecture Notes on Computer Science, 2012. v. 7498. p. 67-82.
-
DIDIER, ANDRE ; MOTA, A. ; MOTA, A. . Identifying Hardware Failures Systematically. In: Brazilian Symposium on Formal Methods, 2012. Lecture Notes on Computer Science, 2012. v. 7498. p. 115-130.
-
REBÊLO, H. ; LIMA, R. ; Kuleska, U. ; Santanna, C. ; Coelho, R. ; MOTA, A. ; MOTA, A. ; Ribeiro, M. . Assessing the Impact of Aspects on Design By Contract Effort: A Quantitative Study. In: International Conference on Software Engineering and Knowledge Engineering, 2011, Miami. 23rd International Conference on Software Engineering and Knowledge Engineering (SEKE 2011), 2011.
-
REBÊLO, Henrique ; COELHO, ROBERTA ; LIMA, RICARDO ; LEAVENS, GARY T. ; HUISMAN, MARIEKE ; Mota, Alexandre ; CASTOR, FERNANDO . On the interplay of exception handling and design by contract. In: the 13th Workshop, 2011, Lancaster. Proceedings of the 13th Workshop on Formal Techniues for Java-Like Programs - FTfJP '11. New York: ACM Press. p. 1.
-
ARAÚJO, JOSÉ ELIAS ; REBÊLO, Henrique ; LIMA, RICARDO ; Mota, Alexandre ; KULESZA, UIRÁ ; SANT'ANNA, CLÁUDIO . An annotation-based approach for JCSP concurrent programming. In: the 1st workshop, 2011, Porto de Galinhas. Proceedings of the 1st workshop on Modularity in systems software - MISS '11. New York: ACM Press. p. 7.
-
Carvalho, G. ; Dias, T. ; MOTA, A. ; MOTA, A. ; SAMPAIO, A. . Analytical Comparison of Refinement Checkers. In: Brazilian Symposium on Formal Methods, 2011, São Paulo. 14th Brazilian Symposium on Formal Methods, Short Papers Proceedings, 2011. p. 61-66.
-
Jesus, Joabe ; MOTA, A. ; MOTA, A. ; Sampaio, Augusto ; Grijo, Luiz . Architectural Verification of Control Systems Using CSP. In: International Conference on Formal Methods (ICFEM), 2011. Lecture Notes in Computer Science, 2011. v. 6991. p. 323-339.
-
MOTA, A. ; JESUS, J. ; GOMES, A. ; FERRI, F. ; WATANABE, E. . Evolving a Safe System Design Iteratively. In: The 29th International Conference on Computer Safety, Reliability and Security, 2010, Viena. The 29th International Conference on Computer Safety, Reliability and Security, 2010. v. 6351. p. 361-374.
-
BERTOLINI, CRISTIANO ; Mota, Alexandre ; ARANHA, EDUARDO ; FERRAZ, CRISTIANO . GUI Testing Techniques Evaluation by Designed Experiments. In: , 2010, Paris. . p. 235-244.
-
BERTOLINI, C. ; MOTA, A. ; ARANHA, E. . Calibrating Probabilistic GUI Testing Models Based on Experiments and Survival Analysis. In: International Symposium on Software Reliability Engineering, 2010, San Jose. Proceedings of the 21th International Symposium on Software Reliability Engineering (ISSRE), 2010. p. 319-328.
-
REBÊLO, H. ; LIMA, R. ; Kuleska, U. ; Coelho, R. ; MOTA, A. ; MOTA, A. ; Ribeiro, M. . The Contract Enforcement Aspect Pattern. In: SugarLoafPLop, 2010, Salvador. VIII Latin American Conference on Pattern Languages of Programming, 2010. p. 99-114.
-
Gomes, Adriano ; MOTA, A. ; MOTA, A. ; Sampaio, Augusto ; Ferri, Felipe ; Buzzi, Julio . Systematic Model-Based Safety Assessment Via Probabilistic Model Checking. In: International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, 2010. Lecture Notes in Computer Science, 2010. v. 6415. p. 625-639.
-
REBÊLO, H. ; LIMA, R. ; CORNÉLIO, M. ; LEAVENS, G. ; MOTA, A. ; OLIVEIRA, C. . Optimizing JML Features Compilation in Ajmlc Using Aspect-Oriented Refactorings. In: Simpósio Brasileiro de Linguagens de Programação, 2009, Gramado. SBLP - XIII Simpósio Brasileiro de Linguagens de Programação, 2009. p. 117-130.
-
BERTOLINI, CRISTIANO ; Mota, Alexandre . Using Probabilistic Model Checking to Evaluate GUI Testing Techniques. In: , 2009, Hanoi. . p. 115-124.
-
BERTOLINI, CRISTIANO ; PERES, GLAUCIA ; D'AMORIM, MARCELO ; Mota, Alexandre . An Empirical Evaluation of Automated Black Box Testing Techniques for Crashing GUIs. In: 2009 International Conference on Software Testing Verification and Validation (ICST), 2009, Denver. 2009 International Conference on Software Testing Verification and Validation, 2009. p. 21.
-
Damasceno, Adriana ; Farias, Adalberto ; MOTA, A. ; MOTA, A. . A Mechanized Strategy for Safe Abstraction of CSP Specifications. In: Brazilian Symposium on Formal Methods, 2009. Lecture Notes in Computer Science, 2009. v. 5902. p. 118-133.
-
Sampaio, Augusto ; NOGUEIRA, SIDNEY ; MOTA, A. ; MOTA, A. . Compositional Verification of Input-Output Conformance via CSP Refinement Checking. In: International Conference on Formal Methods (ICFEM), 2009. Lecture Notes in Computer Science, 2009. v. 5885. p. 20-48.
-
Kaufman, Renata ; Sampaio, Augusto ; MOTA, A. ; MOTA, A. . Formalisation and Analysis of Objects as CSP Processes. In: Brazilian Symposium on Formal Methods, 2009. Lecture Notes in Computer Science, 2009. v. 5902. p. 236-250.
-
Ramos, Rodrigo ; Sampaio, Augusto ; MOTA, A. ; MOTA, A. . Systematic Development of Trustworthy Component Systems. In: International Symposium on Formal Methods (FM), 2009. Lecture Notes in Computer Science, 2009. v. 5850. p. 140-156.
-
BERTOLINI, C. ; MOTA, A. . Using Refinement Checking as System Testing. In: XI Iberoamerican Workshop on Requirements Engineering and Software Environments, 2008, Recife. IDEAS 2008, 2008. p. 17-30.
-
Ramos, Rodrigo ; Sampaio, Augusto ; Mota, Alexandre . Framework composition conformance via refinement checking. In: the 2008 ACM symposium, 2008, Fortaleza. Proceedings of the 2008 ACM symposium on Applied computing - SAC '08. New York: ACM Press. p. 119.
-
NOGUEIRA, S. ; SAMPAIO, A. ; MOTA, A. . Guided Test Generation from CSP Models. In: ICTAC - International Colloquium on Theoretical Aspects of Computing, 2008, Istanbul. 5th International Colloquium on Theoretical Aspects of Computing, 2008. p. 258-273.
-
PERES, G. ; MOTA, A. . A Tool to Translate CSP Models into English Requirements. In: II Encontro Brasileiro de Teste de Software, 2007, Recife. Encontro Brasileiro de Teste de Software, 2007.
-
FERREIRA, P. ; SAMPAIO, A. ; MOTA, A. . Viewing CSP specifications with UML-RT diagrams. In: Simpósio Brasileiro de Métodos Formais, 2006, Porto Alegre. SBMF - Simpósio Brasileiro de Métodos Formais, 2006. p. 73-88.
-
RAMOS, R. ; Sampaio, Augusto ; MOTA, A. ; MOTA, A. . Transformation Laws for UML-RT. In: International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS), 2006. Lecture Notes in Computer Science, 2009. v. 4037. p. 123-137.
-
BORGES, R. ; MOTA, A. . Integrando UML e Métodos Formais. In: Simpósio Brasileiro de Métodos Formais, 2005, Porto Alegre. Proceedings of the Brazilian Symposium on Formal Methods, 2005. p. 80-95.
-
COLE, L. ; BORBA, P. ; MOTA, A. . Proving aspect-oriented programming laws. In: Foundations of Aspect-Oriented Languages, 2005, Chicago. 4th Foundations of Aspect-Oriented Languages (FOAL), 2005. p. 1-10.
-
Ramos, Rodrigo ; Sampaio, Augusto ; MOTA, A. ; MOTA, A. . A Semantics for UML-RT Active Classes via Mapping into Circus. In: International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS), 2005. Lecture Notes in Computer Science, 2005. v. 3535. p. 99-114.
-
Farias, Adalberto ; MOTA, A. ; MOTA, A. ; Sampaio, Augusto . Efficient CSPZ Data Abstraction. In: International Conference on Integrated Formal Methods (IFM), 2004. Lecture Notes in Computer Science, 2004. v. 2999. p. 108-127.
-
MOTA, A. ; BORBA, P. ; SAMPAIO, A. . Mechanical Abstraction of CSPz Processes. In: FORMAL METHODS EUROPE, 2002, Copenhagem. FME 2002: Formal Methods - Getting IT Right, 2002. v. 2391. p. 163-183.
-
MOTA, A. ; FARIAS, A. ; SAMPAIO, A. . Efficient Analysis of Infinite CSPZ Processes. In: Workshop de Métodos Formais, 2002, Gramado. 5th Workshop on Formal Methods (WMF'02), 2002. p. 113-128.
-
MOTA, A. ; FARIAS, A. ; SAMPAIO, A. . De CSPz para CSPm: Uma ferramenta transformacional Java. In: Workshop de Métodos Formais, 2001, Rio de Janeiro. 4th Workshop on Formal Methods (WMF'01), 2001. p. 1-10.
-
MOTA, A. ; SAMPAIO, A. . Model Checking Processes with States: An Industrial Case Study. In: SIMPÓSIO BRASILEIRO DE ENGENHARIA DE SOFTWARE, 1998, MARINGÁ. XII SBES - SIMPÓSIO BRASILEIRO DE ENGENHARIA DE SOFTWARE, 1998. p. 23-36.
-
MOTA, A. ; SAMPAIO, A. . Model Checking CSPz. In: European Joint Conferences on the Theory and Practice of Software, 1998, Lisboa. Fundamental Approaches to Software Engineering, 1998. v. 1382. p. 205-220.
-
ARAÚJO, JOELSON ; ARAÚJO, JAEDSON ; MAGALHÃES, CLÁUDIO ; ANDRADE, JOÃO ; Mota, Alexandre . Feasibility of using Source Code Changes on the Selection of Text-based Regression Test Cases. In: the 2nd Brazilian Symposium, 2017, Fortaleza. Proceedings of the 2nd Brazilian Symposium on Systematic and Automated Software Testing - SAST, 2017. p. 1.
-
MAGALHÃES, CLÁUDIO ; Mota, Alexandre ; MAIA, ELIOT . Automatically Finding Hidden Industrial Criteria used in Test Selection. In: The 28th International Conference on Software Engineering and Knowledge Engineering, 2016. p. 470.
-
MOTA, A. ; MOTA, A. ; FARIAS, A. . Implementing an SMT-based Model Checker for CSP from its Operational Semantics. In: Simpósio Brasileiro de Métodos Formais, 2013, Brasília. Simpósio Brasileiro de Métodos Formais 2013, 2013.
-
Costa, M. ; MOTA, A. ; MOTA, A. . From SCR to SCADE. In: Simpósio Brasileiro de Métodos Formais, 2012, Natal. Simpósio Brasileiro de Métodos Formais, 2012. v. 1. p. 1-1.
-
BARBOSA, R. ; COSTA, A. ; TEDESCO, P. ; MOTA, A. . Using CSP in the Formal Specification of the Micro-Organizational Level of Multiagent Systems. In: AT2AI-7, 2010, Vienna. Seventh International Symposium "From Agent Theory to Agent Implementation", 2010.
-
ARAÚJO, J. ; REBÊLO, H. ; LIMA, R. ; MOTA, A. ; CASTOR, F. ; LIMA, T. ; LUCENA, J. ; LIMA, F. . AN ASPECT-BASED APPROACH FOR CONCURRENT PROGRAMMING USING CSP FEATURES. In: 5th International Conference on Software and Data Technologies, 2010, University of Piraeus. Proceedings of the 5th International Conference on Software and Data Technologies. p. 226.
-
MOTA, A. ; FARIAS, A. ; SAMPAIO, A. . A Support Tool for CSPZ Data Abstraction. In: FORMAL METHODS EUROPE, 2003, Pisa. FM 2003: the 12th International FME Symposium, 2003.
-
MOTA, A. ; SAMPAIO, A. ; BORBA, P. . Model Checking CSPz: Techniques to Overcome State Explosion. In: SOCIEDADE BRASILEIRA DE COMPUTAÇÃO, 2002, FLORIANÓPOLIS. XXII CONGRESSO DA SOCIEDADE BRASILEIRA DE COMPUTAÇÃO, 2002.
-
MOTA, A. ; MOTA, A. ; Aplicando Métodos Formais em Sistemas Aeronáuticos (Palestrante convidado - INPE). 2014. (Apresentação de Trabalho/Conferência ou palestra).
-
MOTA, A. ; MOTA, A. ; Palestrante convidado (Workshop de Métodos Formais na Embraer): An Introduction to the process algebra CSP and model checker FDR. 2009. (Apresentação de Trabalho/Conferência ou palestra).
-
MOTA, A. ; MOTA, A. ; YANG, F. ; TEIXEIRA, C. . Formally Verifying a Real World Smart Contract. Cornell University, 2023 (arXiv).
Outras produções
MOTA, A. ; MOTA, A. ; Magalhães, C. . AutoEDA: Ferramenta para Diagnose de Defeitos Escapados. 2020.
REIS, J. ; MOTA, A. ; MOTA, A. . ArcWizard: Identificador de Regiões da Interface de Celular Android associadas à Teste de Regressão. 2018.
ANDRADE, JOÃO ; PERRUSI, LUCAS ; MOTA, A. ; MOTA, A. . AutoTestCoverage: Identificador de Regiões de Aplicações a serem Testadas e seu Monitoramento. 2017.
Magalhães, C. ; ANDRADE, JOÃO ; MOTA, A. . AutoTestPlan: Seleção Automática de Casos de Testes baseada em Release Notes. 2016.
Araújo, R. ; MOTA, A. ; MOTA, A. . Gerador de Modelos Probabilísticos PRISM a partir de DSL-Robomind. 2015.
Santos, F. ; MOTA, A. ; MOTA, A. . Verificador de Modelos para Circus. 2015.
MARANHAO, H. P. ; MOTA, A. ; MOTA, A. . Sintetizador Automático de Programas em C. 2015.
MOTA, A. ; MOTA, A. ; FARIAS, A. . Verificador de Modelos para CML. 2014.
DIDIER, A. ; MOTA, A. ; MOTA, A. . Identificador automático de lógicas de falhas. 2012.
Costa, M. ; MOTA, A. ; MOTA, A. ; CORNÉLIO, MÁRCIO . Tradutor de requisitos em SCR para diagramas SCADE. 2012.
Gomes, Adriano ; WESLEY, D. ; MOTA, A. ; MOTA, A. . Extrator automático de modelos PRISM a partir de diagramas Simulink. 2011.
JESUS, J. ; MOTA, A. ; MOTA, A. ; Sampaio, Augusto . Extrator automático de modelos CSP a partir de diagramas Simulink. 2010.
MOTA, A. ; MOURA, A. . Simpósio Brasileiro de Métodos Formais. 2004. (Editoração/Anais).
MOTA, A. . Model Checking: Análise Automática de Software. 2003. (Curso de curta duração ministrado/Outra).
MOTA, A. . Model checking: provando propriedades automaticamente. 2003. (Curso de curta duração ministrado/Outra).
MOTA, A. ; MOTA, A. ; IFM 2012. 2012 (Membro do Comitê de Programa) .
MOTA, A. ; MOTA, A. ; UML & FM. 2012 (Membro do Comitê de Programa) .
MOTA, A. ; MOTA, A. ; SBPC. 2012 (Revisor de Artigo Técnico) .
MOTA, A. ; MOTA, A. ; ICFEM. 2012 (Membro do Comitê de Programa) .
MOTA, A. ; MOTA, A. ; SBMF. 2012 (Membro do Comitê de Programa) .
MOTA, A. ; MOTA, A. ; UML & FM. 2011 (Membro do Comitê de Programa) .
MOTA, A. ; MOTA, A. ; FM. 2011 (Revisor de Artigo Técnico) .
MOTA, A. ; MOTA, A. ; SBPC. 2011 (Revisor de Artigo Técnico) .
MOTA, A. ; MOTA, A. ; CBSOFT - Ferramentas. 2011 (Membro do Comitê de Programa) .
MOTA, A. ; MOTA, A. ; UML & FM. 2010 (Membro do Comitê de Programa) .
MOTA, A. ; MOTA, A. ; Simpósio Brasileiro de Métodos Formais. 2010 (Membro do Comitê de Programa) .
MOTA, A. ; MOTA, A. ; ICFEM 2010. 2010 (Revisor de Artigo Técnico) .
MOTA, A. ; MOTA, A. ; FACEPE (Artigos de Iniciação Científica). 2010 (Revisor de Artigo Técnico) .
MOTA, A. ; MOTA, A. ; ICST 2011. 2010 (Revisor de Artigo Técnico) .
MOTA, A. ; MOTA, A. ; UML & FM. 2009 (Membro do Comitê de Programa) .
MOTA, A. ; MOTA, A. ; Simpósio Brasileiro de Métodos Formais. 2009 (Membro do Comitê de Programa) .
MOTA, A. ; MOTA, A. ; FACEPE (Artigos de Iniciação Científica). 2009 (Revisor de Artigo Técnico) .
MOTA, A. ; MOTA, A. ; UML & FM. 2008 (Membro do Comitê de Programa) .
MOTA, A. ; MOTA, A. ; Simpósio Brasileiro de Métodos Formais. 2008 (Membro do Comitê de Programa) .
MOTA, A. ; MOTA, A. ; Simpósio Brasileiro de Métodos Formais. 2007 (Membro do Comitê de Programa) .
MOTA, A. . Simpósio Brasileiro de Métodos Formais. 2006 (Membro do Comitê de Programa) .
MOTA, A. . Sociedade Brasileira de Computação. 2006 (Membro da Comissão de Educação) .
MOTA, A. . Software Engineering and Formal Methods (SEFM). 2006 (Revisor de Artigo Técnico) .
MOTA, A. . Journal of the Brazilian Computer Society. 2006 (Revisor de Artigo Técnico) .
MOTA, A. . Simpósio Brasileiro de Métodos Formais. 2005 (Membro do Comitê de Programa) .
MOTA, A. . International Conference on Formal Engineering Methods. 2005 (Membro do Comitê de Programa) .
MOTA, A. . Simpósio Brasileiro de Engenharia de Software (Ferramentas). 2005 (Membro do Comitê de Programa) .
MOTA, A. . Simpósio Brasileiro de Métodos Formais. 2004 (Membro do Comitê de Programa) .
MOTA, A. . Simpósio Brasileiro de Métodos Formais. 2004 (Organizador Local) .
MOTA, A. . Simpósio Brasileiro de Engenharia de Software (Ferramentas). 2004 (Membro do Comitê de Programa) .
Projetos de pesquisa
-
2025 - Atual
Verificação Formal e Sugestão Automática de Propriedades em Contratos Inteligentes: Integrando LLMs e Preservacao Semântica, Descrição: Contratos inteligentes são programas autônomos executados em plataformas blockchain, cuja corretude e segurança são cruciais para garantir a integridade das aplicações descentralizadas. Este trabalho propõe o uso de técnicas de verificação formal como uma abordagem sistemática para assegurar a preser\-vação semântica em transformações aplicadas a contratos inteligentes, incluindo refatorações, otimizações e traduções entre linguagens. Além disso, exploramos o uso de modelos de linguagem de grande porte (LLMs) como ferramenta auxiliar para sugerir propriedades de segurança e comportamento esperados dos contratos, e propomos métodos formais para verificar a correção dessas sugestões. A abordagem visa combinar o poder expressivo das LLMs com a robustez das provas formais, promovendo maior confiança no desenvolvimento e evolução de contratos inteligentes.. , Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (1) . , Integrantes: Alexandre Cabral Mota - Integrante / Alexandre Mota - Coordenador / Márcio Cornélio - Integrante / Juliano Iyoda - Integrante / Manoel Felipe Araújo Villarim - Integrante.
-
2022 - 2025
Formalização de STPA: Uma Aplicação Industrial envolvendo Robôs, Celulares e Urnas Eletrônicas, Situação: Concluído; Natureza: Pesquisa. , Integrantes: Alexandre Cabral Mota - Integrante / Alexandre Mota - Coordenador / Marina Dioto - Integrante.
-
2021 - Atual
Residência em Robótica e Inteligência Artificial Aplicadas a Testes, Descrição: O projeto do Curso de Pós-Graduação Lato Sensu (Especialização) de Residência em Robótica e Inteligência Artificial Aplicadas a Testes de Software envolve três dimensões complementares e paralelas: (i) Capacitação; (ii) Inovação e Pesquisa; e (iii) Automação e Execução de Testes de Software. O projeto segue a filosofia de uma residência tecnológica (inspirada nas residências médicas). Existem dois ambientes para execução do projeto: a sala de aula e o laboratório. Os alunos têm dedicação exclusiva e, em meio turno, dedicam-se a assistir às aulas (i). No outro turno, realizam no laboratório atividades práticas de Inovação e Pesquisa (ii) e Automação e Execução de Testes de Software (iii). O curso capacita (na teoria e prática) os alunos em programação de braços robóticos e técnicas de inteligência artificial aplicadas a teste de software. Braços robóticos (adquiridos prontos no mercado---este projeto não engloba construção de robôs) são reprogramados para realizar testes de interface, que envolvem tanto interface gráfica como gestual (toques na tela, rotações e translações em dispositivos). Testes assim são usualmente executados por humanos. Inteligência artificial suporta a descoberta de defeitos de forma sistemática e preditiva. Tal modelo de residência provê ao aluno tanto capacitação teórica em sala de aula (pela manhã) quanto experiência de trabalho em atividades práticas de automação e execução de teste de software (pela tarde). Desafios de inovação e pesquisa na área de robótica e inteligência artificial aplicadas a teste de software são solucionados tanto pela equipe fixa do projeto (líder técnico e engenheiros) quanto pelos alunos em suas monografias. E, em adição às duas primeiras dimensões, as atividades práticas de automação e execução de teste de software utilizando robôs e técnicas de inteligência artificial completam a formação teórica dos alunos. Tal ambiente prático tem dois papéis: é onde os alunos ficam imersos durante um turno do dia vivenciando experiências de trabalho, e é o celeiro que tanto gera desafios de inovação e pesquisa quanto serve como laboratório onde tais soluções são testadas. Estas três dimensões constituem um ambiente integrado de atividades simultâneas de capacitação teórica e prática, inovação, pesquisa e desenvolvimento.. , Situação: Em andamento; Natureza: Pesquisa. , Integrantes: Alexandre Cabral Mota - Integrante / Alexandre Mota - Coordenador / Augusto Sampaio - Integrante.
-
2019 - 2024
Modelagem, Análise, Simulação e Implementação de Sistemas de Sistemas (SoS): Enxame de Robôs, Descrição: Este projeto visa criar uma metodologia sistemática e rigorosa para especificar, verificar, projetar e implementar aplicações sobre enxames de robôs. A ideia é construir sobre o projeto RoboCalc (https://www.cs.york.ac.uk/circus/RoboCalc/), já em desenvolvimento em York e liderado por Ana Cavalcanti. Atualmente, o projeto RoboCalc oferece os seguintes recursos: Uma notação baseada em máquina de estados (RoboChart) para modelar robôs individuais;Uma tradução do RoboChart para a álgebra de processos CSP que usa a ferramenta FDR (em segundo plano) para fins de análises funcionais (tanto de propriedades clássicas como deadlock e livelock, quanto propriedades específicas do domínio); eRoboTool, implementado como um plugin do Eclipse, para suportar a edição e análise do modelo, conforme descrito nos itens anteriores.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (3) / Mestrado acadêmico: (3) / Doutorado: (2) . , Integrantes: Alexandre Cabral Mota - Integrante / Alexandre Mota - Coordenador / Augusto Sampaio - Integrante / Márcio Cornélio - Integrante / Jones Oliveira de Albuquerque - Integrante / Juliano Iyoda - Integrante / Sidney Nogueira - Integrante / Gustavo Carvalho - Integrante / Lucas Albertins - Integrante / Jim Woodcock - Integrante / Ana Cavalcanti - Integrante / Madiel de Souza Conserva Filho - Integrante.
-
2019 - 2024
Análise de Confiabilidade para Sistemas Robóticos descritos em RoboChart, Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Mestrado acadêmico: (1) . , Integrantes: Alexandre Cabral Mota - Integrante / Alexandre Mota - Coordenador / Sidney Nogueira - Integrante / Jim Woodcock - Integrante / Madiel de Souza Conserva Filho - Integrante / Marina Dioto - Integrante.
-
2017 - Atual
RoboTIC@ - Information and Communication Technology for Robotics and Applications, Descrição: The main objective of this project is to create a systematic and rigorous methodology to specify, verify, design and implement robotic applications. It is one of the projects of INES (https://ines.org.br/) and is part of the RoboStar initiative (https://www.cs.york.ac.uk/RoboStar/). The focus is on the design of a graphical simulation language, RoboSim, and mapping models in RoboSim to several target platforms: Arduino, B and Simulink/Stateflow, among others. Development of the final implementations from the simulations is also in scope. Finally, we will also consider probabilistic models, modelling of the environment and the development of real world applications.. , Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (3) / Mestrado acadêmico: (4) / Doutorado: (4) . , Integrantes: Alexandre Cabral Mota - Integrante / Alexandre Mota - Integrante / Márcio Cornélio - Integrante / Jones Oliveira de Albuquerque - Integrante / Marcel Oliveira - Integrante / Juliano Iyoda - Integrante / Sidney Nogueira - Integrante / Augusto Cezar Alves Sampaio - Coordenador / Jim Woodcock - Integrante / Ana Cavalcanti - Integrante / Madiel de Souza Conserva Filho - Integrante / Thiérry Lecomte - Integrante.
-
2015 - Atual
Seleção Automática de Testes de Regressão para Dispositivos Móveis (Cooperação CIn-Motorola), Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (2) / Mestrado acadêmico: (6) / Doutorado: (5) . , Integrantes: Alexandre Cabral Mota - Integrante / Alexandre Mota - Coordenador / Augusto Sampaio - Integrante / Ricardo Bastos Cavalcante Prudêncio - Integrante / Flávia Barros - Integrante / Kelvin Lopes Dias - Integrante / Tsang Ing Ren - Integrante / Leopoldo Motta Teixeira - Integrante.
-
2015 - Atual
Processos de Testes de Dispositivos Móveis (Cooperação CIn-Motorola), Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (23) / Mestrado acadêmico: (10) / Doutorado: (4) . , Integrantes: Alexandre Cabral Mota - Integrante / Alexandre Mota - Coordenador / Carlos Alexandre de Barros Mello - Integrante / Abel Guilhermino da Silva Filho - Integrante / Eduardo Antonio Guimarães Tavares - Integrante / Kelvin Lopes Dias - Integrante / Paulo Romero Martins Maciel - Integrante / Ricardo Martins de Abreu e Silva - Integrante / Tsang Ing Ren - Integrante.
-
2014 - 2018
Verificação de Modelos com Estados Enriquecidos, Descrição: Neste projeto (o qual é apoiado pela Embraer), propomos a construção de um verificador automático de modelos (model checker) para uma linguagem formal,seguindo fielmente sua semântica operacional estruturada e que seja capaz de lidar com espaço de estados enriquecido com tipos de dados complexos, tais como conjuntos, sequências,bags, etc. (Tipos de dados provenientes da linguagem formal Z). O formalismo alvo deste projeto é a linguagem formal Circus, que integra a álgebra de processos CSP, para expressar os aspectos de dados e a linguagem de comandos guardados de Dijkstra. Tal combinação faz de Circus não apenas uma linguagem de especificação, mas também de programação. Circus é um formalismo adequado para descrever os vários aspectos do projeto de grandes sistemas, particularmente, com ênfase em Sistemas de Sistemas (SoS, Systems of Sytems).. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (1) / Mestrado acadêmico: (2) / Doutorado: (1) . , Integrantes: Alexandre Cabral Mota - Integrante / Alexandre Mota - Coordenador / Adalberto Farias - Integrante / Augusto Sampaio - Integrante / Juliano Iyoda - Integrante / André Didier - Integrante / Fabio Soares dos Santos - Integrante / Rafael Pereira de Araújo - Integrante., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro.
-
2012 - 2014
Desenvolvimento sistemático e rigoroso para sistemas aeronáuticos, Descrição: Este projeto objetiva empregar técnicas de teste, métodos formais e de análise de segurança em sistemas aeronáuticos. O principal desafio é promover avanços teórico-práticos para a indústria aeronáutica bem como as áreas de pesquisa associadas. Em particular, procuramos com este projeto permitir que sistemas aeronáuticos sejam desenvolvidos com ainda mais qualidade, onde corretude e segurança são os principais fatores envolvidos, não obstante requerendo um custo menor do que o empregado atualmente. A Embraer (Empresa Brasileira de Aeronáutica S.A.), visando satisfazer requisitos de desenvolvimento e certificação de sistemas, usa padrões sistemáticos e rigorosos como a FAR 25.1309 (Federal Aviation Regulations)[FAR25] e ARP 4754, 4761 (Aerospace Recommended Practice) [ARP4754, ARP4761]. Estes padrões definem guias para a produção de sistemas e equipamentos de aviação, os quais devem executar suas funções de acordo com o especificado (comportamento funcional ou nominal), tendo como resultado um nível de confiança em segurança (comportamento com falhas ou anormal) alto, tal qual requer o domínio aeronáutico. Desta forma, desde 2006 a Embraer vem manifestando interesse em colaborar com as pesquisas realizadas pelo proponente deste projeto (ver Anexo I) com o objetivo de diminuir o custo com o desenvolvimento de seus sistemas aeronáuticos e ao mesmo tempo aumentar a confiabilidade e segurança sobre os mesmos. Desde o início desta colaboração Universidade-Indústria, temos conseguido satisfazer a três maiores objetivos para a pesquisa brasileira (e mundial): (i) Publicar resultados científicos alcançados; (ii) Transferir tais resultados para a indústria como tecnologia; (iii) Formar capital humano qualificado. Este projeto considerará as seguintes direções de pesquisa: (1) definição de um cálogo de refatoramentos para introdução de tolerância a falhas; (2) investigação sobre a corretude dos refatoramentos deste catálogo; (3) experimentação dos refatoramentos em metodol. , Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Mestrado acadêmico: (2) Doutorado: (2) . , Integrantes: Alexandre Cabral Mota - Coordenador / Adalberto Farias - Integrante / Augusto Sampaio - Integrante / Juliano Iyoda - Integrante., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro.
-
2011 - 2014
COMPASS Comprehensive Modelling for Advanced Systems of Systems, Descrição: COMPASS will augment existing industry tools and practice with an underlying modelling language in which Systems of Systems (SoS) architectures and contracts can be expressed. A formal semantic foundation the first to be developed specifically for SoS engineering will enable this language to support analysis of global SoS properties. The language and methods will be supported by an open, extendible tools platform with integrated prototype plugins for model construction, dynamic analysis by simulation and test automation, static analysis by model checking and proof, and links to an established architectural modelling language (SysML). These strengthened foundations and tools will support enhanced methods guidelines that help users embed this new technology in industrial SoS practice. Technical advances in COMPASS are focussed on industry needs evaluated through substantial industry led case studies in three diverse and complementary areas. These will be augmented by challenge problems solicited from a range of SoS stakeholders and developer organisations through a special interest group. The open platform, tools plugins, semantics, development guidelines, industry case study experience and challenge problems will ensure that COMPASS‟s outputs can be readily exploited by SoS developers and stakeholders as well as in future research and development.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (1) / Mestrado acadêmico: (2) / Doutorado: (2) . , Integrantes: Alexandre Cabral Mota - Integrante / Adalberto Farias - Integrante / Márcio Cornélio - Integrante / Marcel Oliveira - Integrante / Juliano Iyoda - Integrante / André Didier - Integrante / Gustavo Carvalho - Integrante / Augusto Cezar Alves Sampaio - Coordenador / Lucas Albertins - Integrante / Jim Woodcock - Integrante / Ana Cavalcanti - Integrante., Financiador(es): Comunidade Européia - Cooperação.
-
2010 - 2012
Análise de Segurança Baseada em Modelos para Sistemas Autônomos, Descrição: O futuro da exploração espacial implica em sistemas ainda mais complexos. Percebe-se um esforço mundial em desenvolver dispositivos cada vez mais autônomos que não dependam apenas do controle humano remoto em terra para recuperar-se de eventuais falhas. Sendo assim, pode-se alcançar uma maior probabilidade de êxito na missão desde que o sistema autônomo seja confiável. A importância do desenvolvimento do controle de satélites artificiais tolerantes a falhas é evidente. Tomemos como exemplo os satélites que possuem uma curta janela de comunicação com a terra durante o período de uma órbita completa. Uma pequena falha no sistema que o levasse a não detectar o momento exato para transmitir seus dados resultaria na perda da telemetria e, consequentemente, no precoce fim da missão, mesmo que outros dispositivos ainda estivessem funcionando perfeitamente. Técnicas de simulações e testes estão bastante difundidas nesse setor para reduzir as probabilidades de falha. Apesar de úteis, elas não são completas, pois carregam consigo dois problemas básicos: ausência de garantia da corretude do funcionamento dos sistemas e alto custo para remodelá-los em caso de falhas encontradas tardiamente durante os testes. Com esse projeto estamos dispostos a aplicar técnicas de Métodos Formais e Análise de Segurança e Sistemas (associadas a linguagens de especificação formais e ferramentas de Model Checker) aos dispositivos críticos que compõem um satélite artificial. Sendo assim, seremos capazes de modelá-los matematicamente (quer sejam hardware ou software) sem a necessidade de qualquer implementação anterior. Implicando, assim, em um menor custo envolvido no processo. A partir de então, será possível extrair propriedades do sistema, detectar ambiguidades, imprecisões, incoerências, calcular a probabilidade de ocorrência de eventos indesejados e verificar todos os estados aos quais o sistema esta sujeito (garantindo, dessa forma, sua corretude). Tudo indica que essa abordagem ofere. , Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (1) / Mestrado acadêmico: (2) . , Integrantes: Alexandre Cabral Mota - Coordenador / Adalberto Farias - Integrante / Augusto Sampaio - Integrante / Juliano Iyoda - Integrante / Adriano Gomes - Integrante / Flávia Soares - Integrante / Luis Filipe - Integrante., Financiador(es): Agência Espacial Brasileira - Auxílio financeiro.
-
2010 - 2012
Análise de Segurança de Sistemas Aviônicos com Métodos Formais, Descrição: Este projeto tem como enfoque empregar técnicas de Métodos Formais e de Análise de Segurança de Sistemas em sistemas aeronáuticos. O principal objetivo é promover avanços teórico-práticos nestas áreas de pesquisa. Em particular, procuramos com este projeto permitir que sistemas aeronáuticos sejam desenvolvidos com ainda mais qualidade, onde corretude e segurança são os principais fatores envolvidos, entretanto requerendo um custo menor do que o empregado atualmente. Resumo A Embraer (Empresa Brasileira de Aeronáutica S.A.) tem utilizado como meio de cumprimento de requisitos de desenvolvimento e certificação de sistemas os padrões FAR 25.1309 (Federal Aviation Regulations)[FAR25] e ARP 4754, 4761 (Aerospace Recommended Practice) [ARP4754, ARP4761]. Esses padrões definem guias para a produção de sistemas e equipamentos de aviação, os quais que devem executar suas funções esperadas (comportamento nominal ou normal) com um nível de confiança em segurança (comportamento com falhas ou anormal) de acordo com os requisitos aeronáuticos determinados. Desta forma, a Embraer manifestou interesse em colaborar com o presente projeto de pesquisa (ver Anexo I) com o objetivo de diminuir o custo com o desenvolvimento de seus sistemas aeronáuticos e ao mesmo tempo aumentar a confiabilidade e segurança sobre os mesmos. Resumo O projeto considerará as seguintes direções de pesquisa: (1) investigação de notações formais para modelar sistemas aeronáuticos heterogêneos com características tais como não-determinismo, probabilidade e tempo; (2) proposta de uso de linguagens formais como semântica para diagramas de bloco, árvores de falhas, cadeias de markov, diagramas de influência e diagramas de seqüências de eventos; (3) emprego de verificação e validação formal de sistemas para a análise de propriedades funcionais, não-funcionais e/ou de segurança de sistemas aeronáuticos; (4) suporte para geração automática de modelos formais a partir de modelos de falhas de sistemas contínuos, discre. , Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (1) / Mestrado acadêmico: (2) . , Integrantes: Alexandre Cabral Mota - Coordenador / Adalberto Farias - Integrante / Augusto Sampaio - Integrante / Juliano Iyoda - Integrante / Adriano Gomes - Integrante / Flávia Soares - Integrante / Luis Filipe - Integrante., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro.
-
2007 - 2009
Combinando Tecnicas de Metodos Formais e Teste na Construcao de Sistemas Embarcados de Tempo Real, Descrição: O valor total do projeto: R$ 415.903,16, dividos nas seguintes rubricas: R$ 110.000,00 (custeio), R$ 85.800,00 (capital), R$ 220.103,16 (bolsas). O projeto envolve o CIn, a UFCG e a UFRN.. , Situação: Em andamento; Natureza: Pesquisa. , Integrantes: Alexandre Cabral Mota - Integrante / Augusto Sampaio - Integrante / Patrícia Duarte de Lima Machado - Integrante / David Boris Paul Déharbe - Coordenador / Anamaria Martins Moreira - Integrante / Marcel Oliveira - Integrante.
-
2006 - 2008
Uma Estratégia para Desenvolvimento Sistemático de Aplicações Críticas, Descrição: A Embraer (Empresa Brasileira de Aeronáutica S.A.) tem utilizado como meio de cumprimento de requisitos de certificação de software o padrão DO-178B [RTCA]. O padrão DO-178B define guias para a produção de software para sistemas e equipamentos de aviação que executam sua função esperada com um nível de confiança em segurança de acordo com os requisitos aeronáuticos. Desta forma, a Embraer manifestou interesse em colaborar com o presente projeto de pesquisa com o objetivo de evoluir de um ciclo de desenvolvimento V (onde várias atividades do desenvolvimento de sistemas é realizada ainda manualmente) para um ciclo de desenvolvimento Y (onde, exceto pelos requisitos do sistema, as demais atividades são realizadas automaticamente e com presença mínima de falhas). Assim sendo, seus requisitos precisam ser documentados formalmente, com propriedades verificadas, projeto e implementação gerados automaticamente e, finalmente, propriedades testadas diretamente a partir da implementação do sistema, para obter uma garantia adicional de que a implementação não sofreu qualquer distorção após considerar requisitos não-funcionais.. , Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (0) / Especialização: (0) / Mestrado acadêmico: (1) / Mestrado profissional: (0) / Doutorado: (1) . , Integrantes: Alexandre Cabral Mota - Coordenador / Adalberto Farias - Integrante / Augusto Sampaio - Integrante / Joabe Bezerra de Jesus Júnior - Integrante / Ana Lúcia Caneca Cavalcanti - Integrante., Financiador(es): Centro de Informática - Auxílio financeiro., Número de produções C, T & A: 1
-
2005 - 2008
Projeto Integrado de Avaliação, Seleção e Geração Automática de Casos de Teste, Descrição: A atividade de testes, pela própria natureza, objetiva identificar erros, mas, em geral, não garante a ausência de erros. A principal razão é que o número de cenários a considerar é, usualmente, infinito. Portanto, a comunidade científica, em cooperação com a indústria de TI, está sempre buscando o desenvolvimento de técnicas que contribuam para tornar a atividade de teste progressivamente mais efetiva. Os resultados têm impacto evidente na qualidade de produtos desenvolvidos, na produtividade das organizações envolvidas e, conseqüentemente, no custo de desenvolvimento. No contexto de uma cooperação já existente entre a Motorola do Brasil e o Centro de Informática (CIn) da UFPE, o objetivo mais amplo deste projeto é contribuir com todo o processo de testes da Motorola.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (0) / Especialização: (0) / Mestrado acadêmico: (10) / Mestrado profissional: (0) / Doutorado: (2) . , Integrantes: Alexandre Cabral Mota - Integrante / Augusto Sampaio - Integrante / Paulo Borba - Coordenador / Alexandre Vasconcelos - Integrante / Patrícia Duarte de Lima Machado - Integrante / André Santos - Integrante., Financiador(es): Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco - Bolsa.
-
2002 - 2006
Formal Methods and UML-RT Integration, Descrição: O objetivo geral deste projeto é integrar métodos semi-formais, usados para especificação e modelagem, e que possuem grande apelo prático, com métodos formais, que oferecem uma base matemática sólida complementar. Em particular, a notação gráfica UML [B99] (e sua extensão para tempo real, UML-RT [P99]) será uma linguagem de referência para o projeto, devido a sua ampla aceitação prática. A integração de UML-RT com métodos formais visa contribuir com um processo de desenvolvimento de software que permita a geração de artefatos (documentos) com semântica bem definida, ou seja, não-ambíguos, consistentes e precisos. Por outro lado, a integração visa difundir o uso de métodos formais na Indústria, encapsulando-os através dos diagramas de UML. Um dos requisitos centrais do processo integrado é flexibilidade: o desenvolvedor pode optar pelo grau de formalismo usado em seu projeto, podendo variar desde uma descrição puramente em UML até uma especificação completamente formal, para descrever tanto os aspectos estáticos quanto os dinâmicos da modelagem. O passo inicial do projeto proposto é a definição de uma linguagem de especificação formal capaz de capturar todos os elementos conceituais disponíveis em UML-RT, pois, do nosso conhecimento, não há, na literatura, um formalismo que integre objetos, concorrência e tempo real (elementos de UML-RT). Entretanto, ao invés de criar uma tal linguagem por completo, o objetivo é, novamente, utilizar princípios de integração de teorias e ferramentas [P99], com o propósito de definir uma linguagem de especificação formal através da combinação de outras já bem definidas e com comprovada aceitação pela Comunidade Científica. Em diversos trabalhos de pesquisa realizados anteriormente [MS01,MS02,SSC01,CW02,SWC02], obtivemos resultados interessantes com relação à integração, ortogonal e formal, de diversos aspectos envolvidos no processo de especificação, modelagem e análise de software. Em particular, estudamos a combinação de nota. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (0) / Especialização: (0) / Mestrado acadêmico: (4) / Mestrado profissional: (0) / Doutorado: (2) . , Integrantes: Alexandre Cabral Mota - Integrante / Augusto Sampaio - Coordenador / Ana Lúcia Caneca Cavalcanti - Integrante / James Charles Paul Woodcock - Integrante., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro., Número de produções C, T & A: 3
-
2002 - 2002
Derivação Automática de Aspectos a partir de Programa em Java, Descrição: Projeto consiste em analisar o código-fonte de um programa em Java e extrair semi-automaticamente aspectos relevantes sobre tal programa. A partir da internvenção de um usuário, a escolha por esses ou aqueles trechos de código se tornariam aspectos e assim o programa seria reescrito de forma a explorar os aspectos selecionados. A situação ideal é que os aspectos relevem características importantes sobre o software mas sejam ortogonais ao seu objetivo maior, ou seja, o software pode ser desenvolvido sem a preocupação de armazenamento em banco de dados. Tal parte poderia ser implantada como um aspecto do software.. , Situação: Desativado; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (2) / Especialização: (0) / Mestrado acadêmico: (0) / Mestrado profissional: (0) / Doutorado: (0) . , Integrantes: Alexandre Cabral Mota - Coordenador / George Fragoso - Integrante / Jonas Lima - Integrante., Financiador(es): Faculdade Integrada do Recife - Bolsa.
Prêmios
2025
Produtividade em Pesquisa (PQ-C), CNPq.
2025
Professor homenageado Formatura Engenharia da Computação 2024.2, UFPE.
2024
Professor homenageado Formatura Engenharia da Computação 2024.1, Universidade Federal de Pernambuco.
2024
Palestrante convidado do Simpósio de Inovação do Real Hospital Português, Real Hospital Português.
2021
Professor homenageado Formatura Engenharia da Computação 2020.2, Universidade Federal de Pernambuco.
2018
Palestrante convidado, Brazilian Symposium on Formal Methods.
2018
Produtividade em Pesquisa (Nível 2), CNPq.
2016
2o melhor artigo científico no Simpósio de Teste - SAST, Sociedade Brasileira de Computação.
2013
Melhor Docente do Curso de Residência em Software, Convênio CIn/Motorola.
2013
Produtividade em Desenvolvimento Tecnológico e Extensão Inovadora (Nível 2), CNPq.
2010
Produtividade em Desenvolvimento Tecnológico e Extensão Inovadora (Nível 2), CNPq.
2009
Best Paper Award para o artigo A Mechanyzed Strategy for Safe Abstraction of CSP Specifications, Simpósio Brasileiro de Métodos Formais - SBMF.
2002
1o Lugar no Concurso de Teses de Doutorado, Sociedade Brasileira de Computação.
Histórico profissional
Endereço profissional
-
Universidade Federal de Pernambuco, Centro de Informática, Departamento de Sistemas de Computação. , Avenida Jornalista Aníbal Fernandes, Cidade Universitária, 50740560 - Recife, PE - Brasil - Caixa-postal: 7851, Telefone: (81) 21268430, Ramal: 4336, Fax: (81) 21268438, URL da Homepage:
Experiência profissional
2011 - 2014
Comunidade EuropéiaVínculo: Colaborador, Enquadramento Funcional: Vice-coordenador no Brasil
2002 - 2002
Faculdade Integrada do RecifeVínculo: Funcionário, Enquadramento Funcional: Professor titular, Carga horária: 20
Outras informações:
Relacionado às atividades de ensino, ministrei cursos de Lógica e Compiladores. Participei do projeto de iniciação científica, como orientador de 2 alunos, lançado no período em que me encontrava nesta instituição.
Atividades
-
02/2002 - 06/2002
Ensino, Sistemas de Informação, Nível: GraduaçãoDisciplinas ministradas, Lógica para Computação, Teoria dos Compiladores
2019 - Atual
Universidade Federal de PernambucoVínculo: Servidor público, Enquadramento Funcional: Professor titular, Regime: Dedicação exclusiva.
2015 - Atual
Universidade Federal de PernambucoVínculo: Servidor público, Enquadramento Funcional: Professor Associado III, Regime: Dedicação exclusiva.
2002 - 2015
Universidade Federal de PernambucoVínculo: , Enquadramento Funcional: Professor Associado II, Carga horária: 40, Regime: Dedicação exclusiva.
2001 - 2002
Universidade Federal de PernambucoVínculo: Professor substituto, Enquadramento Funcional: Professor substituto, Carga horária: 20
Outras informações:
Professor Substituto
1998 - 1999
Universidade Federal de PernambucoVínculo: Bolsista DTI, Enquadramento Funcional: , Carga horária: 20
Atividades
-
08/2015
Ensino, Ciências da Computação, Nível: GraduaçãoDisciplinas ministradas, IF669 - Introdução à Programação (Curso: Engenharia da Computação)
-
07/2002
Ensino, Ciências da Computação, Nível: Pós-GraduaçãoDisciplinas ministradas, IN1112 - Especificação de Sistemas Distribuídos
-
06/2002
Pesquisa e desenvolvimento, Departamento de Sistemas de Computação, Departamento de Sistemas de Computação.Linhas de pesquisa
-
03/2015 - 08/2015
Ensino, Engenharia da Computação, Nível: GraduaçãoDisciplinas ministradas, IF669 - Introdução à Programação
-
03/2015 - 08/2015
Ensino, Ciências da Computação, Nível: Pós-GraduaçãoDisciplinas ministradas, IN1112 - Especificação de Sistemas Distribuídos
-
02/2001 - 06/2002
Ensino, Ciência da Computação (Professor Substituto), Nível: GraduaçãoDisciplinas ministradas, Linguagens de Programação, Métodos Formais
-
01/1998 - 01/1999
Outras atividades técnico-científicas , Centro de Informática, Centro de Informática.Atividade realizada, Implementação de um Simulador em Java.
Criando um monitoramento
Nossos robôs irão buscar nos nossos bancos de dados todos os processos de Alexandre Cabral Mota e sempre que o nome aparecer em publicações dos Diários Oficiais, avisaremos por e-mail e pelo painel do usuário
Criando um monitoramento
Nossos robôs irão buscar nos nossos bancos de dados todas as movimentações desse processo e sempre que o processo aparecer em publicações dos Diários Oficiais e nos Tribunais, avisaremos por e-mail e pelo painel do usuário
Confirma a exclusão?