Geração de especificação formal de sistemas a partir de documento de requisitos

Abstract

A escrita de requisitos, dentro do processo de desenvolvimento de sistemas, está sujeita a falhas, uma vez que os requisitos são escritos em Linguagem Natural, como Inglês, que pode conter definições ambíguas ou de difícil entendimento. Por outro lado, Linguagem Natural é a opção mais simples e flexível para se especificar um sistema, e é a linguagem de entendimento comum entre clientes e contratados. Desta forma, para minimizar a existência de erros nos documentos de requisitos, técnicas de validação com inspeção ou revisão de documentos são utilizadas. Entretanto, o custo de se realizar este tipo de validação é alto e sua eficácia é questionável; erros podem persistir. Além disso, requisitos escritos usando de linguagem natural são de difícil processamento, dificultando a geração de outros artefatos a partir do mesmo. Esta dissertação define uma estratégia que utiliza templates de especificação de casos de use e uma Linguagem Natural Controlada (LNC) para descrever requisitos. Os templates de casos de uso asseguram a estruturação correta do documento de requisitos e a LNC garante a exatidão da gramática do texto que especifica o comportamento do sistema. Foram criados dois templates de casos de uso, cada um com uma visão diferente do sistema. A visão mais abstrata se chama visão do usuário e a visão mais detalhada se chama visão de componentes. A partir dessa estruturação dos requisitos torna-se, possível definir uma estratégia de geração automática de uma especificação formal da aplicação em questão. A geração automática de especificação formal de sistemas reduz custo e necessidade de mão de obra especializada em projetos de desenvolvimento de software. Ou seja, uma vez que é possível realizar a geração automática do modelo formal de sistemas podemos fazer uso do mesmo na validação de propriedades do sistema. Além disso, artefatos como casos de teste e diagramas UML podem ser gerados a partir deste. Em particular, esta dissertação define uma estratégia para gerar modelos formais na álgebra de processo CSP a partir das duas visões de caso de uso, mantendo a consistência entre os artefatos. Também foi definida uma relação de refinamento entre os modelos gerados garantindo a consistência entre as visões. Finalmente, todo o processo foi automatizado através de ferramentas. Estas foram vali- dadas através de experimentos realizados no contexto de aplicação para celulares da Motorola, empresa parceira e financiadora do projeto de pesquisa com o CIn/UFPE