Adalberto Cajueiro de Farias

Formação complementar

Idiomas

Áreas de atuação

Organização de eventos

Participação em eventos

Participação em bancas

Orientou

Produções bibliográficas

• MOTA, A. ; A. FARIAS ; WOODCOCK, J. ; LARSEN, P. G. . Model checking CML: tool development and industrial applications. Formal Aspects of Computing , v. 1, p. 1-35, 2015.

• DAMASCENO, A. ; A. FARIAS ; A. Mota . A Mechanized Strategy for Safe Abstraction of CSP Specifications. Lecture Notes in Computer Science , v. 5902, p. 118-133, 2009.

• Didier, André ; A. FARIAS ; MOTA, Alexandre . Checking Z Data Refinements Using Traces Refinement. Electronic Notes in Theoretical Computer Science , v. 240, p. 129-148, 2009.

• A. FARIAS ; A. Mota ; A. Sampaio . Compositional Abstraction of CSPZ Processes. Journal of the Brazilian Computer Society , v. 14, p. 23-44, 2008.

• A. FARIAS ; A. Mota ; A. Sampaio . Um Conversor da Notação CSPZ para CSPM. REIC. Revista Eletrônica de Iniciação Científica , v. 1, p. 105-120, 2001.

• A. Mota ; A. FARIAS ; DIDIER, A. ; Woodcock, J. . Rapid Prototyping of a Semantically Well Founded Circus Model Checker. In: Software Engineering Formal Methods, 2014, Grenoble. Software Engineering and Formal Methods, 2014. v. 8702. p. 235-249.

• GONDIM, D. ; RAMALHO, F. ; A. FARIAS . UCL Uma Linguagem Unificada para Construção de Compiladores. In: II Workshop de Teses e Dissertações do CBSoft, 2012, Natal. Anais do II Workshop de Teses e Dissertações do CBSoft. Natal, 2012. v. 6. p. 73-78.

• DAMASCENO, A. ; A. FARIAS ; A. Mota . A Mechanyzed Strategy for Safe Abstraction of CSP Specifications. In: Brazilian Symposium on Formal Methods, 2009, Gramado. A Mechanyzed Strategy for Safe Abstraction of CSP Specifications, 2009. v. 12. p. 118-133.

• DIDIER, A. ; A. FARIAS ; A. Mota . Checking Z Refinements Using Traces Refinement. In: Brazilian Symposium on Formal Methods, 2008, Salvador. Proceeding of the Brazilian Symposium on Formal Methods. Salvador: Editora Gráfica da UFBA, 2008. v. 1. p. 67-82.

• A. FARIAS ; A. Mota ; A. Sampaio . Efficient CSPz Data Abstraction. In: Integrated Formal Methods, 2004, Canterbury. Proceedings of the 4th International Conference on Integrated Formal Methods, 2004. p. 108-127.

• A. FARIAS ; A. Mota ; A. Sampaio . Efficient Analysis of Infinite CSPZ Specifications. In: Workshop On Formal Methods, 2002, Gramado. Proceedings Of 5th Workshop On Formal Methods, 2002. v. 5. p. 113-128.

• A. FARIAS ; A. Mota ; A. Sampaio . De CSPZ para CSPM: Uma Ferramenta Transformacional Java. In: Workshop de Métodos Formais, 2001, Rio de Janeiro. Proceedings Of 4th Workshop On Formal Methods, 2001. v. 4. p. 1-10.

• A. FARIAS ; FERRAZ, C. A. G. ; OLIVEIRA, J. P. ; SIMÕES, M. A. C. ; ALMEIDA, M. P. ; ROSA, N. S. . TNS: Um serviço de Nomes CORBA Tolerante a Falhas.. In: Workshop de Objetos Distribuídos, 2001. Anais do 1o Workshop de Objetos Distribuídos.

• A. FARIAS ; P. LUCENA . Sistemas Dedutivos Rotulados e suas Aplicações ao Raciocínio Abdutivo. In: VII CONIC (Congresso Nacional de Iniciação Científica), 1999, Recife. Anais do VII CONIC, 1999. p. 148-149.

• A. Mota ; A. FARIAS . A Rapid Approach for Building a Semantically Well Founded Circus Model Checker. In: Congresso Brasileiro de Software, 2014, Maceió. Anais da Sessão de Ferramentas do CBSoft 2014, 2014. v. 2. p. 77-84.

• A. Mota ; A. FARIAS . Implementing an SMT-based Model Checker for CSP from its Operational Semantics. In: Congresso Brasileiro de Software, 2013, Brasília. XVI Simpósio Brasileiro de métodos formais, 2013. v. 1. p. 36-41.

• A. FARIAS ; A. Mota ; A. Sampaio . A Support Tool for CSP-Z Data Abstraction. In: FME Symposium, 2003, Pisa. The 12th International FME Symposium, 2003. p. 11-14.

• A. FARIAS . Efficient Analysis of Infinite CSPZ Specifications: strategy and tool support. 2004. (Apresentação de Trabalho/Seminário).

• A. FARIAS ; A. Mota ; A. Sampaio . Efficient Analysis of Infinite CSPZ Specifications. 2002. (Apresentação de Trabalho/Seminário).

Outras produções

Projetos de pesquisa

• 2014 - Atual

  Verificação de Modelos com Estados Enriquecidos, Projeto certificado pelo(a) coordenador(a) Alexandre Cabral Mota em 18/12/2014., 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: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Mestrado acadêmico: (2) . , Integrantes: Adalberto Cajueiro de Farias - Integrante / Alexandre Cabral Mota - Coordenador / Augusto Sampaio - Integrante / Juliano Manabu Iyoda - Integrante / Fabio Soares dos Santos - Integrante / Rafael Pereira de Araújo - Integrante.

• 2014 - Atual

  Uma Infra-estrutura Integrada para Desenvolvimento de Aplicações Envolvendo Analytics e Big-Data, Descrição: Analytics é a descoberta e comunicação de padrões nos dados que sejam úteis para algum propósito. Essa técnica tem um valor imenso em áreas de manipulação de dados e faz uso de diversas áreas, teorias e técnicas sobrejacentes tais como estatística, programação, pesquisa operacional, mineração, otimização, visualização de dados, etc. Neste contexto onde diversas ferramentas são utilizadas por analytics, a definição, aplicação e adaptação de técnicas de analytics tem diversos custos associados: contextualização do problema, conhecimento e seleção da técnica mais adequada para o problema, conhecimento de frameworks para implementação da técnica, conhecimentos arquiteturais programáticos, conhecimentos de infra-estrutura para grandes volumes de dados, etc. Nesse sentido, a integração das ferramentas é algo extremamente desejável para reduzir custos da aplicação de analytics. O objetivo desta proposta é produzir um protótipo de um framework que integre metodologias e ferramentas ao processo de desenvolvimento de aplicações que lidam com análise de grandes volumes de dados. Adicionalmente, o protótipo tem também o propósito de ser utilizado em novos ?startups? da UFCG (e quais quer outros projetos) que estejam alinhados com o tema, ampliar os horizontes e consolidar a UFCG nesta área de pesquisa. Apesar disso representar um significativo impacto regional, o protótipo proposto, num escopo mais amplo, será o passo inicial de uma infra-estrutura integrada de suporte para desenvolvimento de aplicações relacionadas a Big-Data. Nesse sentido a proposta foca em diminuir o impacto de lidar com Big Data no processo de desenvolvimento de software, abstraindo detalhes de analytics e integração entre frameworks sobrejacentes.. , Situação: Em andamento; Natureza: Pesquisa. , Integrantes: Adalberto Cajueiro de Farias - Coordenador / Leandro Balby - Integrante / Nazareno Andrade - Integrante / Andrey Elísio Monteiro Brito - Integrante / Tiago Massoni - Integrante / Reinaldo Cézar de Morais Gomes - Integrante.

• 2012 - 2014

  Desenvolvimento sistemático e rigoroso para sistemas aeronáuticos, Projeto certificado pelo(a) coordenador(a) Alexandre Cabral Mota em 02/01/2014., 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: Concluído; Natureza: Pesquisa. , Integrantes: Adalberto Cajueiro de Farias - Integrante / Alexandre Cabral Mota - Coordenador / Augusto Cesar Alves Sampaio - Integrante / Juliano Manabu Iyoda - Integrante.

• 2011 - 2014

  COMPASS Comprehensive Modelling for Advanced Systems of Systems, Projeto certificado pelo(a) coordenador(a) Augusto Cezar Alves Sampaio em 23/05/2013., 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) / Especialização: (2) / Mestrado acadêmico: (2) . , Integrantes: Adalberto Cajueiro de Farias - Integrante / Alexandre Cabral Mota - Integrante / Augusto Cesar Alves Sampaio - Coordenador / Juliano Manabu Iyoda - Integrante / Márcio Lopes Cornélio - Integrante.

• 2009 - 2011

  Análise de Segurança Baseada em Modelos para Sistemas Autônomos, Descrição: O projeto é direcionado ao emprego integrado e complementar de técnicas de Métodos Formais e Confiabilidade para sistemas aeroespaciais. O principal objetivo é a definição de estratégias para a modelagem formal e análise de aspectos funcionais e não-funcionais (segurança) de sistemas aeroespaciais. Em particular, procuramos com este projeto permitir que sistemas aeroespaciais sejam desenvolvidos com ainda mais qualidade, onde corretude e segurança são os principais fatores envolvidos, no entanto requerendo um custo menor do que o empregado atualmente. Avanços são esperados em vários aspectos e norteados pela alta competitividade do mercado e pelos estudos existentes sobre o custo da não-conformidade dos softwares. , Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (1) / Mestrado acadêmico: (2) . , Integrantes: Adalberto Cajueiro de Farias - Integrante / Alexandre Cabral Mota - Coordenador / Augusto Cesar Alves Sampaio - Integrante / Juliano Manabu Iyoda - Integrante., Financiador(es): Agência Espacial Brasileira - Auxílio financeiro.

• 2009 - 2011

  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 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.. , Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (1) / Mestrado acadêmico: (2) . , Integrantes: Adalberto Cajueiro de Farias - Integrante / Alexandre Cabral Mota - Coordenador / Augusto Cesar Alves Sampaio - Integrante / Juliano Manabu Iyoda - Integrante., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro.

• 2014 - 2014

  Investigação de novos cenários para utilização dos terminais Ingenico, Descrição: Pesquisa de novas situações de uso para terminais Ingenico.. , Situação: Concluído; Natureza: Outra. , Integrantes: Adalberto Cajueiro de Farias - Integrante / Wilkerson Andrade - Coordenador / Patricia Machado - Integrante / Nazareno Andrade - Integrante / Dalton Guerrero - Integrante.

• 2014 - 2014

  SAFF - Análise estatísticas dos arquivos de falhas dos terminais Ingenico Telium, Descrição: Análise de falhas de software acontecidas em terminais Ingenico.. , Situação: Concluído; Natureza: Outra. , Alunos envolvidos: Graduação: (4) . , Integrantes: Adalberto Cajueiro de Farias - Integrante / Alexandre Mota - Integrante / Wilkerson Andrade - Coordenador / Jorge Abrantes - Integrante.

• 2013 - 2015

  Smart-TCE, Descrição: Projeto destinado a investigar técnicas de analytics e vizualização de dados armazenados em HP Vertica.. , Situação: Concluído; Natureza: Outra. , Integrantes: Adalberto Cajueiro de Farias - Coordenador / Wilkerson Andrade - Integrante / Leandro Balby - Integrante / Nazareno Andrade - Integrante / Andrey Elísio Monteiro Brito - Integrante.

• 2013 - 2013

  Componentização de novos casos de uso de Contactless (NFC) e de Identificação Biométrica, Descrição: Projeto focado em desenvolver aplicações para uso de contactless e identificação biométrica envolvendo terminais da Ingenico.. , Situação: Concluído; Natureza: Outra. , Integrantes: Adalberto Cajueiro de Farias - Integrante / Wilkerson Andrade - Coordenador / Patricia Machado - Integrante / Dalton Guerrero - Integrante.

Prêmios