Navegando por Assunto "Diagrama de atividade"

Agora exibindo 1 - 2 de 2

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.