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