51 |
ScaleSem : model checking et web sémantique / ScaleSem : model checking and semantic webGueffaz, Mahdi 11 December 2012 (has links)
Le développement croissant des réseaux et en particulier l'Internet a considérablement développé l'écart entre les systèmes d'information hétérogènes. En faisant une analyse sur les études de l'interopérabilité des systèmes d'information hétérogènes, nous découvrons que tous les travaux dans ce domaine tendent à la résolution des problèmes de l'hétérogénéité sémantique. Le W3C (World Wide Web Consortium) propose des normes pour représenter la sémantique par l'ontologie. L'ontologie est en train de devenir un support incontournable pour l'interopérabilité des systèmes d'information et en particulier dans la sémantique. La structure de l'ontologie est une combinaison de concepts, propriétés et relations. Cette combinaison est aussi appelée un graphe sémantique. Plusieurs langages ont été développés dans le cadre du Web sémantique et la plupart de ces langages utilisent la syntaxe XML (eXtensible Meta Language). Les langages OWL (Ontology Web Language) et RDF (Resource Description Framework) sont les langages les plus importants du web sémantique, ils sont basés sur XML.Le RDF est la première norme du W3C pour l'enrichissement des ressources sur le Web avec des descriptions détaillées et il augmente la facilité de traitement automatique des ressources Web. Les descriptions peuvent être des caractéristiques des ressources, telles que l'auteur ou le contenu d'un site web. Ces descriptions sont des métadonnées. Enrichir le Web avec des métadonnées permet le développement de ce qu'on appelle le Web Sémantique. Le RDF est aussi utilisé pour représenter les graphes sémantiques correspondant à une modélisation des connaissances spécifiques. Les fichiers RDF sont généralement stockés dans une base de données relationnelle et manipulés en utilisant le langage SQL ou les langages dérivés comme SPARQL. Malheureusement, cette solution, bien adaptée pour les petits graphes RDF n'est pas bien adaptée pour les grands graphes RDF. Ces graphes évoluent rapidement et leur adaptation au changement peut faire apparaître des incohérences. Conduire l’application des changements tout en maintenant la cohérence des graphes sémantiques est une tâche cruciale et coûteuse en termes de temps et de complexité. Un processus automatisé est donc essentiel. Pour ces graphes RDF de grande taille, nous suggérons une nouvelle façon en utilisant la vérification formelle « Le Model checking ».Le Model checking est une technique de vérification qui explore tous les états possibles du système. De cette manière, on peut montrer qu’un modèle d’un système donné satisfait une propriété donnée. Cette thèse apporte une nouvelle méthode de vérification et d’interrogation de graphes sémantiques. Nous proposons une approche nommé ScaleSem qui consiste à transformer les graphes sémantiques en graphes compréhensibles par le model checker (l’outil de vérification de la méthode Model checking). Il est nécessaire d’avoir des outils logiciels permettant de réaliser la traduction d’un graphe décrit dans un formalisme vers le même graphe (ou une adaptation) décrit dans un autre formalisme / The increasing development of networks and especially the Internet has greatly expanded the gap between heterogeneous information systems. In a review of studies of interoperability of heterogeneous information systems, we find that all the work in this area tends to be in solving the problems of semantic heterogeneity. The W3C (World Wide Web Consortium) standards proposed to represent the semantic ontology. Ontology is becoming an indispensable support for interoperability of information systems, and in particular the semantics. The structure of the ontology is a combination of concepts, properties and relations. This combination is also called a semantic graph. Several languages have been developed in the context of the Semantic Web. Most of these languages use syntax XML (eXtensible Meta Language). The OWL (Ontology Web Language) and RDF (Resource Description Framework) are the most important languages of the Semantic Web, and are based on XML.RDF is the first W3C standard for enriching resources on the Web with detailed descriptions, and increases the facility of automatic processing of Web resources. Descriptions may be characteristics of resources, such as the author or the content of a website. These descriptions are metadata. Enriching the Web with metadata allows the development of the so-called Semantic Web. RDF is used to represent semantic graphs corresponding to a specific knowledge modeling. RDF files are typically stored in a relational database and manipulated using SQL, or derived languages such as SPARQL. This solution is well suited for small RDF graphs, but is unfortunately not well suited for large RDF graphs. These graphs are rapidly evolving, and adapting them to change may reveal inconsistencies. Driving the implementation of changes while maintaining the consistency of a semantic graph is a crucial task, and costly in terms of time and complexity. An automated process is essential. For these large RDF graphs, we propose a new way using formal verification entitled "Model Checking".Model Checking is a verification technique that explores all possible states of the system. In this way, we can show that a model of a given system satisfies a given property. This thesis provides a new method for checking and querying semantic graphs. We propose an approach called ScaleSem which transforms semantic graphs into graphs understood by the Model Checker (The verification Tool of the Model Checking method). It is necessary to have software tools to perform the translation of a graph described in a certain formalism into the same graph (or adaptation) described in another formalism
|
52 |
Hjälpmedel för hantering av BIM-modeller : Ett steg mot det ritningsfria projektet / Tools for managing BIM-models : A step towards the drawing free projectSvensson, Edgar, Turac, Jannis January 2013 (has links)
I dagens byggprocess läggs enormt mycket tid och resurser på hantering av pappersritningar och andra utskrivna dokument som är nödvändiga för att produktion och förvaltning ska fungera. Vid stora projekt kan det handla om tusentals olika ritningar och dokument som ska hanteras och dokumenteras vilket kan vara oerhört omständligt, inte minst när revideringar måste utföras. När ett BIM-projekt utförs idag så tappas en hel del av den information som modellen innehåller till följd av att det ska skrivas ut på en pappersritning, vilket i sin tur gör att mycket av informationen inte kommer till sin rätt. I dagsläget finns ett flertal programvaror med syftet att hantera BIM-modeller och andra dokument rent digitalt i datorn eller i surfplattan. Här har man kommit en bra bit på vägen mot ett ritningsfritt projekt men det finns mycket kvar att arbeta vidare med. Sweco Architects och NCC påbörjade under 2012 ett projekt vid namn ”Det ritningsfria projektet” som till en början delvis gått ut på att kartlägga vilka problem som kan uppkomma vid övergången till ett ritningsfritt projekt. Utifrån författarnas egna funderingar och dessa frågeställningar har examensarbetet formats. Med detta examensarbete vill författarna belysa att det i dagsläget finns ett flertal olika verktyg för hantering av BIM-modeller i byggprocessens olika led även om de inte är fullt utvecklade ännu. Genom att själva testa programmen utifrån given frågeställning kan svagheterna och styrkorna med programvaran kartläggas. Detta är viktigt för att vidare utveckling av programmen och de nya arbetssätt som dessa medför ska kunna ske. Förhoppningsvis leder examensarbetet till vidare arbete mot ett ritningsfritt projekt. / In the building process today, an enormous amount of time and resources are sacrificed to the management of paper drawings and other printed documents, which are all necessary for the production- and management-phases to work. In large projects this could mean thousands of drawings and documents that have to be managed and documented. This can be extremely tedious, especially when revisions need to be made. When BIM-projects are being performed today a lot of the information that the model contains are lost just because it has to be printed as a paper drawing. This makes it redundant to fill the model with that much information in the first place. As of today there are several software programs whose purpose are to handle BIM-models and other documents entirely digitally on the computer or on a tablet device. These software programs have contributed a lot to the movement towards the drawing free project, but there is still a long way to go. In 2012 Sweco Architects and NCC began a project named “Det ritningsfria projektet” which initially passed on to identify the problems faced in the transition to a drawing free project. Based on the author’s own thoughts and these identified problems the thesis has been formed. With this thesis the authors want to highlight that there are a number of tools for managing BIM-models today in the various stages of the building process, even though they all need further development. By testing the software available today based on the given issues the weaknesses and strengths can be highlighted and mapped. This is very important for further work with the software and the new work procedure that the software provides. Hopefully the thesis will lead to further work towards a drawing free project.
|
53 |
Polymorfní samočinně testovatelné obvody / Polymorphic Self-Checking CircuitsMazuch, Martin January 2008 (has links)
This Master's thesis deals with question of the development of self-checking polymorphic circuits. It deals with a traditional way of creating reliable and self-checking circuits, presenting basic principles and methods. Also a method of Cartesian Genetic Programming for development of combinational circuits is explained. This thesis describes concepts of polymorphic gates and circuits and their benefits in practical use. Some existing self-checking polymorphic circuits are presented and their self-checking capabilities are analyzed. A proposal of realization of a design system for self-checking polymorphic circuits is given. A design system has been built based on presented specification and an application allowing simulations and analysis of system-proposed solutions has been created. Variety of experiments have been performed at created system and several interesting solutions have been acquired. At the end, conclusion is given and benefits of MSc. project are discussed.
|
54 |
Automatic Hardening against Dependability and Security Software Bugs / Automatisches Härten gegen Zuverlässigkeits- und SicherheitssoftwarefehlerSüßkraut, Martin 15 June 2010 (has links) (PDF)
It is a fact that software has bugs. These bugs can lead to failures. Especially dependability and security failures are a great threat to software users. This thesis introduces four novel approaches that can be used to automatically harden software at the user's site. Automatic hardening removes bugs from already deployed software. All four approaches are automated, i.e., they require little support from the end-user. However, some support from the software developer is needed for two of these approaches. The presented approaches can be grouped into error toleration and bug removal. The two error toleration approaches are focused primarily on fast detection of security errors. When an error is detected it can be tolerated with well-known existing approaches. The other two approaches are bug removal approaches. They remove dependability bugs from already deployed software. We tested all approaches with existing benchmarks and applications, like the Apache web-server.
|
55 |
Utilização de aritmética bit-serial para redução de consumo de energia.FARIA, Roberto Medeiros de. 13 September 2017 (has links)
Submitted by Johnny Rodrigues (johnnyrodrigues@ufcg.edu.br) on 2017-09-13T17:59:11Z
No. of bitstreams: 1
Utilizacao de Aritmetica Bit-serial para Reducao de Consumo de Energia-Roberto Medeiros de Faria.pdf: 1661698 bytes, checksum: c7ef8816ca92eeeed7c8d271bc93933a (MD5) / Made available in DSpace on 2017-09-13T17:59:11Z (GMT). No. of bitstreams: 1
Utilizacao de Aritmetica Bit-serial para Reducao de Consumo de Energia-Roberto Medeiros de Faria.pdf: 1661698 bytes, checksum: c7ef8816ca92eeeed7c8d271bc93933a (MD5)
Previous issue date: 2014-12 / Hoje, uma das maiores preocupações, senão a maior, da indústria de semicondutores
é o desenvolvimento de chips com baixo consumo de energia. Existem vários fenômenos físicos causadores de consumo de energia em circuitos CMOS e várias técnicas que reduzem o consumo de energia de um chip. O objetivo principal desta pesquisa de mestrado foi investigar o quanto o consumo de energia estática em circuitos CMOS pode ser reduzido por meio do emprego de aritmética bit-serial em substituição à aritmética bit-paralela. A pesquisa está focada em circuitos construídos a partir de standard cells (células padrão), com aplicação em processamento de sinais, e para os quais o principal requisito não é o alto desempenho computacional, mas o baixo consumo de energia. A metodologia foi aplicada em um estudo de caso, utilizando-se para isto, simulações com o IP core SPVR. O SPVR é um verificador de identidade vocal implementado em um circuito dedicado capaz de ter desempenho suficiente para funcionar em tempo real, mesmo empregando um sinal de clock lento. Foi constatado na pesquisa, que o uso de aritmética bit-serial, em termos de diminuição de consumo estático, é vantajoso para somadores e circuitos de pequena complexidade. Porém, para sistemas de maior complexidade, esta substituição só é vantajosa em situações específicas de grande número de operações aritméticas e baixo uso de armazenamento em registradores paralelos. No caso inverso, as vantagens se perdem, porque embora haja diminuição de consumo estático, há um crescimento muito grande de consumo dinâmico. / Today, one of the biggest concerns, if not the largest, for the semiconductor industry is the development of chips with low power consumption. There are several physical
phenomena that cause power consumption in CMOS circuits and various techniques
that reduce the energy consumption of a chip. The main objective of this masters
research was to investigate how the static power consumption in CMOS circuits can be
reduced through the use of bit-serial arithmetic in place of bit-parallel arithmetic. The
research is focused on circuits built from standard cells, with application to signal
processing, and for which the main requirement is not the high computing
performance, but the low power consumption. The methodology was applied in a case
study, using for this, simulations with the SPVR IP core. The SPVR is a vocal identity
checker implemented in a dedicated circuit able to have enough performance to run in
real time, even employing a slow clock signal. It has been found in research that the
use of bit-serial arithmetic, in terms of reduction of static consumption, is
advantageous to adders and small circuit complexity. However, for more complex
systems, this substitution is only advantageous in specific situations of large number
of arithmetic operations and low storage usage in parallel registers. In the reverse
case, the advantages are lost, because although there are static consumption
decrease, there is a very large dynamic consumption growth.
|
56 |
Automatic Hardening against Dependability and Security Software BugsSüßkraut, Martin 21 May 2010 (has links)
It is a fact that software has bugs. These bugs can lead to failures. Especially dependability and security failures are a great threat to software users. This thesis introduces four novel approaches that can be used to automatically harden software at the user's site. Automatic hardening removes bugs from already deployed software. All four approaches are automated, i.e., they require little support from the end-user. However, some support from the software developer is needed for two of these approaches. The presented approaches can be grouped into error toleration and bug removal. The two error toleration approaches are focused primarily on fast detection of security errors. When an error is detected it can be tolerated with well-known existing approaches. The other two approaches are bug removal approaches. They remove dependability bugs from already deployed software. We tested all approaches with existing benchmarks and applications, like the Apache web-server.:1 Introduction 1
1.1 Terminology . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
1.2 Automatic Hardening . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
1.3 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
1.4 Theses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
2 Enforcing Dynamic Personalized System Call Models 9
2.1 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
2.2 SwitchBlade Architecture . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
2.3 System Call Model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
2.3.1 Personalization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
2.3.2 Randomization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.4 Model Learner . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
2.4.1 Problem: False Positives . . . . . . . . . . . . . . . . . . . . . . . . 22
2.4.2 Data-
ow-Based Learner . . . . . . . . . . . . . . . . . . . . . . . . 26
2.5 Taint Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
2.5.1 TaintCheck . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
2.5.2 Escaping Valgrind . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2.5.3 Replay of Requests . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2.6 Model Enforcement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
2.6.1 Loading the System Call Model . . . . . . . . . . . . . . . . . . . . 31
2.6.2 Checking System Calls . . . . . . . . . . . . . . . . . . . . . . . . . 31
2.7 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
2.7.1 Synthetic Exploits . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
2.7.2 Apache . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
2.7.3 Exploits . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
2.7.4 Micro Benchmarks . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
2.7.5 Model Size . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
2.7.6 Stateful Application . . . . . . . . . . . . . . . . . . . . . . . . . . 39
2.8 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
3 Speculation for Parallelizing Runtime Checks 43
3.1 Approach . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
3.1.1 Compiler Infrastructure . . . . . . . . . . . . . . . . . . . . . . . . 47
3.1.2 Runtime Support . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
3.2 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
3.3 Deterministic Replay and Speculation . . . . . . . . . . . . . . . . . . . . . 52
3.3.1 Interface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
3.3.2 Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
3.4 Switching Code Bases . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
3.4.1 Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
3.4.2 Integration with parexc chkpnt . . . . . . . . . . . . . . . . . . 58
3.4.3 Code Transformations . . . . . . . . . . . . . . . . . . . . . . . . . 59
3.4.4 Stack-local Variables . . . . . . . . . . . . . . . . . . . . . . . . . . 67
3.5 Speculative Variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
3.5.1 Interface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68
3.5.2 Deadlock Avoidance . . . . . . . . . . . . . . . . . . . . . . . . . . 69
3.5.3 Storage Back-ends . . . . . . . . . . . . . . . . . . . . . . . . . . . 69
3.6 Parallelized Checkers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69
3.6.1 Out-of-Bounds Checks . . . . . . . . . . . . . . . . . . . . . . . . . 70
3.6.2 Data Flow Integrity Checks . . . . . . . . . . . . . . . . . . . . . . 71
3.6.3 FastAssert Checker . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
3.6.4 Runtime Checking in STM-Based Applications . . . . . . . . . . . . 72
3.7 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
3.7.1 Performance . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
3.7.2 Checking Already Parallelized Applications . . . . . . . . . . . . . . 77
3.7.3 ParExC Overhead . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
3.8 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80
4 Automatically Finding and Patching Bad Error Handling 83
4.1 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84
4.2 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86
4.3 Learning Library-Level Error Return Values from System Call Error Injection 89
4.3.1 Components . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91
4.3.2 E cient Error Injection . . . . . . . . . . . . . . . . . . . . . . . . 91
4.3.3 Obtain OS Error Specification . . . . . . . . . . . . . . . . . . . . . 92
4.4 Finding Bad Error Handling . . . . . . . . . . . . . . . . . . . . . . . . . . 92
4.4.1 Argument Recording . . . . . . . . . . . . . . . . . . . . . . . . . . 93
4.4.2 Systematic Error Injection . . . . . . . . . . . . . . . . . . . . . . . 94
4.4.3 Static Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96
4.5 Fast Error Injection using Virtual Machines . . . . . . . . . . . . . . . . . 99
4.5.1 The fork Approach . . . . . . . . . . . . . . . . . . . . . . . . . . 100
4.5.2 Virtual Machines for Fault Injection . . . . . . . . . . . . . . . . . . 101
4.6 Patching Bad Error Handling . . . . . . . . . . . . . . . . . . . . . . . . . 102
4.6.1 Error Value Mapping . . . . . . . . . . . . . . . . . . . . . . . . . . 103
4.6.2 Preallocation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105
4.6.3 Patch Generation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106
4.7 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108
4.7.1 Measurements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109
4.8 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 115
5 Robustness and Security Hardening of COTS Software Libraries 117
5.1 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 118
5.2 Approach . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 119
5.3 Test Values . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 122
5.3.1 Ballista Type System . . . . . . . . . . . . . . . . . . . . . . . . . . 123
5.3.2 Meta Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 124
5.3.3 Feedback . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 125
5.3.4 Type Templates . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 126
5.3.5 Type Characteristics . . . . . . . . . . . . . . . . . . . . . . . . . . 128
5.3.6 Reducing the Number of Test Cases . . . . . . . . . . . . . . . . . . 128
5.3.7 Other Sources of Test Values . . . . . . . . . . . . . . . . . . . . . . 130
5.4 Checks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 130
5.4.1 Check Templates . . . . . . . . . . . . . . . . . . . . . . . . . . . . 131
5.4.2 Parameterized Check Templates . . . . . . . . . . . . . . . . . . . . 133
5.5 Protection Hypotheses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 134
5.5.1 Minimizing the Truth Table . . . . . . . . . . . . . . . . . . . . . . 134
5.5.2 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 135
5.6 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 136
5.6.1 Coverage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137
5.6.2 Autocannon as Dependability Benchmark . . . . . . . . . . . . . . 138
5.6.3 Protection Hypotheses . . . . . . . . . . . . . . . . . . . . . . . . . 139
5.7 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 140
6 Conclusion 143
6.1 Publications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 144
References 147
List of Figures 159
List of Tables 163
Listings 165
|
57 |
Metodika vkládání kontrolních prvků do číslicového systému / Methodology of Inserting Checkers into Digital SystemBartl, Michal January 2009 (has links)
The topics described in this diploma thesis belong to the area of digital systems testability analysis. Basic concepts as dependability, controllability, observability and testability are explained. Methods of raising testability and dependability of digital circuits are mentioned including the metrics which allow to evaluate testability parameters. Furthermore, the thesis describes the formal model of digital systems which introduces the implementing part of the thesis. Within this part, a program tool is demonstrated, which allows to identify the components of digital circuits and their function. The other function of the program tool is to create control circuits that check the correct function of such digital circuits.
|
58 |
Metodologie pro návrh číslicových obvodů se zvýšenou spolehlivostí / Methodology of highly reliable systems designStraka, Martin Unknown Date (has links)
In the thesis, a methodology alternative to existing methods of digital systems design with increased dependability implemented into FPGA is presented, new features which can be used in the implementation and testing of these systems are demonstrated. The research is based on the use of FPGA partial dynamic reconfiguration for the design of fault tolerant systems. In these applications, the partial dynamic reconfiguration can be used as a mechanism to correct the fault and recover the system after the fault occurrence. First, the general principles of diagnostics, testing and digital systems dependability are presented including a brief description of FPGA components and their architectures. Next, a survey of currently used methods and techniques used for the design and implementation of fault tolerant systems into FPGA is described, especially the methods used for fault detection and localization, their correction, together with the principles of evaluating fault tolerant systems design quality. The most important part of the thesis is seen in the description of the design methodology, implementation and testing of fault tolerant systems implemented into FPGAs which uses SRAMs as the configuration memory. First, the methodology of developing and automated checker components design for digital systems and communication protocols is presented. Then, a reference architecture of a dependable system implemented into FPGA is demonstrated including several fault tolerant architectures based on the use of partial dynamic reconfiguration as the mechanism of fault correction and the recovery from it. The principles of controlling the reconfiguration process are described together with the description of the test platform which allows to test and verify the design of fault tolerant systems based on the methodology presented in the thesis. The experimental results and the contribution of the thesis are discussed in the conclusions.
|
59 |
Domain Specific Modeling Support for ArCon / Stöd för domänspecifik modellering med ArConAzari, Leila January 2013 (has links)
One important phase in software development process is to create a design model of the system which follows all the architectural rules. Often the architectural rules are defined by the system architect and the system model is designed by the system designer. The architect defines the rules in a text file where no standard or pattern is followed. Therefore, there is always the risk of violating the architectural rules by the designer. So manual reviews on the system model should be done by the architect to ensure the system model is valid.In order to remove this manual checking which can be erroneous and time consuming ArCon (Architecture Conformance Checker) was developed by Combitech AB. ArCon is a tool which lets the architect define the architectural rules in the format of UML (Unified Modeling Language) models where the elements of the model have different meaning than the standard UML. ArCon can read this model and extract architectural rules from it and check the system model against those rules and then print all the rule violations.ArCon is an open source tool i.e. free for everyone to download and use. Currently, it supports Papyrus as the UML modeling tool. Papyrus is integrated to Eclipse platform and is a general purpose modeling tool. It supports users with all types of UML diagrams and elements.The idea for this thesis work was to implement a new feature for ArCon in order to facilitate the design process for system designers. The feature should provide the system designers only those types of elements which they are permitted to add to a specific fraction of the system model. The list of permitted element types should be extracted from the architecture model where all the architectural rules are defined in advance. This new support in ArCon was named Domain Specific Modeling (DSM) support.To evaluate the effect of DSM support on the system designers performance a few test sessions, called usability tests, were performed. The participants in the test sessions were a representative sample of software designers. After analyzing the data collected from the test sessions, the pros and cons of the new support were discovered. Furthermore, a few new ideas for enhancing DSM support were generated.
|
60 |
Metodologie pro návrh číslicových obvodů se zvýšenou spolehlivostí / Methodology of highly reliable systems designStraka, Martin January 2013 (has links)
In the thesis, a methodology alternative to existing methods of digital systems design with increased dependability implemented into FPGA is presented, new features which can be used in the implementation and testing of these systems are demonstrated. The research is based on the use of FPGA partial dynamic reconfiguration for the design of fault tolerant systems. In these applications, the partial dynamic reconfiguration can be used as a mechanism to correct the fault and recover the system after the fault occurrence. First, the general principles of diagnostics, testing and digital systems dependability are presented including a brief description of FPGA components and their architectures. Next, a survey of currently used methods and techniques used for the design and implementation of fault tolerant systems into FPGA is described, especially the methods used for fault detection and localization, their correction, together with the principles of evaluating fault tolerant systems design quality. The most important part of the thesis is seen in the description of the design methodology, implementation and testing of fault tolerant systems implemented into FPGAs which uses SRAMs as the configuration memory. First, the methodology of developing and automated checker components design for digital systems and communication protocols is presented. Then, a reference architecture of a dependable system implemented into FPGA is demonstrated including several fault tolerant architectures based on the use of partial dynamic reconfiguration as the mechanism of fault correction and the recovery from it. The principles of controlling the reconfiguration process are described together with the description of the test platform which allows to test and verify the design of fault tolerant systems based on the methodology presented in the thesis. The experimental results and the contribution of the thesis are discussed in the conclusions.
|
Page generated in 0.0431 seconds