Made available in DSpace on 2014-06-12T15:49:26Z (GMT). No. of bitstreams: 1
license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5)
Previous issue date: 2009 / 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
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufpe.br:123456789/1364 |
| Date | 31 January 2009 |
| Creators | FARIAS, Adalberto Cajueiro de |
| Contributors | MOTA, Alexandre Cabral |
| Publisher | Universidade Federal de Pernambuco |
| Source Sets | IBICT Brazilian ETDs |
| Language | English |
| Detected Language | Portuguese |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/doctoralThesis |
| Source | reponame:Repositório Institucional da UFPE, instname:Universidade Federal de Pernambuco, instacron:UFPE |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0023 seconds