Transformação automática de modelos UML para modelos markovianos parametrizados

Abstract

Na construção de produtos de software, é essencial a utilização de técnicas de verificação capazes de medir atributos de qualidade, para garantir que determinados padrões sejam alcançados. Dentre essas técnicas, se destaca o model checking, que recebe como entrada um modelo do sistema sob avaliação e a propriedade a ser avaliada; e verifica, de forma automática, se essa propriedade é satisfeita pelo modelo. No entanto, de maneira geral, a criação dos modelos utilizados nessa verificação ainda é feita manualmente e exige uma análise cuidadosa dos modelos comportamentais do sistema. Além disso, à medida que os produtos de software crescem, ela se torna mais trabalhosa e propensa a erros. Tendo em vista esse contexto, o presente trabalho visa solucionar o problema descrito através da automatização da transformação de modelos UML para modelos Markovianos parametrizados passíveis de análise. Para validar esse trabalho, serão considerados os casos da Beverage Machine e da BSN-SPL. ___________________________________________________________________________ ABSTRACT

When building software products, the use of verification techniques capable of measuring quality attributes is essential, in order to ensure that certain standards be met. Among these techniques, we emphasize model checking, which takes as input a model of the system under analysis and the property to be evaluated; and verifies, automatically, if this property is satisfied by the model. However, in general, models used in this type of verification are still built manually, which requires careful consideration of the system’s behavioral models. Moreover, as software products grow, this task requires more effort and becomes more error prone. Given this context, this work aims to solve the described issue by automating the transformation of UML models to parameterized Markov models that can be analyzed. To validate this work, the Beverage Machine and BSN-SPL cases will be considered.