| dc.description | 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 | |
