Lima, Lucas Albertins deRibeiro Júnior, Amaury Tavares2023-02-172023-02-172021-07-15RIBEIRO JÚNIOR, Amaury Tavares. Verificação de deadlock e não-determinismo em ações de SysML 2.0. 2021. 61 f. Trabalho de Conclusão de Curso (Bacharelado em Ciência da Computação) – Departamento de Computação, Universidade Federal Rural de Pernambuco, Recife, 2021.https://repository.ufrpe.br/handle/123456789/3992A 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.61 f.poropenAccesshttps://creativecommons.org/licenses/by-nd/4.0/deed.pt_BRSistemas operacionais (Computadores)SysML (Computer science)Kernel Modeling Language (KerML)Verificação de deadlock e não-determinismo em ações de SysML 2.0bachelorThesisAtribuição-SemDerivações 4.0 Internacional (CC BY-ND 4.0)https://n2t.net/ark:/57462/001300000jxks