Lucas Albertins de Lima

Pós-doutorado

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

• RY', ARKADIUSZ ; LIMA, LUCAS ; EXELMANS, JOERI ; JANSSENS, DENNIS ; VANGHELUWE, HANS . Model management to support systems engineering workflows using ontology-based knowledge graphs. Journal Of Industrial Information Integration , v. 42, p. 100720, 2024.

• Falcão, Flávia ; LIMA, LUCAS ; SAMPAIO, AUGUSTO ; ANTONINO, PEDRO . A formal component model for UML based on CSP aiming at compositional verification. Software and Systems Modeling , v. 1, p. 1, 2023.

• LIMA, LUCAS ; TAVARES, AMAURY ; NOGUEIRA, SIDNEY C. . A framework for verifying deadlock and nondeterminism in UML activity diagrams based on CSP. SCIENCE OF COMPUTER PROGRAMMING , v. 197, p. 102497, 2020.

• LIMA, LUCAS ; MIYAZAWA, ALVARO ; CAVALCANTI, ANA ; CORNÉLIO, MÁRCIO ; IYODA, JULIANO ; SAMPAIO, AUGUSTO ; HAINS, RALPH ; LARKHAM, ADRIAN ; LEWIS, VAUGHAN . An integrated semantics for reasoning about SysML design models using refinement. Software & Systems Modeling , v. 16, p. 875-902, 2017.

• LIMA, L. A. . Formal Methods: Foundations and Applications. 1. ed. Springer Cham, 2022. v. 1. 143p .

• LIMA, L. A. . Formalisation of SysML Models and Analysis based on Refinement. 1. ed. Saarbrücken: LAP Lambert Academic Publishing, 2016. v. 1. 320p .

• LIMA, L. A. . Test Case Prioritization Based on Data Reuse. 1. ed. Saarbrücken: LAP LAMBERT, 2011. v. 1. 116p .

• FERREIRA, D. ; LIMA, L. A. . A CSP Semantics for UML State Machines Aiming at Hidden Formal Methods Verification. In: XXVII Brazilian Symposium on Formal Methods (SBMF 2024), 2024, Vitória-ES. Proceeding of the 27th Brazilian Symposium on Formal Methods, 2024.

• FERREIRA, D. ; LIMA, L. A. . Verifying Integrated Designs of UML State Machines and Activities Using CSP. In: XXVII Brazilian Symposium on Formal Methods (SBMF 2024), 2024, Vitória-ES. Proceeding of the 27th Brazilian Symposium on Formal Methods, 2024.

• MARAH, H. ; LIMA, L. A. ; CHALLENGER, M. ; VANGHELUWE, H. . Towards Ontology Enabled Agent-based Twinning for Cyber-physical Systems. In: 2023 ACM/IEEE International Conference on Model Driven Engineering Languages and Systems Companion, 2023, Vasteras. MODELS '23: Proceedings of the 26th International Conference on Model Driven Engineering Languages and Systems: Companion, 2023.

• MITTAL, R. ; ESLAMPANAH, R. ; LIMA, L. A. ; VANGHELUWE, H. ; BLOUIN, D. . Towards an Ontological Framework for Validity Frames. In: 2023 ACM/IEEE International Conference on Model Driven Engineering Languages and Systems Companion, 2023, Vasteras. MODELS '23: Proceedings of the 26th International Conference on Model Driven Engineering Languages and Systems: Companion, 2023.

• CEDERBLADH, J. ; CLEOPHAS, L. ; KAMBURJAN, E. ; LIMA, L. A. ; VANGHELUWE, H. . Symbolic Reasoning for Early Decision-Making in Model-Based Systems Engineering. In: 2023 ACM/IEEE International Conference on Model Driven Engineering Languages and Systems Companion, 2023, Vasteras. MODELS '23: Proceedings of the 26th International Conference on Model Driven Engineering Languages and Systems: Companion, 2023.

• LINDOSO JR, W. ; NOGUEIRA, SIDNEY ; DOMINGUES, R. ; LIMA, L. A. . Visual Specification of Properties for Robotic Designs. In: XXIV Simpósio Brasileiro de Métodos Formais, 2021, Campina Grande - PB. Anais do XXIV Simpósio Brasileiro de Métodos Formais, 2021.

• LIMA, L. A. ; NOGUEIRA, S. C. ; TAVARES, A. . A framework for verifying deadlock and nondeterminism in UML activity diagrams based on CSP. In: Brazilian Symposium on Formal Methods (SBMF), 2019, São Paulo. Proceedings of the XXII Brazilian Symposium on Formal Methods, 2019.

• LIMA, LUCAS ; TAVARES, AMAURY . Verifying Deadlock and Nondeterminism in Activity Diagrams. In: 2019 ACM/IEEE 22nd International Conference on Model Driven Engineering Languages and Systems Companion (MODELSC), 2019, Munich. 2019 ACM/IEEE 22nd International Conference on Model Driven Engineering Languages and Systems Companion (MODELS-C), 2019. p. 764.

• FERREIRA, LARISSA ; NOGUEIRA, SIDNEY ; LIMA, LUCAS ; FONSECA, LILIANE ; FERREIRA, WALDEMAR . Initial findings on the evaluation of a model-based testing tool in the test design process. In: 2019 ACM/IEEE International Symposium on Empirical Software Engineering and Measurement (ESEM), 2019, Porto de Galinhas. 2019 ACM/IEEE International Symposium on Empirical Software Engineering and Measurement (ESEM), 2019. p. 1.

• Falcão, Flávia ; LIMA, L. A. ; SAMPAIO, A. C. A. . Safe and Constructive Design with UML Components. In: Brazilian Symposium on Formal Methods, 2018, Salvador. Proceedings of the XXI Brazilian Symposium on Formal Methods, 2018. v. 11254. p. 234-251.

• LIMA, L. A. ; IYODA, J. M. ; SAMPAIO, A. C. A. . Refinement Verification of Sequence Diagrams Using CSP. In: Brazilian Symposium on Formal Methods, 2016, Natal. Formal Methods: Foundations and Applications. SBMF 2016., 2016.

• LIMA, L. A. ; IYODA, J. M. ; SAMPAIO, A. C. A. . A Formal Semantics for Sequence Diagrams and a Strategy for System Analysis. In: International Conference on ModelDriven Engineering and Software Development, 2014, Lisbon. Proceedings of the 2nd International Conference on Model-Driven Engineering and Software Development, 2014. p. 317.

• MIYAZAWA, A. ; LIMA, L. A. ; CAVALCANTI, A. . Formal Models of SysML Blocks. In: International Conference on Formal Engineering Methods (ICFEM 2013), 2013, Queenstown, New Zealand. Proceedings of the 15th International Conference on Formal Engineering Methods(Lecture Notes in Computer Science), 2013. v. 8144.

• LIMA, L. A. ; DIDIER, A. ; CORNELIO, M. . A Formal Semantics for SysML Activity Diagrams. In: Brazilian Symposium on Formal Methods (SBMF 2013), 2013, Brasilia, DF, BR. Proceedings of the 16th Brazilian Symposium on Formal Methods (Lecture Notes in Computer Science), 2013. v. 8195. p. 179-194.

• LIMA, L. A. ; ARANHA, Eduardo ; IYODA, J. M. ; SAMPAIO, A. C. A. . Test Case Prioritization Based on Data Reuse - An Experimental Study. In: 3rd International Symposium on Empirical Software Engineering and Measurement, 2009, Lake Buena Vista. Proceedings of the 3rd Empirical Software Engineering and Measurement (ESEM), 2009. p. 279-290.

• LIMA, L. A. ; IYODA, J. M. ; SAMPAIO, A. C. A. . A Permutation Technique for Test Case Prioritization in a Black-box Environment. In: SAST - 2nd Brazilian Workshop on Systematic and Automated Software Testing, 2008, Campinas/SP. Anais do 2º Workshop Brasileiro sobre Teste de Software Sistemático e Automatizado, 2008.

• LIMA, L. A. ; BARBOSA, A. E. V. ; FERREIRA NETO, W. P. ; Fechine, J. M. . PERSEU - Ferramenta Computacional para a Prevenção do DORT Causado pelo uso Contínuo do Computador. In: III Simpósio Brasileiro de Sistemas de Informação, 2006, Curitiba. Anais do III Simpósio Brasileiro de Sistemas de Informação, 2006.

• LIMA, L. A. ; FERREIRA NETO, W. P. . Projeto CCT - Component Composition Tools. In: V ENEPET, 2006, Salvador. V ENEPET, 2006.

• FERREIRA NETO, W. P. ; LIMA, L. A. ; BARBOSA, A. E. V. ; Fechine, J. M. . PERSEU - Ferramenta de Profilaxia ao DORT. In: Simpósio de Fatores Humanos em Sistemas Computacionais (IHC), 2006, Natal. Anais Estendidos do IHC 2006, 2006.

• BARBOSA, A. E. V. ; FERREIRA NETO, W. P. ; REGIS, M. V. O. ; LIMA, L. A. . Projeto PERSEU - Uma Ferramenta Computacional Para Auxílio na Recução de DORT Devido ao Uso do Computador. In: XI Encontro Nacional dos Grupos PET (ENAPET), 2006, Florionópolis. Anais do XI ENAPET, 2006.

• LIMA, L. A. ; Fechine, J. M. . Metodologia Utilizada pelo PET-Computação da UFCG. In: XI Encontro Nacional dos Grupos PET (ENAPET), 2006, Florionópolis. Anais do XI ENAPET, 2006.

• LIMA, L. A. ; FERREIRA NETO, W. P. . Eclipse Tools - Ferramenta de Auxílio a Composição Dinâmica de Software. In: I Encontro Unificado de Ensino, Pesquisa e Extensão da UFCG, 2005, Campina Grande. Anais do I Encontro Unificado de Ensino, Pesquisa e Extensão, 2005.

• FERREIRA, D. ; LIMA, L. A. . Verifying Integrated Designs of UML State Machines and Activities Using CSP. 2024. (Apresentação de Trabalho/Conferência ou palestra).

• FERREIRA, D. ; LIMA, L. A. . A CSP Semantics for UML State Machines Aiming at Hidden Formal Methods Verification. 2024. (Apresentação de Trabalho/Conferência ou palestra).

• LIMA, L. A. . Building the support for the verification of activity diagrams in the context of OpenMBEE. 2022. (Apresentação de Trabalho/Conferência ou palestra).

• LIMA, L. A. ; TAVARES, A. . Verifying deadlock and nondeterminism in activity diagrams. 2019. (Apresentação de Trabalho/Conferência ou palestra).

• LIMA, L. A. ; TAVARES, A. ; NOGUEIRA, S. C. . A framework for verifying deadlock and nondeterminism in UML activity diagrams based on CSP. 2019. (Apresentação de Trabalho/Congresso).

• LIMA, L. A. ; IYODA, J. M. ; SAMPAIO, A. C. A. . Refinement Verification of Sequence Diagrams Using CSP. 2016. (Apresentação de Trabalho/Conferência ou palestra).

• LIMA, L. A. ; IYODA, J. M. ; SAMPAIO, A. C. A. . A Formal Semantics for Sequence Diagrams and a Strategy for System Analysis. 2014. (Apresentação de Trabalho/Conferência ou palestra).

• LIMA, L. A. ; IYODA, J. M. ; SAMPAIO, A. C. A. . A Formal Semantics for SysML Activity Diagrams. 2013. (Apresentação de Trabalho/Conferência ou palestra).

• LIMA, L. A. ; ARANHA, Eduardo ; IYODA, J. M. ; SAMPAIO, A. C. A. . Test Case Prioritization Based on Data Reuse - An Experimental Study. 2009. (Apresentação de Trabalho/Simpósio).

• LIMA, L. A. . Report on Guidelines for Analysis of SysML Diagrams 2014 (Relatório Técnico).

Outras produções

Projetos de pesquisa

• 2024 - Atual

  Desenvolvimento de um ambiente para execução e análise de modelos SysML v2, Descrição: Os domínios relacionados a Engenharia de Sistemas estão passando por uma mudança de paradigma em direção a digitalização. Isto é causado pelos crescentes avanços tecnológicos em conjunto com as estritas regulações sobre sustentabilidade, enquanto a satisfação dos clientes e a competitividade do mercado precisam ser alcançados. Em domínios como automobilístico, ferroviário e aviônico, fortes fundações em Engenharia de Sistemas existem para o desenvolvimento e gerenciamento de produtos. Com o advento da digitalização, a Engenharia de Sistemas baseada em Modelos (Model-based System Engineering MBSE) tem se tornado interesse em ser adotada por estas indústrias. Um benefício esperado de uma abordagem MBSE são as capacidades analíticas antecipadas durante o desenvolvimento de sistemas. Isto é habilitado por modelos de sistemas completos que apoiam a tomada de decisão nas fases iniciais do projeto de sistemas. Neste contexto, a linguagem SysML tem ocupado um espaço relevante nas indústrias que buscam aplicar MBSE. É notável o aumento da adoção desta linguagem para habilitar processos de MBSE. Assim, percebemos SysML caminhar para se tornar um padrão e referência neste círculo. Apesar da sua expansão, a primeira versão da linguagem, a qual é especificada como um perfil da linguagem UML, também recebeu diversas críticas, como difícil interoperabilidade, alguns pontos semânticos imprecisos, extensibilidade, dentre outros. Em termos ferramentais, cada fornecedor termina desenvolvendo sua própria versão implementação de SysML na qual diversas funcionalidades como simulação, análise, e animação de modelos podem ser desenvolvidas na maioria das vezes sem relação entre elas, ou seja, sem considerar uma semântica formal única. Devido a estes fatores, a OMG criou um grupo de trabalho para definir uma nova versão da linguagem (SysML v2) de acordo com um conjunto de requisitos especificados para lidar com as críticas da sua primeira versão, como por exemplo, um metamodelo independente da UML, uma semântica formal declarativa baseada em conceitos de lógica e matemática, uma notação textual padronizada além da notação gráfica, dentre outros. A primeira versão beta da linguagem foi lançada em junho de 2023. Apesar de ainda não estar completa, já identificamos a movimentação de fornecedores na corrida para disponibilizar de ferramentas o quanto antes para angariar fatias do mercado. Neste sentido temos o risco de repetir os mesmos problemas que aconteceram com a primeira versão da linguagem. Contudo, percebemos também uma oportunidade de disponibilizar mecanismos baseados em técnicas rigorosas para a construção de ferramentas para apoiar o projeto de sistemas através do uso de SysML v2. Através de uma parceria com o grupo de pesquisa do laboratório Lab-STICC da Universidade ENSTA-Bretagne na França pretendemos usar o arcabouço construído por este grupo para especificar a semântica de SysML v2 e permitir a geração de diversas ferramentas de apoio ao projeto de sistemas como verificadores de propriedades, animadores, depuradores, como também a síntese de código fonte para diferentes plataformas. Tais ferramentas utilizarão uma mesma base semântica, com isto, manteremos a integridade dos resultados, além de basear todas as ferramentas em uma semântica rigorosa.. , Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (1) . , Integrantes: Lucas Albertins de Lima - Coordenador / NOGUEIRA, SIDNEY - Integrante / Ciprian Teodorov - Integrante.

• 2024 - Atual

  Raciocínio automatizado em grafos de conhecimento virtuais para apoiar processos de engenharia, Descrição: A gestão do conhecimento é crucial para apoiar processos de engenharia devido a vasta quantidade de artefatos e formalismos utilizados, muitas vezes sem conexões claras entre eles. Nesta pesquisa buscaremos usar estruturas chamadas grafos de conhecimento (do termo em inglês Knowledge Graphs), as quais vêm sendo bastante utilizadas por grandes companhias como Google, Meta e Amazon, para representar o conhecimento criado pelos processos de engenharia, aliado a técnicas de raciocínio automatizado para otimizar as tarefas dos engenheiros de sistema. Tais grafos visam estabelecer relações entre conceitos que ficam armazenados em uma estrutura de dados que permite consulta e inferência de novos conhecimentos. Para permitir a tipificação destes grafos e garantir sua boa formação, vamos utilizar ontologias, as quais são úteis para especificar conceitos e relações de domínios específicos. A partir do uso de ontologias é possível não só validar propriedades sobre um domínio, como também gerar estruturas a serem conectadas no grafo de conhecimento. Esperamos explorar esta estratégia para reutilizar informações das atividades realizadas durante a execução de processos de engenharia não só para facilitar o acesso ao conhecimento, como também permitir a conexão de artefatos e seus dados para possibilitar raciocínio automatizado sobre esta informações. Com os resultados deste raciocínio esperamos otimizar os processos de engenharia. Por exemplo, com os dados de experimentos previamente realizados, podemos inferir ou guiar que outros experimentos precisam ser realizados poupando tempo do engenheiro de sistema.. , Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (1) / Mestrado acadêmico: (1) . , Integrantes: Lucas Albertins de Lima - Coordenador / NOGUEIRA, SIDNEY - Integrante / Hans Vangheluwe - Integrante.

• 2021 - 2023

  Digital Twin Design - DTDesign, Descrição: This project aims at developing a framework, comprising a methodology and supporting tools, for the systematic and efficient design of Digital Twins providing answers to two question types: (i) production parameters - product performance correlation and (ii) faults detection and diagnosis. The purpose of the framework is to support the user in choosing which data sets and models to combine and how to deploy them (Digital Twin implementation) to get an answer to the posed questions based on application specific requirements and criteria. The final goal is to use the developed framework to efficiently design Digital Twins and implement them for seven industrial use cases.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: / Mestrado profissional: (1) / Doutorado: (3) . , Integrantes: Lucas Albertins de Lima - Integrante / Hans Vangheluwe - Coordenador.

• 2020 - Atual

  Desenvolvimento de um ambiente de código aberto para verificação de modelos UML comportamentais, Descrição: Durante o processo de desenvolvimento de sistemas, sejam eles de hardware ou software, as fases de análise e projeto têm um papel crucial por definir a arquitetura do sistema que será construído. Nestas fases os modelos evoluem, de forma que um modelo mais abstrato é refinado repetidamente até chegar em um modelo concreto, ou seja, mais próximo da implementação. Durante esta evolução é importante garantir que propriedades dos modelos mais abstratos ainda existam nos modelos mais concretos. Em geral, esta abordagem de verificação é feita de forma empírica, baseada principalmente na experiência dos projetistas, o que a torna bastante propícia a erros. A propagação destes erros pode tornar suas correções bastante custosas. Portanto, detecção de problemas ainda nesta fase é crucial para reduzir custos com manutenções. Neste contexto, a linguagem UML (Unified Modeling Language) é usada como padrão para o projeto de sistemas computacionais. Ela propõe diversos diagramas para a modelagem de conceitos estruturais e comportamentais. Dentre os diagramas comportamentais mais utilizados podemos citar: Diagrama de Sequência, Diagrama de Atividades e Diagrama de Máquina de Estados. Apesar de ser bastante difundida na indústria e a Academia, mecanismos de validação de tais modelos são escassos ou sem algum tipo de padronização. Este projeto propõe a criação de um ambiente integrado de código aberto para análise de propriedades de modelos UML comportamentais. A estratégia, baseada em MDE - Model Driven Engineering (Engenharia Dirigida a Modelos), é composicional, no sentido de que a análise de sistemas complexos reutiliza verificações de componentes destes sistemas. Como entrada para a estratégia utilizamos modelos UML de análise e projeto de sistemas. O ambiente proposto integra e estende nossa pesquisa anterior que propõe uma estratégia de análise de propriedades de sistemas modelados em UML, como também semânticas formais para os seus diagramas. No entanto, para aplicar os resultados desta pesquisa, esperamos que o projeto seja desenvolvido num contexto de código aberto para que o ambiente possa ser facilmente integrado com ferramentas UML existentes. Para tanto, visamos fazer parcerias com iniciativas de modelagem integradas como o projeto OpenMBEE, assim como também empresas desenvolvedoras de ambientes de modelagem. Este projeto envolve as seguintes contribuições: (i) definição de noções formais de propriedades a serem verificadas em diagramas comportamentais da UML; (ii) tradução de diagramas comportamentais de UML para CSP (Communicating Sequential Processes), permitindo o reuso de uma estratégia de análise desenvolvida anteriormente para verificação de propriedades; (iii) um ambiente de verificação de diagramas UML comportamentais de código aberto que permita a integração com ferramentas de modelagem existentes; (iv) realização de estudos empíricos para analisar as vantagens comparativas da abordagem proposta com os atuais processos de validação de modelos. Ao final do projeto, espera-se entregar tecnologias que permitam a construção de sistemas mais seguros e com maior qualidade devido ao suporte ferramental para validação de suas arquiteturas.. , Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (2) . , Integrantes: Lucas Albertins de Lima - Coordenador / Sidney de Carvalho Nogueira - Integrante / Amaury Tavares - Integrante / Renato Domingues - Integrante.

• 2019 - Atual

  INCT para Engenharia de Software (INES), Descrição: O objetivo geral deste Instituto é desenvolver técnicas, ferramentas e processos de engenharia de software que sirvam de base para aplicações avançadas, como por exemplo a plataforma aberta de serviços voltada para Cidades Inteligentes descrita no programa de pesquisa da Seção 3. Esperamos avanços em técnicas como Linhas de Produtos de Software (LPS), especificação e testes de sistemas distribuídos, e engenharia de software experimental, entre outras, explorando também a integração entre as técnicas, coordenando os esforços e competências das diversas instituições e pesquisadores envolvidos. Desta forma, esperamos que as técnicas e ferramentas propostas forneçam vantagens competitivas às empresas que as adotem, tanto melhorando a confiabilidade, como a produtividade no desenvolvimento de aplicações para cidades inteligentes. Os objetivos específicos do Instituto: * Desenvolver pesquisa científica de vanguarda com padrão internacional na área de Engenharia de Software, com foco em Cidades Inteligentes * Formar recursos humanos qualificados na área de Engenharia de Software * Difundir conhecimento para a sociedade * Difundir conhecimento para o setor empresarial *.. , Situação: Em andamento; Natureza: Pesquisa. , Integrantes: Lucas Albertins de Lima - Integrante / Augusto Cezar Alves Sampaio - Coordenador.

• 2017 - 2022

  Um Framework Baseado em Modelos para Análise e Teste Composicionais de Sistemas Reativos, Situação: Concluído; Natureza: Pesquisa. , Integrantes: Lucas Albertins de Lima - Integrante / Augusto Cezar Alves Sampaio - Coordenador / Marcel Oliveira - Integrante / CORNÉLIO, MÁRCIO - Integrante / IYODA, JULIANO - Integrante / Alexandre Cabral Mota - Integrante.

• 2017 - 2020

  Desenvolvimento de um Arcabouço para Verificação de Refinamento de Modelos UML comportamentais, Descrição: Durante o processo de desenvolvimento de sistemas, sejam eles de hardware ou software, as fases de análise e projeto têm um papel crucial por definir a arquitetura do sistema que será construído. Nestas fases os modelos evoluem, de forma que um modelo mais abstrato é refinado repetidamente até chegar em um modelo concreto, ou seja, mais próximo da implementação. Durante esta evolução é importante garantir que propriedades dos modelos mais abstratos ainda existam nos modelos mais concretos. Em geral, esta abordagem de verificação é feita de forma empírica, baseada principalmente na experiência dos projetistas, o que a torna bastante propícia a erros. A propagação destes erros pode tornar suas correções bastante custosas. Portanto, detecção de problemas ainda nesta fase é crucial para reduzir custos com manutenções. Assim, este projeto propõe um arcabouço integrado para análise de refinamento de modelos UML comportamentais. A estratégia, baseada em MDE - Model Driven Engineering (Engenharia Dirigida a Modelos), é composicional, no sentido de que a análise de sistemas complexos reutiliza verificações de componentes destes sistemas. Como entrada para a estratégia utilizamos modelos de análise e projeto de sistemas que utilizam a linguagem UML. Tal linguagem é semiformal e sua semântica é definida em linguagem natural e através do uso de meta-modelos, também semiformais. O framework proposto integra e estende, significativamente, uma pesquisa anterior que propõe uma estratégia de análise de propriedades de sistemas modelados em UML, como também semânticas para os seus diagramas. Este projeto envolve as seguintes contribuições: (i) definição de uma noções de refinamentos de diagramas comportamentais da UML, que será a base para permitir uma análise formal dos refinamento de modelos UML; (ii) tradução de diagramas comportamentais de UML para CSP (Communicating Sequential Processes), permitindo o reuso de uma estratégia de análise desenvolvida anteriormente, só que agora explorando aspectos de refinamento; (iii) um arcabouço que integra ferramenta de modelagem e ferramentas formais de forma a verificar automaticamente refinamentos de modelos diagramáticos; (iv) realização de estudos empíricos para analisar as vantagens comparativas da abordagem proposta com os atuais processos de validação de modelos. Ao final do projeto, espera-se entregar tecnologias que permitam a construção de sistemas mais seguros e com maior qualidade devido ao suporte ferramental para validação de suas arquiteturas.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (3) / Mestrado acadêmico: (1) . , Integrantes: Lucas Albertins de Lima - Coordenador / Sidney de Carvalho Nogueira - Integrante / Wallace Santana de Lima - Integrante / Amaury Tavares - Integrante / Daniel Freire de Araújo - Integrante / Renato Domingues - Integrante., Financiador(es): Universidade Federal Rural de Pernambuco - Auxílio financeiro.

• 2013 - 2018

  Modelagem, Verificação e Teste Composicional de Sistemas com Aplicações na Indústria Aeronáutica, Descrição: Neste projeto, propomos a sistematização de vários aspectos do projeto de grandes sistemas, particularmente, com ênfase em Sistemas de Sistemas (SoS, Systems of Sytems). O escopo inclui modelagem (semiformal e formal), verificação (análise formal de propriedades) e teste de tais sistemas. Utilizamos a linguagem SysML para descrever requisitos e os modelos de análise e projeto (design) de um SoS. SysML é uma linguagem semiformal, amplamente utilizada na indústria, com uma semântica definida em linguagem natural e através do uso de meta-modelos, também semiformais. Portanto, ambiguidades nos modelos SysML podem induzir a erros de implementação. No processo proposto, o modelo em SysML é traduzido (automaticamente) para um modelo descrito na linguagem formal Circus, que integra a álgebra de processos CSP, para expressar os aspectos reativos, a linguagem baseada em modelos Z, para expressar os aspectos de dados e a linguagem de comandos guardados de Dijkstra, fazendo de Circus não apenas uma linguagem de especificação, mas também de programação. Como segunda etapa do processo proposto, o modelo Circus será verificado com o objetivo de se garantir a preservação de propriedades de interesse. Isto permitirá, inicialmente, verificar a consistência, tanto individual, como integrada, dos diagramas SysML do sistema. Um outro aspecto da análise é o desenvolvimento de uma estratégia que garanta, por construção, a ausência de problemas clássicos como deadlock no SoS, a partir da verificação da ausência de deadlock em seus componentes. O desafio desta análise é escalabilidade. Como terceira e última etapa do processo, complementar à verificação, será desenvolvida uma estratégia automática de geração de vetores de teste a partir da especificação em Circus. Finalmente, o escopo do projeto inclui uma avaliação, em um ambiente industrial, com o apoio da Embraer, da eficácia dos métodos de modelagem, análise e teste propostos, através da aplicação na área de aviação e na arquitetura IMA (Integrated Modular Avionics) em particular. Este projeto inclui um breve relato das metas atingidas no período anterior. Alguns resultados, restritos a aspectos de controle em CSP e testados em exemplos pequenos, serão estendidos para um formalismo multiparadigma (Circus) e validados em aplicações reais de IMA.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Mestrado acadêmico: (1) Doutorado: (3) . , Integrantes: Lucas Albertins de Lima - Integrante / Augusto Cezar Alves Sampaio - Coordenador.

• 2013 - 2014

  Desenvolvimento de um Arcabouço para construção de sites da Pró-Reitoria de Pesquisa e Pós-Graduação, Descrição: Desenvolvimento de uma infra-estrutura de software que permita a criação de sites de programas de pós-graduação relacionados a Pró-Reitoria de Pesquisa e Pós-Graduação da UFRPE de forma automatizada e padronizada. Uma camada de software será desenvolvida sobre a plataforma Drupal para fornecer tal arcabouço.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (3) . , Integrantes: Lucas Albertins de Lima - Coordenador / RICARDO ANDRÉ CAVALCANTE DE SOUZA - Integrante.

• 2012 - 2015

  Modelagem e Análise Composicional de Sistemas de Sistemas com Aplicações na Indústria Aeronáutica, Descrição: Propomos um processo para modelagem e análise formal de propriedades de Sistemas de Sistemas (SoS, Systems of Sytems), com ênfase em aplicações na área de aviação e na arquitetura IMA (Integrated Modular Avionics) em particular. Utilizamos a linguagem SysML para descrever requisitos e os modelos de análise e projeto (design) de um SoS. SysML é uma linguagem semiformal cuja semântica é definida em linguagem natural e através do uso de meta-modelos, também semiformais. Por um lado, uma notação semiformal (e gráfica) conquista uma adoção ampla e rápida pela indústria devido a sua simplicidade e facilidade de aprendizado. Por outro lado, ambiguidades nos modelos podem induzir a erros de implementação. Por sua vez, usualmente há resistência, no ambiente industrial, com relação à adoção de uma notação formal, mesmo com a promessa de especificações formais serem livres de ambiguidades e poderem ser analisadas de forma rigorosa com auxílio de ferramentas. No processo proposto, o modelo em SysML é traduzido (automaticamente) para um modelo descrito na linguagem formal Circus, que integra a álgebra de processos CSP, para expressar os aspectos reativos, a linguagem baseada em modelos Z, para expressar os aspectos de dados e a linguagem de comandos guardados de Dijkstra, fazendo de Circus não apenas uma linguagem de especificação, mas também de programação. Desta forma, esperamos produzir uma solução em que a notação gráfica continua disponível, porém com os benefícios adicionais oferecidos pela notação formal Circus. Como segunda etapa do processo proposto, o modelo Circus será analisado com o objetivo de se garantir a preservação de propriedades de interesse. Isto permitirá, inicialmente, verificar a consistência, tanto individual, como integrada, dos diagramas SysML do sistema. Um outro aspecto da análise é o desenvolvimento de uma estratégia que garanta, por construção, a ausência de deadlock no SoS, a partir da verificação da ausência de deadlock em seus componentes. O desafio desta análise é escalabilidade. Finalmente, o escopo do projeto inclui uma avaliação, em um ambiente industrial, com o apoio da Embraer, da eficácia dos métodos de modelagem e análise propostos, através da aplicação da abordagem proposta em um estudo de caso real relacionado a sistemas IMA.. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Mestrado acadêmico: (1) Doutorado: (4) . , Integrantes: Lucas Albertins de Lima - Integrante / Juliano Manabu Iyoda - Integrante / Augusto Cezar Alves Sampaio - Coordenador / André Didier - Integrante / Márcio Cornélio - Integrante / Gustavo Carvalho - Integrante / Marcel Oliveira - Integrante / José Oliveira - Integrante / Pedro Antonino - 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, Projeto certificado pelo(a) coordenador(a) Augusto Cezar Alves Sampaio em 04/03/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 plug-ins 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 plug-ins, 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. , Integrantes: Lucas Albertins de Lima - Integrante / Augusto Cezar Alves Sampaio - Coordenador., Financiador(es): Comunidade Européia - Auxílio financeiro.

• 2009 - 2009

  INES, Descrição: Instituto Nacional para Engenharia de Software participando do grupo de Linhas de Produtos de Geração, Seleção, Priorização e Processamento de Testes.. , Situação: Concluído; Natureza: Pesquisa. , Integrantes: Lucas Albertins de Lima - Coordenador., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Outra.

• 2007 - 2009

  Brazil Test Center, Descrição: Participação no grupo de pesquisa do programa da Motorola chamado Brazil Test Center (BTC) proveniente de uma parceria com o Centro de Informática da UFPE, desenvolvendo pesquisa na área de priorização de casos de teste.. , Situação: Concluído; Natureza: Pesquisa. , Integrantes: Lucas Albertins de Lima - Integrante / Augusto Cezar Alves Sampaio - Coordenador., Financiador(es): Motorola Industrial Ltda. - Outra.

• 2005 - 2007

  Desenvolvimento de Software para Aplicações Móveis, Descrição: Tecnologias para Desenvolvimento de Software para Aplicações Móveis Baseadas em J2ME, SYMBIAN, Linux e Padrões Mobile Alliance. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (4) . , Integrantes: Lucas Albertins de Lima - Coordenador., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Bolsa.

Prêmios