GeraÃÃo mecanizada de abstraÃÃes seguras para especificaÃÃes CSP

AUTOR(ES)
DATA DE PUBLICAÇÃO

2008

RESUMO

Com a crescente demanda por diminuiÃÃo de custos no desenvolvimento de software, hà a necessidade de que os programas possam ser construÃdos de acordo com uma especificaÃÃo concordante com os requisitos do cliente. Nesse sentido, a especificaÃÃo formal pode ser utilizada para representar os requisitos do sistema.Uma vez que a especificaÃÃo formal foi desenvolvida, ela pode ser usada como base para investigar determinadas propriedades atravÃs de um verificador de modelos. Ele aceita modelos e propriedades que o sistema final deve satisfazer. EntÃo, a ferramenta gera uma resposta positiva se um dado modelo satisfaz uma dada especificaÃÃo ou um contra-exemplo, em caso negativo. O contra-exemplo detalha a situaÃÃo em que o modelo nÃo foi satisfeito.Mas na maioria das vezes, problemas do mundo real nÃo podem adotar essa abordagem porque usam domÃnios infinitos (levando ao problema da explosÃo de estados). Como forma de resolver essa questÃo, tÃcnicas de abstraÃÃo de dados sÃo empregadas para gerar especificaÃÃes abstratas finitas a partir de sistemas infinitos concretos. A linguagem de especificaÃÃo usada nesse trabalho à CSP (Communicating Sequential Processes). Ela à uma linguagem formal que à usada para descrever padrÃes de interaÃÃo em sistemas concorrentes. Uma das tÃcnicas de abstraÃÃo para especificaÃÃes possÃveis para essa linguagem à a abstraÃÃo segura de dados. Essa abstraÃÃo visa gerar um modelo abstrato a partir de um equivalente concreto que conserve as propriedades do sistema com respeito ao comportamento (modelo de traces) atravÃs da escolha de um dado do domÃnio abstrato para cada subconjunto do domÃnio concreto.O objetivo desse trabalho à propor um algoritmo para geraÃÃo mecanizada de abstraÃÃes seguras para sistemas CSP seqÃenciais com recursÃo simples. A especificaÃÃo do algoritmo à apresentada usando o paradigma funcional e elementos da linguagem Z, com a introduÃÃo da estratÃgia atravÃs de exemplos. No estudo de caso, o software Mathematica à usado para instanciar os valores das variÃveis e realizar a simplificaÃÃo dos predicados construÃdos a partir desse algoritmo.Com esse trabalho, à possÃvel gerar abstraÃÃes seguras de forma mecÃnica, e por conseqÃÃncia verificar o comportamento de modelos infinitos. Ademais, a geraÃÃo de dados de testes automÃtica tambÃm à beneficiada, jà que com o domÃnio abstrato dos dados à possÃvel percorrer todos os caminhos do sistema, gerando 100% de cobertura do modelo. Esse esforÃo à justificado pela importÃncia que a fase de testes tem para a qualidade do software. Estudos prÃvios mostraram que essa fase demanda mais de 50% do custo de seu desenvolvimento, e uma pesquisa detalhada realizada nos EstadosUnidos quantifica os altos impactos econÃmicos de uma infra-estrutura de software inadequada

ASSUNTO(S)

geraÃÃo de dados de testes csp ciencia da computacao abstraÃÃo de dados data test generation csp data abstraction

ACESSO AO ARTIGO

Documentos Relacionados