Made available in DSpace on 2014-06-12T16:00:36Z (GMT). No. of bitstreams: 2 arquivo6806_1.pdf: 3125791 bytes, checksum: d312e759783582d509c1403b479df91e (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2011 / Conselho Nacional de Desenvolvimento Científico e Tecnológico / No ciclo de vida de desenvolvimento de software, especificação de requisitos é uma atividade muito propensa a definições incorretas. Isto geralmente acontece porque esses documentos são normalmente escritos em linguagem natural, tornando muito alta a possibilidade de introduzir ambiguidades e interpretações errôneas. Por outro lado, a utilização de linguagem natural traz simplicidade e flexibilidade ao se especificar requisitos, considerando que esta é uma notação que pode ser compreendida tanto pelo cliente quanto pelo desenvolvedor. Uma vez que projetos de software possuem documentos precisos, engenheiros de software que tenham bom conhecimento em linguagens formais podem criar manualmente uma especificação formal com o propósito de validar as propriedades do sistema. No entanto, esta criação manual pode não cobrir todos os requisitos ou podem conter inconsistências. Desta forma, a geração automática de modelos formais a partir de documento de requisitos parece ser uma boa solução para este problema. Para alcançar este objetivo, os documentos de requisitos devem ser simples, diretos, uniformes e sem ambuiguidades. Para que isto aconteça, Linguagens Naturais Controladas (Controlled Natural Languages - CNL) são comumente utilizadas. Este trabalho faz parte do projeto de Pesquisa e Desenvolvimento do CIn Brazil Test Center (CInBTCRD), que é uma cooperação entre a Motorola e o Centro de Informática da Universidade Federal de Pernambuco (CIn-UFPE). Em primeiro lugar, este trabalho propõe uma linguagem restrita (CNL) para definir casos de uso contendo uma noção de estado, os quais consideram dados de entrada, saída, guarda e atualização de variáveis, como um complemento para a descrição textual. Depois disso, uma tradução automática dessa linguagem para a algebra de processos CSP foi proposta, a fim de permitir a análise formal de requisitos e geração de casos de teste. Finalmente, foi realizada a implementação e integração desta linguagem e sua tradução para CSP em uma ferramenta conhecida como TaRGeT, cujo propósito é a geração de casos de teste a partir de documentos de casos de uso que seguem um template padrão e são escritos utilizando uma CNL. A TaRGeT original não era capaz de lidar com definições de dados e as manipulações destes dados, e utiliza sistemas rotulados por transição (labelled transition systems) em vez de CSP, como formalismo. Para ilustrar as técnicas propostas neste trabalho, um estudo de caso foi realizado no ambiente da Motorola, adaptando um exemplo de caso de uso real da indústria de modo a encaixá-lo no nosso template. O documento de caso de uso considera situações de envio e recebimento de SMS/MMS, contendo uma feature com 7 casos de uso, incluindo definições e manipulações de dados, relacionamentos entre casos de uso e 6 fluxos alternativos. O CSP gerado contém 570 linhas de código e a verificação de suas propriedades foi checada com sucesso utilizando-se a ferramenta FDR, um verificador de modelo para CSP