Modelling and Integrating Formal Models: from Test Cases and Requirements Models

AUTOR(ES)
DATA DE PUBLICAÇÃO

2007

RESUMO

A especificaÃÃo formal de um sistema ou seu modelo formal à uma forma abstrata de representar suas propriedades (caracterÃsticas). MÃtodos formais à um ramo da Engenharia de Software com foco no desenvolvimento de sistemas tendo uma especificaÃÃo formal do mesmo como ponto de partida. Inicialmente, as vantagens de usar notaÃÃes abstratas antes da implementaÃÃo do sistema estavam apenas relacionadas a um melhor entendimento do problema. Depois, tornou-se evidente que o uso de notaÃÃes formais abstratas combinadas com tÃcnicas de refinamentos de modelos reduzem o tempo de desenvolvimento e aumentam a qualidade do produto de sistema. A fase de testes à positivamente influenciada pelo uso de mÃtodos formais. Pesquisas tÃm sido desenvolvidas para melhorar a qualidade do sistema usando modelos formais e casos de teste. Uma vez verificadas as propriedades do sistema atravÃs de uma investigaÃÃo dos modelos formais, à possÃvel gerar casos de testes confiÃveis do sistema que serÃo colocados em aÃÃo para verificar a implementaÃÃo do sistema posteriormente. O campo de pesquisa que explora mÃtodos formais aplicados com testes de software à chamada de Testes Baseados em Modelos, ou simplesmente MBT, do inglÃs Model-Based Testing. PorÃm, hà situaÃÃes onde nÃo à possÃvel possuir o modelo abstrato definido a priori. Para superar tal restriÃÃo outras tÃcnicas surgiram para sintetizar um modelo abstrato seguindo apenas execuÃÃes do sistema. As execuÃÃes de um sistema contÃm comportamentos necessÃrios para construir um modelo abstrato desse sistema. Na literatura atual, tais tÃcnicas usadas para construir representaÃÃes abstratas seguindo execuÃÃes do sistema sÃo chamadas de Anti-Model- Based Testing ou simplesmented Anti-MBT. EntÃo, depois de construir um modelo abstrato, tÃcnicas de verificaÃÃo de modelos e geraÃÃo de casos de teste seguindo modelos formais podem ser aplicadas normalmente. O propÃsito desse trabalho à dar suporte a algumas tÃcnicas de MBT usadas no contexto da Motorola (CIn/BTC). Em tais tÃcnicas, as especificaÃÃes usadas para gerar casos de testes sÃo geralmente incompletas, inconsistentes, e Ãs vezes nÃo existem. Portanto, usando casos de testes reais do sistema à possÃvel criar novas especificaÃÃes e atualizar especificaÃÃes originais do sistema, e posteriormente gerar novos casos de teste usando comportamentos vÃlidos do sistema. Um outro problema detectado em nosso contexto à a distÃncia existente entre as representaÃÃes abstratas e reais. Um caso de teste abstrato, por exemplo, à Ãtil em tÃcnicas formais, mas nÃo à possÃvel executar um caso de teste diretamente no sistema. Dessa forma, para executar (manualmente ou automaticamente) os casos de teste gerados pelas tÃcnicas de MBT à necessÃrio primeiro traduzi-los em uma representaÃÃo real. Como resultado desse trabalho nÃs desenvolvemos tÃcnicas formais de modelagem do comportamento do sistema usando casos de teste. Os resultados das tÃcnicas de modelagem sÃo modelos formais especificados nos formalismos de LTS ou CSP. AlÃm disso, nÃs definimos uma tÃcnica de unificaÃÃo que une modelos formais gerados a partir de diferentes artefatos do sistema (requisitos e casos de teste). O resultado da tÃcnica de unificaÃÃo à um completo e unificado modelo do sistema, que contÃm informaÃÃes providas de diferentes artefatos. NÃs tambÃm definimos uma tÃcnica para traduzir casos de teste abstratos em representaÃÃes reais. Os casos de teste reais gerados por nossa tÃcnica de traduÃÃo sÃo usados no contexto do time de automaÃÃo de testes da Motorola, onde esse trabalho està inserido. Finalmente, nÃs automatizamos as tÃcnicas desenvolvidas usando linguagens de programaÃÃo e especificaÃÃes formais. O resultado à a ferramenta TCRev que à capaz de modelar, unificar e traduzir modelos do sistema. A ferramenta TCRev interage com o outras ferramentas externas, tais como FDR e FDR Explorer. Todos os resultados foram validados em estudos de casos reais executados no contexto da Motorola. Nessa dissertaÃÃo nÃs apresentamos um destes estudo de casos

ASSUNTO(S)

anti-mbt modelagem formal methods and models anti-model-based testing (anti-mbt) csp mÃtodos e modelos formais ciencia da computacao lts model-based testing (mbt) modelling lts teste baseado em modelos (mbt) unificaÃÃo e traduÃÃo de modelos unifying and translating models csp

ACESSO AO ARTIGO

Documentos Relacionados