Abstraction of infinite and communicating CSPZ processes

AUTOR(ES)
DATA DE PUBLICAÇÃO

2009

RESUMO

Esta tese trata de um problema muito comum em verificaÃÃo formal: explosÃo de estados. O problema desabilita a verificaÃÃo automÃtica de propriedades atravÃs da verificaÃÃo de modelos. Isto à superado pelo uso de abstraÃÃo de dados, em que o espaÃo de estados de umsistema à reduzido usandoumprincÃpio simples: descartando detalhes de tal forma que o espaÃo de estados torna-se finito exibindo ainda propriedades desejÃveis. Isso habilita o uso de verificacao de modelos, jà que o modelo mais simples (abstrato) pode ser usado no lugar do modelo original (concreto). Entretanto, abstraÃÃes podem perder propriedades jà que o nÃvel de precisÃo à degradado, para algumas propriedades. Abstrair tipos de dados Ã, normalmente, uma tarefa nÃo-trivial e requer uma profunda experiÃncia: o usuÃrio deve prover domÃnios abstratos, uma relacao matemÃtica entre os estados (concreto e abstrato), uma inicializaÃÃo abstrata, e uma versÃo abstrata para cada operaÃÃo. A abordagem proposta nesta tese transfere a maior parte dessa experiÃncia para um procedimento sistemÃtico que calcula relaÃÃes de abstraÃÃo. Essas relaÃÃes sÃo a base para as relaÃÃes matemÃticas entre os estados, como tambÃm suas imagens determinam os domÃnios abstratos (os valores de dados mÃnimos para preservar propriedades). TambÃm propomos meta-modelos para estabelecer como o sistema abstrato à inicializado e como operaÃÃes sÃo tornadas fechadas sob os domÃnios abstratos. Isso elimina o conhecimento requerido do usuÃrio para fornecer as versÃes abstratas para a inicializaÃÃo e operaÃÃes. Os meta-modelos garantem a correspondÃncia entre os sistemas concreto e abstrato. Assim, nÃs derivamos especificaÃÃes abstratasa partir de concretas de tal formaque a especificaÃÃo concreta à mais determinÃstica que a abstrata por construÃÃo. Esta à a idÃia por trÃs da teoria sobrejacente de nossa abordagem de abstraÃÃo de dados: refinamento de dados. A notaÃÃo adotada à CSPZâuma integraÃÃo formal das linguagens de especificaÃÃo CSP e Z. Uma especificaÃÃo CSPZ tem duas partes: uma parte comportamental (CSP) e outra de dados (Z). O procedimento de cÃlculo foca na parte de Z, mas os resultados sÃo usados na especificaÃÃo CSPZ por completo; isso segue da independÃncia de dados da parte de CSP (os dados nÃo podem afetar seu comportamento). Ao final, a verificaÃÃo automÃtica à obtida pela conversÃo da especificaÃÃo CSPZ em CSP puro e em seguida pelo reuso do verificador de modelos padrÃo de CSP. Nossa abordagem compreende as seguintes tarefas: nÃs extraÃmos a parte de Z de uma especificaÃÃo CSPZ (puramente sintÃtica), calculamos as relaÃÃes de abstraÃÃo (atravÃs de uma anÃlise sistemÃtica de predicados com uso de ferramenta de suporte), construÃmos as relaÃÃes matemÃticas entre os estados, os esquemas abstratos (definidos por meta-modelos), e realizamos um pÃs-processamento na especificaÃÃo abstrata. A Ãltima tarefa pode resultar em alguns ajustes nas relaÃÃes de abstraÃÃo. A novidade prÃtica e maior contribuiÃÃo de nossa abordagem à o cÃlculo sistemÃtico das das relaÃÃes de abstraÃÃo, que sÃo os elementos chave de todas abordagens de abstraÃÃo de dados que estudamos ao longo dos Ãltimos anos. O refinamento de dados entre o sistema produzido por nossa abordagem e o original (concreto) à a segunda contribuiÃÃo deste trabalho. O procedimento sistemÃtico à na verdade uma tÃcnica de anÃlise de predicado que usa as restriÃÃes sobre os dados para determinar seus valores mÃnimos que sÃo suficientes para preservar o comportamento do sistema. Isso evita a execuÃÃo (concreta ou simbÃlica) do sistema analisado. Os passos produzem mapeamentos que revelam alguns elementos cruciais: o espaÃo de estados abstrato e as relaÃÃes matemÃticas entre ele e o espaÃo de estados concreto. Essas relaÃÃes sÃo usadas para construir o sistema abstrato seguindo o formato estabelecido pelos meta-modelos. As limitaÃÃes de nossa abordagem sÃo tambÃm discutidas. NÃs aplicamos a abordagem a alguns exemplos tambÃm analisados por outras tÃcnicas da literatura. Discutimos tambÃm sobre trabalhos relacionados procurando destacar vantagens, desvantagens e aspectos complementares. Finalmente, apresentamos nossas conclusÃes e futuras direÃÃes para este trabalho

ASSUNTO(S)

data abstraction cspz data refinement especificaÃÃo formal mÃtodos formais refinamento de dados model checking engenharia de software process refinement abstraÃÃo de dados verificaÃÃo de modelos formal specification cspz refinamento de processos formal methods

ACESSO AO ARTIGO

Documentos Relacionados