Extração e verificação de modelos para sistemas em evolução

Abstract

Softwares estão sempre em constante evolução e atualização. Durante o ciclo de vida de um sistema, muitas modificações ocorrem, em relação às funcionalidades definidas em sua primeira especificação. É desejável que durante todo o ciclo de vida do sistema, o mesmo execute corretamente as funções para as quais foi projetado, mesmo na ocorrência de modificações. Para isto, o uso de verificação de modelos e teste de software tem desempenhado uma importante função na busca por melhor qualidade de software. Este trabalho busca utilizar técnicas de teste de software, verificação e extração de modelos para obter modelos os quais representem os comportamentos corretos de sistemas mesmo após modificações. O objetivo do trabalho é estabelecer um processo de validação de sistemas em relação a propriedades estabelecidas o qual permita não apenas verificar se as propriedades são preservadas em um modelo do sistema, mas também se o comportamento da implementação gerada corresponde ao definido no modelo. Utilizando uma modelagem manual a partir de um modelo pré-existente, é definida uma única propriedade, onde os comportamentos esperados do sistema em questão são englobados por esta propriedade. Após a modificação do código, um novo modelo é gerado com base no código do sistema e verificado contra a propriedade estabelecida anteriormente, a fim de validar se os comportamentos encontrados no código estão de acordo com a especificação do sistema. Validou-se o processo utilizando dois sistemas previamente codificados, onde um conjunto de alterações foi definido para cada um deles. Através do teste de software e extração de modelos, construiu-se um modelo com comportamentos que são encontrados na implementação de cada sistema. Com a verificação de modelos, a validade destes comportamentos foi comprovada ao realizar tal verificação contra um modelo o qual contém todos os comportamentos de um modelo cuja correção é previamente conhecida, além dos comportamentos adicionados pelas modificações. O processo proposto facilita o suporte para detecção de erros tanto nos modelos extraídos do código quanto nos modelos modificados manualmente, além de apresentar um modelo sem erros quando os comportamentos são todos corretos.

Software is always evolving and changing. During a software lifecycle, many updates are done regarding functions defined on early specification. It’s desirable that during all system lifecycle, all functions are correctly executed, even after software updates. In order to get that, using model checking and software testing has been useful to reach better software quality. This paper uses software testing, model checking and behavior model extraction techniques to obtain models to represent valid software behavior even after an update is done. The purpose of this paper is to get a system validation process against system properties where it’s possible to verify if a mode still represents system properties and to verify if the model behavior is the same as the behavior found on system implementation. Using manual modeling, only one property is defined, there expected system behavior are represented on this single property. After code update, a new model is generated based on the code and it is verified against the property, in order to verify if the code matches the system specification. Two system codes were used on this verification, where a set of updates were defined for each one of them. Using software testing and model extraction, a model was built with behavior found on each system. With model checking, behavior validation was done using this built model against a previous correct known model. This process makes bug detection easier on both extracted models as manually updated models. It also results on a model with no errors when all behaviors found are correct.