51 |
Entwicklung und Evaluation eines Algorithmus zur initialen Konfiguration von Anwendungen in PCOMReinsch, Michael. January 2004 (has links)
Stuttgart, Univ., Diplomarb., 2004.
|
52 |
Problém splnitelnosti omezení a univerzální algebra / Constraint Satisfaction Problem and Universal AlgebraKazda, Alexandr January 2013 (has links)
The thesis consists of a collection of my contributions to universal algebra. Motivated by the Constraint Satisfaction Problem (CSP), we study the algebras of polymorphisms of relational structures. We begin by showing by an algebraic argument (and a bit of calculus) that random relational structures' CSP is almost always NP-complete. We then study digraphs with a Maltsev polymorphism, and conclude that such digraphs must also have a majority polymorphism. Next, we show how to use absorption tech- niques to prove that congruence modular reflexive digraphs must have an NU operation. We close our work by giving an algebraic proof of a result (first obtained by graph theorists) that 3-conservative relational structures with only unary and binary relations either define NP-complete CSP, or CSP for them can be solved by the local consistency algorithm. 1
|
53 |
Prédiction de la fiabilité de composants élecroniques de type WL-CSP soumis à des sollicitations mécaniques / Reliability study of electronic wafer-level chip-scale packaged components subjected to mechanical loadingsLe Coq, Cédric 07 July 2010 (has links)
L’étude présentée s’inscrit dans le cadre général de l’amélioration de la fiabilité mécanique des composants électroniques. Les composants de type WL-CSP (Wafer-Level Chip-Scale Package : boîtier aux dimensions comparables à celles de la puce) sont couramment utilisés dans les appareils nomades (par exemple les téléphones) et assurent de nombreuses fonctions. La tenue dans le temps de ces appareils passe par l’allongement de la durée de vie de leurs éléments. Ce sujet est une problématique complexe car la structure des composants peut varier selon les technologies employées et nécessite des essais spécifiques, qui consomment beaucoup de temps et de ressources.Un modèle numérique est développé afin d’accélérer le développement des boîtiers de ces composants et d’optimiser les ressources disponibles. Des essais de fiabilité sont menés sur le test de chute et un banc d’essai de flexion est mis en place. Les résultats de ces essais permettent de valider la simulation numérique et de mettre au point un modèle de fatigue.D’autre part, une campagne de caractérisation des matériaux permet de déterminer les propriétés mécaniques de la structure étudiée. La caractérisation concerne notamment les couches minces pour lesquelles les propriétés mécaniques sont fortement dépendantes de leurs conditions de dépôts.Ces éléments sont incorporés dans un modèle numérique incluant un certain nombre d’hypothèses. Le modèle est confronté à l’expérience pour déterminer les constantes d’un modèle de fatigue. Ensuite, la simulation et le modèle de fatigue sont utilisés conjointement pour évaluer l’influence de paramètres géométriques et matériaux sur la fiabilité des composants de type WL-CSP. / The work described in this report is related to the mechanical improvement of electronicdevices mechanical reliability. WL-CSP (Wafer-Level Chip-Scale Package) components are widely used in handheld devices and run many functions. The longevity increase of such adevice necessarily requires progresses in its components reliability. This subject is complexas the component structure can vary depending on the employed technologies. So, it requires time and ressources.A numerical model is developed to enhance the packages development as well as available resources. Reliability tests are performed on the drop-test bench and a bend-testbench is designed. These tests provide results to validate the numerical results and to establish a fatigue model.Aside from these tests, the component materials are characterized to determine the studied structure properties. It specifically concerns the thin layers for which mechanical properties strongly depends on the deposition process. All of this is incorporated in a numerical model which includes hypotheses. The model is compared with the experiments to determine fatigue model constants. Then, modeling and experiments are used together to evaluate material and geometrical parameters influence.
|
54 |
Systematic Development of Trustworthy Component-based SystemsTeixeira Ramos, Rodrigo 31 January 2011 (has links)
Made available in DSpace on 2014-06-12T15:54:23Z (GMT). No. of bitstreams: 2
arquivo6881_1.pdf: 1905257 bytes, checksum: 04bfefe5198fb11e1af4564f77de083a (MD5)
license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5)
Previous issue date: 2011 / Petróleo Brasileiro S.A. / Apesar de componentes serem tratados como unidades básicas de composição no desenvolvimento
baseado em componentes (CBD), para que eles obtenham um disseminado status de
serem facilmente conectados como peças de lego a integração de componentes precisa ser
cuidadosamente projetada, sistematizada e verificada; somente isto poderá garantir arquiteturas
confiáveis. Além dos argumentos gerais sobre redução de custo através de reuso, abordagens
CBD precisam oferecer uma interessante, e frutífera, oportunidade para o desenvolvimento de
sistemas críticos de alta qualidade e viável no contexto industrial.
Para alcançar esta meta, propomos neste trabalho uma abordagem sistematizada para a
construção de sistemas baseados em componentes (CBS) confiáveis. A abordagem foca na
realização de análises que consideram preocupações de engenharia no CBD. Ela se baseia em
um modelo de componentes que caracteriza os blocos de construção de nossa abordagem de
desenvolvimento, e que impõe as restrições necessárias para sua interação segura. Além disto,
definimos restrições de construção para o nosso modelo de componentes, baseadas em regras
de composição para componentes. Estas permitem verificar quando dois componentes são
compatíveis para trocarem informações.
As regras de composição compreendem um método sistematizado para preservar, por construção,
propriedades comportamentais em composições de componentes; em particular, focamos
na preservação de progresso local e da ausência de deadlock nas composições. Como
conseqüência, é possível prever o comportamento de uma vasta gama de CBS, antes de sua implementação,
com base em propriedades conhecidas do sistema. Em nossa abordagem, também
propomos alternativas de verificação mais amenas: a) predições de condições de composição
baseadas na análise de metadados de componentes; b) simplificações em verificações de componente
associados a estilos arquiteturais específicos.
Toda a abordagem é apoiada pela álgebra de processos CSP, que oferece modelos semânticos
que suportam uma vasta gama de verificações e comparações de processos. Além disto,
ilustramos a aplicação desta abordagem através de dois estudos de caso, que focam em diferentes
aspectos da nossa abordagem, e verificamos mecanicamente a preservação de propriedades
comportamentais de componentes na evolução dessas aplicações
|
55 |
Geração automática de casos de teste CSP orientada por propósitosde Carvalho Nogueira, Sidney January 2006 (has links)
Made available in DSpace on 2014-06-12T15:59:45Z (GMT). No. of bitstreams: 2
arquivo5536_1.pdf: 1197982 bytes, checksum: 344557c29e4105a048177410482f40ca (MD5)
license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5)
Previous issue date: 2006 / Conselho Nacional de Desenvolvimento Científico e Tecnológico / O processo de desenvolvimento de software está sujeito a inserção de erros diversos cuja presença
compromete a qualidade final dos produtos de software. Teste é uma atividade dinâmica
e bastante custosa dentro das várias empregadas pela Garantia da Qualidade de Software. O
objetivo de teste é demonstrar que um comportamento específico (cenário) de um sistema foi
bem (passou no teste) ou mal sucedido (falhou no teste), através de um veredicto.
Automação de testes visa tornar o processo mais ágil em atividades repetitivas e menos suscetível
a erros humanos. Existem várias abordagens de geração automática de teste, baseadas
na representação formal do comportamento do sistema, que empregam diferentes critérios de
seleção para os testes. Quando o objetivo do teste é focar na investigação de certas propriedades
ou comportamentos importantes do sistema a ser testado, podemos utilizar o critério de seleção
denominado propósito de teste (test purposes).
CSP (Communicating Sequential Processes) é uma notação formal bastante expressiva, uma
álgebra de processos útil para especificar comportamentos de sistemas concorrentes e distribuídos,
de hardware e software. Infelizmente, não existe na literatura abordagens para geração
de testes diretamente a partir de álgebras de processo como CSP. As abordagens existentes
utilizam a representação operacional (sistemas de transições rotuladas LTS) dos processos
CSP.
O objetivo deste trabalho é introduzir uma estratégia para geração automática de testes consistentes
(sound), elaborada inteiramente a partir da semântica denotacional de CSP (notação
de processos e modelos semânticos). É definida uma teoria de testes baseada na Teoria de Testes
de Tretmans. Um ponto comum entre estas teorias é que o conjunto de ações de entrada
e saída para especificações (alfabetos), implementações e testes são separados, de forma a definir
com precisão os veredictos para execução dos testes e a relação de conformidade entre
implementação e especificação. Adicionalmente, uma relação de conformidade denotada cspioco
é introduzida em termos de refinamentos de processos para determinar se o processo que
representa a implementação a ser testada está coerente com o comportamento do processo da
especificação. É apresentada, ainda, a estrutura e a utilização de uma ferramenta implementada
com o propósito de avaliar esta abordagem dentro do ambiente de teste de um projeto de pesquisa
que envolve uma cooperação entre o CIn-UFPE e a Motorola Industrial Limitada. Alguns
experimentos práticos foram realizados neste contexto
|
56 |
Extração automática de modelos CSP a partir de casos de usoARAÚJO, Renata Bezerra e Silva de 31 January 2011 (has links)
Made available in DSpace on 2014-06-12T16:00:36Z (GMT). No. of bitstreams: 2
arquivo6806_1.pdf: 3125791 bytes, checksum: d312e759783582d509c1403b479df91e (MD5)
license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5)
Previous issue date: 2011 / Conselho Nacional de Desenvolvimento Científico e Tecnológico / No ciclo de vida de desenvolvimento de software, especificação de requisitos é uma atividade
muito propensa a definições incorretas. Isto geralmente acontece porque esses documentos são
normalmente escritos em linguagem natural, tornando muito alta a possibilidade de introduzir
ambiguidades e interpretações errôneas. Por outro lado, a utilização de linguagem natural traz
simplicidade e flexibilidade ao se especificar requisitos, considerando que esta é uma notação
que pode ser compreendida tanto pelo cliente quanto pelo desenvolvedor.
Uma vez que projetos de software possuem documentos precisos, engenheiros de software
que tenham bom conhecimento em linguagens formais podem criar manualmente uma especificação
formal com o propósito de validar as propriedades do sistema. No entanto, esta criação
manual pode não cobrir todos os requisitos ou podem conter inconsistências. Desta forma, a
geração automática de modelos formais a partir de documento de requisitos parece ser uma boa
solução para este problema. Para alcançar este objetivo, os documentos de requisitos devem ser
simples, diretos, uniformes e sem ambuiguidades. Para que isto aconteça, Linguagens Naturais
Controladas (Controlled Natural Languages - CNL) são comumente utilizadas.
Este trabalho faz parte do projeto de Pesquisa e Desenvolvimento do CIn Brazil Test Center
(CInBTCRD), que é uma cooperação entre a Motorola e o Centro de Informática da Universidade
Federal de Pernambuco (CIn-UFPE). Em primeiro lugar, este trabalho propõe uma
linguagem restrita (CNL) para definir casos de uso contendo uma noção de estado, os quais
consideram dados de entrada, saída, guarda e atualização de variáveis, como um complemento
para a descrição textual. Depois disso, uma tradução automática dessa linguagem para a algebra
de processos CSP foi proposta, a fim de permitir a análise formal de requisitos e geração de
casos de teste. Finalmente, foi realizada a implementação e integração desta linguagem e sua
tradução para CSP em uma ferramenta conhecida como TaRGeT, cujo propósito é a geração
de casos de teste a partir de documentos de casos de uso que seguem um template padrão e
são escritos utilizando uma CNL. A TaRGeT original não era capaz de lidar com definições
de dados e as manipulações destes dados, e utiliza sistemas rotulados por transição (labelled
transition systems) em vez de CSP, como formalismo.
Para ilustrar as técnicas propostas neste trabalho, um estudo de caso foi realizado no ambiente
da Motorola, adaptando um exemplo de caso de uso real da indústria de modo a encaixá-lo
no nosso template. O documento de caso de uso considera situações de envio e recebimento de
SMS/MMS, contendo uma feature com 7 casos de uso, incluindo definições e manipulações de
dados, relacionamentos entre casos de uso e 6 fluxos alternativos. O CSP gerado contém 570
linhas de código e a verificação de suas propriedades foi checada com sucesso utilizando-se a
ferramenta FDR, um verificador de modelo para CSP
|
57 |
Corporate Social Responsibility och dess påverkan på lönsamhetAhmed, Aymann, Bjelica, Marina January 2017 (has links)
BAKGRUND: Företag fyller en stor roll i vårt samhälle eftersom de på många sätt är en viktig beståndsdel i att driva vårt samhälle mot vidare utveckling. För vidare hållbar utveckling krävs ansvarstagande av alla inblandade parter, men hur mycket ansvar ska företagen egentligen ta? Ska de ta ansvar för aspekter som exempelvis miljö och mänskliga rättigheter? Eller ska de endast fokusera på att vara så vinstmaximerande som möjligt? SYFTE: Syftet med denna uppsats är att undersöka sambandet mellan svenska företags rapporterade hållbarhetsredovisning och deras lönsamhet. METOD: För att kunna svara på syftet på bästa sätt valdes en kvantitativ metod med ett deduktivt synsätt. Tvärsnittsdesign valdes eftersom studien skulle undersöka sambandet mellan Corporate Social Responsibility och lönsamhet under en viss tidpunkt. Variabeln CSR operationaliseras genom användning av Folksams index för ansvarsfullt företagande och lönsamhet genom en justerad formel för Tobins Q. En regressionsanalys gjordes för att kunna undersöka korrelationen mellan CSR och lönsamhet. SLUTSATS: Sambandet mellan CSR och lönsamhet är neutralt, det vill säga statistiskt går det inte att påvisa något signifikant samband mellan CSR och lönsamhet för de studerade företagen i denna studie.
|
58 |
Identifying and exploiting symmetry for CSP refinement checkingMoffat, Nicholas January 2011 (has links)
No description available.
|
59 |
Kryptografické protokoly v praxi / Cryptographic protocols in practiceTruneček, Petr January 2009 (has links)
The purpose of this work was first to describe the requirements for cryptographic protocols. Furthermore, the classification of these protocols should have been made with specific examples given. The aim of the next part of the work was to describe the methods which are suitable for description and modeling of cryptographic protocols. This work also addressed the analysis of cryptographic protocols by appropriate analytical means. The CSP method for modeling of the cryptographic protocols was applied in the practical part. The Yahalom protocol was selected as a protocol suitable for modeling. Two analysis was made. The first analysis concerned the standard version of the Yahalom protocol, which was tested to the requirements of cryptographic properties of the secrecy and authenticity. The second analysis was based on the possibility of disclosure of the key, including counterexamples and traces given by FDR. The first analysis did not reveal any weakening, in terms of two cryptographic properties. To demonstrate the possibility of FDR, Yahalom protocol was modified in order to cause the situation when the disclosure of keys appears. FDR then finds the exact procedure that an intruder must make to get the possession of the key.
|
60 |
Process-based decomposition and multicore performance : case studies from StringologyStrauss, Marthinus David January 2017 (has links)
Current computing hardware supports parallelism at various levels. Conventional programming techniques, however, do not utilise efficiently this growing resource. This thesis seeks a better fit between software and current hardware while following a hardware-agnostic software development approach. This allows the programmer to remain focussed on the problem domain. The thesis proposes process-based problem decomposition as a natural way to structure a concurrent implementation that may also improve multicore utilisation and, consequently, run-time performance.
The thesis presents four algorithms as case studies from the domain of string pattern matching and finite automata.
Each case study is conducted in the following manner. The particular sequential algorithm is decomposed into a number of communicating concurrent processes. This decomposition is described in the process algebra CSP. Hoare's CSP was chosen as one of the best known process algebras, for its expressive power, conciseness, and overall simplicity.
Once the CSP-based process description has brought ideas to a certain level of maturity, the description is translated into a process-based implementation. The Go programming language was used for the implementation as its concurrency features were inspired by CSP. The performance of the process-based implementation is then compared against its conventional sequential version (also provided in Go).
The goal is not to achieve maximal performance, but to compare the run-time performance of an ``ordinary'' programming effort that focussed on a process-based solution over a conventional sequential implementation.
Although some implementations did not perform as well as others, some did significantly outperform their sequential counterparts. The thesis thus provides prima facie evidence that a process-based decomposition approach is promising for achieving a better fit between software and current multicore hardware. / Thesis (PhD)--University of Pretoria, 2017. / Computer Science / PhD / Unrestricted
|
Page generated in 0.0384 seconds