Navegando por Assunto "SysML (Computer science)"

Agora exibindo 1 - 2 de 2

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 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.