Skip navigation
Please use this identifier to cite or link to this item: https://repositorio.ufpe.br/handle/123456789/19519
Title: Model checking requirements written in a controlled natural language
Authors: BARZA, Sérgio
Keywords: Linguagem Natural Controlada;Case Frames;Model Checker;Verificação de Modelos;NuSMV;Lógica Temporal;CTL
Issue Date: 25-Feb-2016
Publisher: Universidade Federal de Pernambuco
Abstract: No contexto de Engenharia de Software e modelos de processos, o primeiro passo que deve ser realizado para o desenvolvimento de um sistema é o levantamento e a análise de requisitos. É nesta fase onde Engenheiros de Requisitos identificam quais as necessidades de seus clientes através de técnicas como entrevistas e questionários, brainstorms, etc. Um dos artefatos de saída desta etapa é o Documento de Requisitos, onde são registradas, geralmente em linguagem natural, todas as funcionalidades que o sistema deve possuir, fornecendo aos desenvolvedores as informações necessárias para a construção do software e para a elaboração de seus testes. Uma vez que as linguagens naturais são passíveis de possuir ambiguidade, as interpretações dadas aos requisitos podem variar de acordo com quem as lê, gerando um efeito indesejado, pois os erros gerados pela má interpretação podem se propagar e levar a uma descobertatardiaecara. Umamaneiradealiaralegibilidadedalinguagemnaturaleaeliminação da sua ambiguidade é a adoção de uma Linguagem Natural Controlada, LNC. Além disso, por ela possuir uma estrutura gramatical concisa, é possível extrair, utilizando algumas teorias, informaçõessemânticas,denominadasCaseFrames,quetornampossívelomapeamentodaLNC para uma linguagem formal. Há várias ferramentas implementadas cujo principal objetivo é a geração de casos de teste a partir de requisitos de software descritos em LNC. Uma em partilar, NAT2TEST, realiza essa tarefa através de Case Frames. Este trabalho tem como objetivo realizar a tradução automática de Case Frames para modelos NuSMV. Utilizando verificação de modelos, é possível verificar se os requisitos, uma vez descritos em LNC, satisfazem um conjunto de propriedades escritas em Lógica Temporal. Essa abordagem pode detectar possíveis erros nos requisitos: uma vez detectado que o modelo gerado não satisfaz alguma(s) proprieade(s), a propagação de erros é evitada, diminuindo os custosdesoftware. Alémdageraçãodemodelos,opresentetrabalhotambémtemcomoobjetivo acriaçãodeumagramáticaparaespecificaçãodeumaLNC,bemcomoasuatraduçãoautomática para a Lógica Temporal CTL, utilizada como uma das linguagens de propriedades de NuSMV. O propósito desta LNC é permitir ao usuário descrever as propriedades do modelo e esconder do mesmo todo formalismo de CTL, bem como alguns detalhes técnicos que são internos a cada modelo. Em suma, os requisitos devem ser escritos de acordo com a CNL de NAT2TEST, onde são traduzidos para modelos NuSMV. As propriedades dos modelos a serem verificadas são descritas de acordo com a CNL desenvolvida neste trabalho, onde são traduzidas para CTL. Deste modo, NuSMV é capaz de realizar model checking utilizando essas traduções. Ilustramos as estratégias desenvolvidas neste trabalho através de um estudo de caso.
URI: https://repositorio.ufpe.br/handle/123456789/19519
Appears in Collections:Dissertações de Mestrado - Ciência da Computação

Files in This Item:
File Description SizeFormat 
SergioBarzaDissertation.pdf2.1 MBAdobe PDFView/Open


This item is protected by original copyright



This item is licensed under a Creative Commons License Creative Commons