Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico. Programa de Pós-Graduação em Ciência da Computação. / Made available in DSpace on 2012-10-24T03:23:03Z (GMT). No. of bitstreams: 1
262342.pdf: 660822 bytes, checksum: 20d4a5e1fe3ccf4f7e05dc3288b9c7a9 (MD5) / O escopo tradicional da veri¯ca»c~ao funcional foi ampliado com o surgimento dos °uxos de projeto em n¶³vel de sistema eletr^onico (ESL). Nesses °u-xos, logo ap¶os o particionamento hardware-software, a veri¯ca»c~ao precisa lidar com tipos abstratos de dados, com artefatos de implementa»c~ao e com a poss¶³vel n~ao-preserva»c~ao, no dispositivo sob veri¯ca»c~ao (DUV), da ordem dos comportamentos no modelo de refer^encia (golden model ). As t¶ecnicas existentes para veri¯ca»c~ao p¶os-particionamento est~ao limitadas pelo uso de heur¶³sticas (que colocam em risco as garantias de veri¯ca»c~ao) ou por abordagens black-box (que restringem a observabilidade). Este trabalho adota uma abordagem white-box e prop~oe uma nova t¶ecnica que opera sobre amostras de dados capturadas por monitores e armazenadas na forma dos assim-chamados logs. Para cada ponto a ser veri¯cado, inserem-se monitores espelhados: um no modelo de refer^encia, outro no DUV. A veri¯ca»c~ao autom¶atica dos logs ¶e formulada com um problema de casamento (matching) em um grafo bipartido. O problema cl¶assico foi modi¯cado para capturar n~ao apenas a compatibilidade de valores monitorados, mas tamb¶em a preced^encia de eventos, de forma a viabilizar o tratamento da n~ao-preserva»c~ao da ordem no DUV. A formula»c~ao adotada permitiu provar v¶arias propriedades, as quais
foram utilizadas como base te¶orica para determinar as garantias de veri¯ca»c~ao da t¶ecnica proposta. A implementa»c~ao dos monitores utilizou infra-estrutura pr¶e-existente baseada em re°ex~ao computacional. S~ao apresentados resultados experimentais que validam a formula»c~ao e os algoritmos propostos.
The traditional scope of functional veri¯cation has been extended
with the rise of electronic-system-level (ESL) design °ows. In those °ows, immediately after hardware-software partitioning, veri¯cation has to deal with abstract data, with implementation artifacts, and, possibly, with the non-preservation, by the device under veri¯cation (DUV), of the the order of behaviors at the golden model. Existing approaches are limited either by the use of greedy heuristics (jeopardizing veri¯cation guarantees) or by black-box approaches (impairing observability). This work adopts a white-box approach and proposes a new technique that operates on data samples captured by monitors and stored in the form of so-called logs. For each point to be veri¯ed, mirrored monitors are inserted: one at the golden model, another at the DUV. The automatic veri¯cation of the logs of a pair of mirrored monitors is cast as a bipartite graph matching problem. The
classical problem was modi¯ed to capture not only value compatibility, but also event precedence, so as to allow the treatment of the non-preserved event order at the DUV. The adopted formulation allowed us to prove several properties, which were used as stepping stones for determining the veri¯cation guarantees of the proposed technique. The implementation of monitors relied on pre-existing infrastructure based upon computational re°ection. Experimental results validate the formulation and the proposed algorithms.
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufsc.br:123456789/91869 |
| Date | January 2008 |
| Creators | Marcílio, Gabriel Maicon |
| Contributors | Universidade Federal de Santa Catarina, Santos, Luiz Claudio Villar dos |
| Publisher | Florianópolis, SC |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | Portuguese |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Format | xiii, 83 f.| il., tabs., grafs. |
| Source | reponame:Repositório Institucional da UFSC, instname:Universidade Federal de Santa Catarina, instacron:UFSC |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.002 seconds