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

A new method is developed to determine a set of informative and refined interface assertions satisfied by functions that are represented by feed-forward neural networks. Neural networks have often been criticized for their low degree of comprehensibility.It is difficult to have confidence in software components if they have no clear and valid interface description. Precise and understandable interface assertions for a neural network based software component are required for safety critical applications and for theintegration into larger software systems. The interface assertions we are considering are of the form &quote if the input x of the neural network is in a region (alpha symbol) of the input space then the output f(x) of the neural network will be in the region (beta symbol) of the output space &quote and vice versa. We are interested in computing refined interface assertions, which can be viewed as the computation of the strongest pre- and postconditions a feed-forward neural network fulfills. Unions ofpolyhedra (polyhedra are the generalization of convex polygons in higher dimensional spaces) are well suited for describing arbitrary regions of higher dimensional vector spaces. Additionally, polyhedra are closed under affine transformations. Given a feed-forward neural network, our method produces an annotated neural network, where each layer is annotated with a set of valid linear inequality predicates. The main challenges for the computation of these assertions is to compute the solution of a non-linear optimization problem and the projection of a polyhedron onto a lower-dimensional subspace.