Navegando por Assunto "Kernel Modeling Language (KerML)"
Agora exibindo 1 - 1 de 1
- Resultados por Página
- Opções de Ordenação
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.