| Summary: | Made available in DSpace on 2014-06-12T15:59:48Z (GMT). No. of bitstreams: 1
license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5)
Previous issue date: 2007 === 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
|
|---|
