Bacharelado em Ciência da Computação (Sede)

URI permanente desta comunidadehttps://arandu.ufrpe.br/handle/123456789/6

Siglas das Coleções:

APP - Artigo Publicado em Periódico
TAE - Trabalho Apresentado em Evento
TCC - Trabalho de Conclusão de Curso

Navegar

Agora exibindo 1 - 4 de 4

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/5978273506894399
A 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.
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/7089611179473920
Conforme 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.
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.
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/5219541109924367
A 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.