TCC - Bacharelado em Ciência da Computação (Sede)
URI permanente para esta coleçãohttps://arandu.ufrpe.br/handle/123456789/415
Navegar
Item Análise comparativa de técnicas de engenharia de prompt aplicadas a tarefas de recomendação via LLMs(2026-02-13) Silva, Cleyton José Rodrigues da; Lima, Lucas Albertins de; http://lattes.cnpq.br/0465071050875729Sistemas de recomendação são produzidos para sugerir itens a serem consumidos por usuários clientes de uma determinada plataforma digital, seja em e-commerce ou em aplicativos de streaming de conteúdo, tendo o intuito de se adequar cada vez mais às preferências dos usuários-alvos, buscando um teor de personalização que contribua para o sucesso da plataforma. As abordagens mais utilizadas atualmente se apresentam numa combinação de técnicas tradicionais de recomendação com o poder dos LLMs para alavancar a qualidade e precisão das recomendações. Os LLMs são modelos que possuem altas capacidades de compreensão de linguagem e de inferência de linguagem natural e, desde a apresentação do modelo GPT-3, foi evidenciado que o resultado de tarefas executadas por modelos deste tipo podem ter sua qualidade alavancada ao estruturar as prompts de interação sob pretextos que melhor extraiam sua capacidade in-context-learning. Técnicas de engenharia de prompt como as zero-shot, onde se descreve a tarefa em linguagem natural, foram desde então integradas no funcionamento de sistemas de recomendação, e este trabalho analisa uma abordagem onde se usa o LLM como recomendador, propondo uma análise comparativa dos impactos de aplicar quatro variantes de estratégias representativas a técnicas de engenharia de prompt distintas, em substituição a uma estratégia definida como baseline de comparação. Experimentos são feitos para diferentes combinações entre três LLMs em duas bases de dados distintas, apresentando resultados experimentais variados dentre as combinações modelo-estratégia, encontrando ganhos de até 17.76% em taxa de acerto de recomendação entre diferentes combinações, com métricas que em parte mostram superação em taxa de acerto contra o baseline, e que, por outro lado, mostram o baseline mantendo superioridade na qualidade da recomendação gerada.Item Verificação de deadlock e não-determinismo em ações de SysML 2.0(2021-07-15) Ribeiro Júnior, Amaury Tavares; Lima, Lucas Albertins de; http://lattes.cnpq.br/0465071050875729; http://lattes.cnpq.br/5978273506894399A crescente complexidade dos sistemas tem levado a um esforço crescente para validálos. Focar em iniciativas para criar ferramentas para a identificação de problemas o mais cedo possível vem sendo uma abordagem bastante desejada para minimizar custos e esforços. Alguns problemas como deadlock e nãodeterminismo podem se tornar cada vez mais difíceis de detectar devido à natureza concorrente e distribuída que os sistemas podem apresentar. A linguagem SysML 2.0 com sua notação para ações que vem sendo desenvolvida pela OMG pode ser usada para modelar comportamentos, mesmo os concorrentes, o que os torna adequados para descrever a dinâmica desses sistemas. Vários trabalhos propõem semântica formal a modelos SysML 1.0 para fins de verificação, incluindo verificação de deadlock. Mas nossa proposta é distinta no fato de fornecermos uma semântica formal para ações de SysML 2.0 que não apenas verifica a presença de deadlocks, mas também nãodeterminismo. Este último é geralmente negligenciado na literatura, embora possa ser considerado relevante em arquiteturas complexas de sistemas. Todo este processo de verificação é automatizado provendo também total rastreabilidade de volta para SysML 2.0 em caso de ser detectado problema no modelo. Portanto, o usuário não precisa entender ou manipular notações formais em qualquer parte do processo. Sendo assim, nossa principal contribuição é um verificador para analisar propriedades de ações de SysML 2.0, especificamente deadlock e nãodeterminismo, não exigindo nenhum conhecimento da semântica formal subjacente.Item Verificação de modelos comportamentais UML como um serviço habilitando a aplicação de métodos formais ocultos(2022-10-04) Cavalcanti, Paulo Henrique Nascimento; Lima, Lucas Albertins de; http://lattes.cnpq.br/0465071050875729; http://lattes.cnpq.br/7089611179473920Conforme os sistemas vão ficando mais complexos, mais esforço tem sido necessário para realizar validações sobre eles. Além da complexidade, o custo de correções também aumenta conforme os projetos avançam de fase, tornando essencial a detecção de erros nos estágios mais iniciais. Dentro da Model-Based Systems Engineering, a verificação de modelos é uma das possíveis abordagens para a solução do problema. Contudo, realizar tal verificação envolve muitas vezes a utilização de métodos formais. Estes métodos são complexos e nem todos os projetistas de sistemas têm conhecimento deles. Um outro ponto importante é que, dada a necessidade cada vez maior de suportar grandes cargas, é comum a utilização de concorrência nos sistemas. Essa natureza concorrente dos sistemas atuais traz consigo a possibilidade da inclusão de problemas como deadlock e não-determinismo, normalmente não verificados pelas ferramentas atuais, que muitas vezes também exigem licenças para sua utilização e oferecem poucas possibilidades de integração com outras ferramentas ou ambientes. Neste sentido, nosso trabalho utiliza-se do arcabouço construído em trabalhos anteriores parwa expandir a possibilidade da checagem de modelos através de microsserviços, gratuitos e de código aberto. Apesar de outros trabalhos já realizarem a verificação de propriedades em modelos UML, em sua maioria, eles dependem da instalação de ferramentas e permitem pouca ou nenhuma integração com outros sistemas. Sendo assim, nossa principal contribuição é a construção de uma arquitetura baseada em microsserviços para disponibilizar serviços de verificação de propriedades clássicas (deadlock e não-determinismo) para um subconjunto de modelos UML comportamentais, mais precisamente diagramas de atividade e de máquinas de estado.Item Verificação de propriedades de diagramas de atividade em um ambiente de modelagem aberto com suporte a rastreabilidade(2022-05-27) Silva Filho, Renato Cavalcanti Domingues da; Lima, Lucas Albertins de; http://lattes.cnpq.br/0465071050875729; http://lattes.cnpq.br/4996480197238824À medida que a tecnologia avança, os modelos e sistemas tornam-se cada vez mais complexos, assim como o esforço para verificá-los. À medida que um projeto avança, o custo de correção de erros aumenta exponencialmente. Assim, técnicas que auxiliem na identificação antecipada de tais erros são cada vez mais importantes. Dentre essas técnicas, a verificação de modelos tem se apresentado como uma abordagem interessante. No entanto, ela requer a manipulação de notações formais que são difíceis de operar por projetistas de sistemas. Portanto, a criação de ferramentas que abstraem os aspectos formais dessas abordagens de verificação tem se mostrado um caminho promissor. Outro aspecto relevante é que alguns problemas podem surgir devido à natureza concorrente desses sistemas. Problemas como deadlock e não determinismo estão bastante presentes nessa perspectiva. No entanto, a maioria das ferramentas atuais não tem a capacidade de lidar com esses problemas. Além disso, as que conseguem geralmente são ferramentas que exigem licenças pagas. Neste trabalho, expandimos a ferramenta criada em trabalhos anteriores para que ela possa ser utilizada em ambientes de modelagem abertos, sem deixar de ser de código aberto e não comercial. Nossa ferramenta agora tem a capacidade de verificar propriedades como deadlock e não determinismo de diagramas de atividades que são criados usando a linguagem SysML em um ambiente de modelagem aberto chamado OpenMBEE. Embora alguns outros trabalhos realizem a verificação de deadlock, poucos são aqueles que realizam a verificação de não-determinismo, menos ainda são aqueles que podem realizar ambos. Nossa ferramenta possui uma mecanização formal subjacente que nos permite realizar verificações automatizadas. Além disso, a ferramenta também traz a vantagem de que seus usuários não precisam entender ou manipular essa linguagem formal, pois fornecemos um módulo de rastreabilidade que rastreia os resultados da verificação formal de volta à notação do ambiente de modelagem, que é baseada no formato JSON. As principais contribuições deste trabalho são o aumento da expressividade da ferramenta e a adição de suporte para a verificação de diagramas de atividades de um ambiente de modelagem aberto. Avaliamos nossa abordagem usando um modelo real da indústria relacionado ao desenvolvimento de um Telescópio de Trinta Metros (TMT), que é fornecido pela comunidade OpenMBEE.Item Verificação de refinamento em diagramas de sequência com estruturas de controle(2019) Araújo, Daniel José Freire de; Lima, Lucas Albertins de; http://lattes.cnpq.br/0465071050875729; http://lattes.cnpq.br/5219541109924367A linguagem UML oferece diversos tipos de diagramas para modelagem de sistemas,entre os principais diagramas comportamentais está o diagrama de sequência. O diagrama de sequência pode ser utilizado para modelar casos de uso de sistemas deforma simples e visual. Contudo, a linguagem UML como um todo apresenta modelos informais que possuem verificações baseadas em experiência humana. Este trabalho é a continuação de um linha de pesquisa que tem o objetivo de formalizar diagramas de sequência UML e realizar verificações de refinamento entre diagramas. Aqui é proposta a versão inicial de uma ferramenta capaz de traduzir diagramas de sequência UML para uma especificação formal CSP e realizar a verificação de refinamentos através do verificador FDR4. O ponto diferencial deste trabalho é o processo de formalização de fragmentos combinados que representam estruturas de controle no contexto de diagramas de sequência, aqui serão abordados os fragmentos option, alternative, parallel e loop.Item Verifying deadlock and nondeterminism of UML/SysML state machines integrated with activities(2024-02-20) Ferreira, Diego Soares Pires; Lima, Lucas Albertins de; http://lattes.cnpq.br/0465071050875729; http://lattes.cnpq.br/9706450322426642This paper presents a framework for verifying deadlock and nondeterminism in UML/SysML state machines integrated with activities, addressing the critical need for automated checks in UML projects. The framework aims to provide architects and system designers with na automated way to model and verify properties in state machine diagrams integrated with activity diagrams, emphasizing the absence of deadlock and nondeterminism crucial aspects in critical systems. The framework is implemented as a plug-in for the Astah modeling environment, utilizing the Astah API to read the components used in state machine and activity diagrams. The translation of the diagram is performed into the formal CSP language and is verified using the FDR tool. In the case of deadlock or nondeterminism, an interactive counterexample is generated in the modeling platform, facilitating the identification of the reasons for the failure. The paper also discusses the developed semantics, a case study, and the functionalities of the framework. Additionally, it compares this work with related approaches and highlights the limitations and future directions for the framework.