subject:(PVS)

Universidade de Brasília

1. Rodrigo Borges Nogueira. Verificação formal de protocolos criptográficos : o caso dos protocolos em cascata.

Degree: 2008, Universidade de Brasília

URL: http://bdtd.bce.unb.br/tedesimplificado/tde_busca/arquivo.php?codArquivo=4267

►

Ensuring the security of cryptographic protocols is not a simple task. The Dolev-Yao model, proposed in the early 80s, is an important mathematical modeling method… (more)

▼

Ensuring the security of cryptographic protocols is not a simple task. The Dolev-Yao model, proposed in the early 80s, is an important mathematical modeling method of cryptographic protocols, enabling the analysis and verification of the safety of these protocols. But the analytical verification does not guarantee that implementations are not error-prone. Indeed, we have, in the history of protocols, a lot of examples with flaws detected even after a decade of its introduction. Thus, formal method approaches are very useful to ensure the security of protocol implementations. In this work, we use the PVS (Prototype Verification System) to specify and mechanically verify the safety of a protocol class in the Dolev- Yao model: the two-party cascade protocols. By verifying our specification, we have detected a few flaws in the original definitions and we have proposed more general concepts and lemmas.

Garantir a segurança de protocolos criptográficos não é uma tarefa simples. O modelo Dolev-Yao, proposto no início da década de 80, constitui uma importante metodologia matemática de modelagem de protocolos criptográficos, possibilitando a análise e verificação da segurança destes protocolos. Porém, a verificação analítica não garante isenção de erros nas implementações. Com efeito, existem vários exemplos de protocolos que foram considerados matematicamente seguros, mas com falhas descobertas até mesmo após mais de uma década de quando propostos. Dessa forma, as abordagens baseadas em métodos formais são de grande utilidade para garantir, efetivamente, a segurança de implementações destes protocolos. Neste trabalho, utilizamos um sistema de especificação e prova, o PVS (Prototype Verification System), para especificar e verificar mecanicamente a segurança de uma classe de protocolos no modelo Dolev-Yao: os Protocolos em Cascata para dois usuários. Fazendo isto, detectaram-se falhas definicionais na especificação matemática desta classe de protocolos e formularam se noções e lemas mais gerais que os inicialmente propostos.

Advisors/Committee Members: Mauricio Ayala Rincon, Anderson Clayton Alves Nascimento, Flávio Leonardo Cavalcanti de Moura.

Subjects/Keywords: PVS; PVS; CIENCIA DA COMPUTACAO; verificação formal; protocolos criptográficos; formal verification; cryptographic protocols

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

Nogueira, R. B. (2008). Verificação formal de protocolos criptográficos : o caso dos protocolos em cascata. (Thesis). Universidade de Brasília. Retrieved from http://bdtd.bce.unb.br/tedesimplificado/tde_busca/arquivo.php?codArquivo=4267

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Chicago Manual of Style (16^th Edition):

Nogueira, Rodrigo Borges. “Verificação formal de protocolos criptográficos : o caso dos protocolos em cascata.” 2008. Thesis, Universidade de Brasília. Accessed January 21, 2021. http://bdtd.bce.unb.br/tedesimplificado/tde_busca/arquivo.php?codArquivo=4267.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

MLA Handbook (7^th Edition):

Nogueira, Rodrigo Borges. “Verificação formal de protocolos criptográficos : o caso dos protocolos em cascata.” 2008. Web. 21 Jan 2021.

Vancouver:

Nogueira RB. Verificação formal de protocolos criptográficos : o caso dos protocolos em cascata. [Internet] [Thesis]. Universidade de Brasília; 2008. [cited 2021 Jan 21]. Available from: http://bdtd.bce.unb.br/tedesimplificado/tde_busca/arquivo.php?codArquivo=4267.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Council of Science Editors:

Nogueira RB. Verificação formal de protocolos criptográficos : o caso dos protocolos em cascata. [Thesis]. Universidade de Brasília; 2008. Available from: http://bdtd.bce.unb.br/tedesimplificado/tde_busca/arquivo.php?codArquivo=4267

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Universidade de Brasília

2. André Luiz Galdino. Uma formalização da teoria de reescrita em linguagem de ordem superior.

Degree: 2008, Universidade de Brasília

URL: http://bdtd.bce.unb.br/tedesimplificado/tde_busca/arquivo.php?codArquivo=4014

►

Theories for Abstract Reduction Systems (ARS) and Term Rewriting Systems (TRS) in the proof assistant PVS (Prototype Verification System) called ars and trs, respectively, we… (more)

▼

Theories for Abstract Reduction Systems (ARS) and Term Rewriting Systems (TRS) in the proof assistant PVS (Prototype Verification System) called ars and trs, respectively, we developed. The ars theory built on the PVS library for binary relations, contains specifications of notions such as reduction, confluence, normal forms, and non basic concepts such as Noetherianity. On the other hand, the trs theory built on the ars theory and the PVS library for finite sequences, contains a formalization to deal with the structure of terms as well as formalizations of non-trivial notions of TRS. Theories ars and trs were developed with the main goal of providing the necessary concepts and definitions to deal with the Theory of Rewriting in general. In other words, ars and trs contain elements that conform a solid basis to formalize properties of the Theory of Rewriting in PVS. To make sure that the goal was achieved well-known and non-trivial results were formalised; among these, the correctness of the principle of noetherian induction, the Newmans Lemma, the Commutation Lemma and the Knuth-Bendix Critical Pair Theorem. Apart from being a basis for formalization of properties of the Theory of Rewriting, in general, the formalization presented is highlighted by: 1. the use a higherorder language, which allows for the specification of high-order properties naturally, 2. for their high-level of abstraction, which allows for the specification properties in an almost geometric style, as desirable in Rewriting Theory, and 3. the high degree of control allowed by PVS in the development of proofs.

Teorias para Sistemas Abstratos de Redução (ARS) e Sistemas de Reescrita de Termos (TRS) no assistente de provas PVS (Prototype Verification System) chamadas ars e trs, respectivamente, foram desenvolvidas. A teoria ars, construída com base na teoria para relações binárias do PVS, contém especificações de noções tais como redução, confluência, formas normais, e conceitos não básicos como por exemplo noeterianidade. Por outro lado, a teoria trs, construída com base na teoria ars e a teoria para seqüências finitas encontrada na biblioteca do PVS, contém uma formalização para lidar com a estrutura dos termos, assim como, formalizações de noções não triviais de TRS. As teorias ars e trs foram desenvolvidas com o objetivo de agregar os conceitos e as definições necessários para lidar com a Teoria de Reescrita, em geral. Em outras palavras, ars e trs contém elementos que formam uma base sólida para formalizar propriedades da Teoria de Reescrita em PVS. Para certificar-se de que o objetivo foi alcançado vários resultados bem conhecidos e não triviais foram formalizados; dentre estes, destacam-se a correção do princípio de indução Noeteriana, o Lema de Newman, os Lemas de Comutação e o Teorema dos Pares Críticos de Knuth-Bendix. Além de constituir uma base para formalização de propriedades da Teoria de Reescrita, em geral, a formalização apresentada se destaca por: 1. utilizar uma linguagem de orderm superior, a qual permite expressar naturalmente…

Advisors/Committee Members: Elaine Gouvea Pimentel, Edward Hermann Haeusler, Mauricio Ayala Rincon, Marcelo Finger, César Muñoz.

Subjects/Keywords: MATEMATICA; Teoria de Reescrita; PVS: pares críticos; formalização

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

Galdino, A. L. (2008). Uma formalização da teoria de reescrita em linguagem de ordem superior. (Thesis). Universidade de Brasília. Retrieved from http://bdtd.bce.unb.br/tedesimplificado/tde_busca/arquivo.php?codArquivo=4014

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Chicago Manual of Style (16^th Edition):

Galdino, André Luiz. “Uma formalização da teoria de reescrita em linguagem de ordem superior.” 2008. Thesis, Universidade de Brasília. Accessed January 21, 2021. http://bdtd.bce.unb.br/tedesimplificado/tde_busca/arquivo.php?codArquivo=4014.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

MLA Handbook (7^th Edition):

Galdino, André Luiz. “Uma formalização da teoria de reescrita em linguagem de ordem superior.” 2008. Web. 21 Jan 2021.

Vancouver:

Galdino AL. Uma formalização da teoria de reescrita em linguagem de ordem superior. [Internet] [Thesis]. Universidade de Brasília; 2008. [cited 2021 Jan 21]. Available from: http://bdtd.bce.unb.br/tedesimplificado/tde_busca/arquivo.php?codArquivo=4014.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Council of Science Editors:

Galdino AL. Uma formalização da teoria de reescrita em linguagem de ordem superior. [Thesis]. Universidade de Brasília; 2008. Available from: http://bdtd.bce.unb.br/tedesimplificado/tde_busca/arquivo.php?codArquivo=4014

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

3. Santos, Sara Lisboa Santos Fonseca. Estudo da alteração dimensional de um silicone de adição após um método de desinfecção e esterilização.

Degree: 2014, RCAAP

URL: https://www.rcaap.pt/detail.jsp?id=oai:comum.rcaap.pt:10400.26/13828

►

Dissertação para obtenção do grau de Mestre no Instituto Superior de Ciências da Saúde Egas Moniz

Objectivos: Avaliar o efeito da desinfecção e da autoclavagem,… (more)

▼

Dissertação para obtenção do grau de Mestre no Instituto Superior de Ciências da Saúde Egas Moniz

Objectivos: Avaliar o efeito da desinfecção e da autoclavagem, na estabilidade do Imprint 4 Penta Putty (3M ESPETM) e análise dos respectivos modelos de gesso. Materiais e Métodos: As 90 amostras de silicone foram confeccionados com uma matriz metálica, de acordo com a norma ISO 4823:2000 para materiais de impressão elastoméricos. A viabilidade das amostras foi confirmada com a presença da linha de 75micra e foram constituídos 9 grupos. Os grupos 1, 2 e 3 correspondem ao Controlo a diferentes tempos (0 horas; 24h e 1semana); os grupos 4, 5 e 6 foram sujeitos a imersão durante 10 minutos em hipoclorito de sódio a 5,25% e medidos nos diferentes tempos (0 horas; Tm; 24h e 1semana) e ainda os grupos 7, 8 e 9 submetidos autoclavagem a 134ºC durante 40 minutos também medidos nos diferentes tempos. Após a última medição, as amostras foram passadas a gesso tipo IV onde foi confirmado a reprodutibilidade da linha de 75 micra e também medida a estabilidade dimensional. As medições foram feitas com o Interferómetro de Michelson. Resultados: Na analisa da alteração dimensional das amostras de silicone verificou-se que nos grupos de Controlo e Hipoclorito não existem alterações estatisticamente significativas ao longo do tempo (p>0,05). Nos grupos Autoclave conclui-se que, excepto os valores obtidos em Tm e 24h, todos os outros apresentam diferenças significativas de alteração (p<0,05). Para os modelos de gesso, nenhum dos grupos apresentou alterações estatisticamente significativas ao longo do tempo (p>0,05). Conclusão: Tanto para os silicones como para modelos de gesso, as maiores alterações deram-se nos grupos Autoclave. As amostras de silicone devem ser passadas a gesso 24h depois da impressão. As alterações encontradas nos silicones são maiores do que as encontradas nos gessos, havendo assim uma aproximação destes à matriz inicial.

Advisors/Committee Members: Maurício, Paulo Durão.

Subjects/Keywords: Alterações dimensionais; PVS; Desinfecção; Esterilização; Interferómetro de Michelson

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

Santos, S. L. S. F. (2014). Estudo da alteração dimensional de um silicone de adição após um método de desinfecção e esterilização. (Thesis). RCAAP. Retrieved from https://www.rcaap.pt/detail.jsp?id=oai:comum.rcaap.pt:10400.26/13828

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Chicago Manual of Style (16^th Edition):

Santos, Sara Lisboa Santos Fonseca. “Estudo da alteração dimensional de um silicone de adição após um método de desinfecção e esterilização.” 2014. Thesis, RCAAP. Accessed January 21, 2021. https://www.rcaap.pt/detail.jsp?id=oai:comum.rcaap.pt:10400.26/13828.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

MLA Handbook (7^th Edition):

Santos, Sara Lisboa Santos Fonseca. “Estudo da alteração dimensional de um silicone de adição após um método de desinfecção e esterilização.” 2014. Web. 21 Jan 2021.

Vancouver:

Santos SLSF. Estudo da alteração dimensional de um silicone de adição após um método de desinfecção e esterilização. [Internet] [Thesis]. RCAAP; 2014. [cited 2021 Jan 21]. Available from: https://www.rcaap.pt/detail.jsp?id=oai:comum.rcaap.pt:10400.26/13828.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Council of Science Editors:

Santos SLSF. Estudo da alteração dimensional de um silicone de adição após um método de desinfecção e esterilização. [Thesis]. RCAAP; 2014. Available from: https://www.rcaap.pt/detail.jsp?id=oai:comum.rcaap.pt:10400.26/13828

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Brno University of Technology

4. Hodes, Vít. Výpočet viditelnosti v 3D bludišti: Visibility Determination in 3D Maze.

Degree: 2019, Brno University of Technology

URL: http://hdl.handle.net/11012/56450

► This work is about solving the visibility problem in the environment of simple 3D maze by means of BSP tree and PVS computation between leaves.… (more)

Subjects/Keywords: PVS; BSP; portál; potenciální; sada; viditelnosti; binární; dělení; prostoru; OpenGL; bludiště; 3D; uzel; list; strom; PVS; BSP; portal; potential; visibility; set; binary; space; partitioning; OpenGL; maze; 3D; leaf; node; tree

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

Hodes, V. (2019). Výpočet viditelnosti v 3D bludišti: Visibility Determination in 3D Maze. (Thesis). Brno University of Technology. Retrieved from http://hdl.handle.net/11012/56450

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Chicago Manual of Style (16^th Edition):

Hodes, Vít. “Výpočet viditelnosti v 3D bludišti: Visibility Determination in 3D Maze.” 2019. Thesis, Brno University of Technology. Accessed January 21, 2021. http://hdl.handle.net/11012/56450.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

MLA Handbook (7^th Edition):

Hodes, Vít. “Výpočet viditelnosti v 3D bludišti: Visibility Determination in 3D Maze.” 2019. Web. 21 Jan 2021.

Vancouver:

Hodes V. Výpočet viditelnosti v 3D bludišti: Visibility Determination in 3D Maze. [Internet] [Thesis]. Brno University of Technology; 2019. [cited 2021 Jan 21]. Available from: http://hdl.handle.net/11012/56450.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Council of Science Editors:

Hodes V. Výpočet viditelnosti v 3D bludišti: Visibility Determination in 3D Maze. [Thesis]. Brno University of Technology; 2019. Available from: http://hdl.handle.net/11012/56450

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

5. Gilbert, Frédéric. Extending higher-order logic with predicate subtyping : application to PVS : Extension de la logique d'ordre supérieur avec le sous-typage par prédicats : application à PVS.

Degree: Docteur es, Mathématiques. Logique et fondements de l'informatique, 2018, Sorbonne Paris Cité

URL: http://www.theses.fr/2018USPCC009

►

Le système de types de la logique d'ordre supérieur permet d'exclure certaines expressions indésirables telles que l'application d'un prédicat à lui-même. Cependant, il ne suffit… (more)

▼

Le système de types de la logique d'ordre supérieur permet d'exclure certaines expressions indésirables telles que l'application d'un prédicat à lui-même. Cependant, il ne suffit pas pour vérifier des critères plus complexes comme l'absence de divisions par zéro. Cette thèse est consacrée à l’étude d’une extension de la logique d’ordre supérieur appelée sous-typage par prédicats (predicate subtyping), dont l'objet est de rendre l'attribution de types aussi expressive que l'attribution de prédicats. A partir d'un type A et d'un prédicat P(x) de domaine A, le sous-typage par prédicats permet de construire un sous-type de A, noté {x : A | P(x)}, dont les éléments sont les termes t de type A tels que P(t) est démontrable. Le sous-typage par prédicats est au coeur du système PVS.Ce travail présente la formalisation d'un système minimal incluant le sous-typage par prédicats, appelé PVS-Core, ainsi qu'un système de certificats vérifiables pour PVS-Core. Ce deuxième système, appelé PVS-Cert, repose sur l'introduction de termes de preuves et de coercions explicites. PVS-Core et PVS-Cert sont munis d'une notion de conversion correspondant respectivement à l'égalité modulo beta et à l'égalité modulo beta et effacement des coercions, choisi pour établir une correspondance simple entre les deux systèmes.La construction de PVS-Cert est semblable à celle des PTS (Pure Type Systems) avec paires dépendantes et PVS-Cert peut être muni de la notion de beta-sigma-réduction utilisée au coeur de ces systèmes. L'un des principaux théorèmes démontré dans ce travail est la normalisation forte de la réduction sous-jacente à la conversion et de la beta-sigma-réduction. Ce théorème permet d'une part de construire un algorithme de vérification du typage (et des preuves) pour PVS-Cert et d'autre part de démontrer un résultat d'élimination des coupures, utilisé à son tour pour prouver plusieurs propriétés importantes des deux systèmes étudiés. Par ailleurs, il est également démontré que PVS-Cert est une extension conservative du PTS lambda-HOL, et qu'en conséquence PVS-Core est une extension conservative de la logique d'ordre supérieur.Une deuxième partie présente le prototype d'une instrumentation de PVS pour produire des certificats de preuve. Une troisième et dernière partie est consacrée à l'étude de liens entre logique classique et constructive avec la définition d'une traduction par double négation minimale ainsi que la présentation d'un algorithme de constructivisation automatique des preuves.

The type system of higher-order logic allows to exclude some unexpected expressions such as the application of a predicate to itself. However, it is not sufficient to verify more complex criteria such as the absence of divisions by zero. This thesis is dedicated to the study of an extension of higher-order logic, named predicate subtyping, whose purpose is to make the assignment of types as expressive as the assignment of predicates. Starting from a type A and a predicate P(x) of domain A, predicate subtyping allows to build a subtype of A, denoted…

Advisors/Committee Members: Dowek, Gilles (thesis director), Kirchner, Florent (thesis director).

Subjects/Keywords: Prototype verification system (PVS); Logique d'ordre supérieur; Sous-typage par prédicats; Prototype verification system (PVS); Higher-order logic; Predicate subtyping; Type theory; Proof theory

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

Gilbert, F. (2018). Extending higher-order logic with predicate subtyping : application to PVS : Extension de la logique d'ordre supérieur avec le sous-typage par prédicats : application à PVS. (Doctoral Dissertation). Sorbonne Paris Cité. Retrieved from http://www.theses.fr/2018USPCC009

Chicago Manual of Style (16^th Edition):

Gilbert, Frédéric. “Extending higher-order logic with predicate subtyping : application to PVS : Extension de la logique d'ordre supérieur avec le sous-typage par prédicats : application à PVS.” 2018. Doctoral Dissertation, Sorbonne Paris Cité. Accessed January 21, 2021. http://www.theses.fr/2018USPCC009.

MLA Handbook (7^th Edition):

Gilbert, Frédéric. “Extending higher-order logic with predicate subtyping : application to PVS : Extension de la logique d'ordre supérieur avec le sous-typage par prédicats : application à PVS.” 2018. Web. 21 Jan 2021.

Vancouver:

Gilbert F. Extending higher-order logic with predicate subtyping : application to PVS : Extension de la logique d'ordre supérieur avec le sous-typage par prédicats : application à PVS. [Internet] [Doctoral dissertation]. Sorbonne Paris Cité; 2018. [cited 2021 Jan 21]. Available from: http://www.theses.fr/2018USPCC009.

Council of Science Editors:

Gilbert F. Extending higher-order logic with predicate subtyping : application to PVS : Extension de la logique d'ordre supérieur avec le sous-typage par prédicats : application à PVS. [Doctoral Dissertation]. Sorbonne Paris Cité; 2018. Available from: http://www.theses.fr/2018USPCC009

McMaster University

6. Pang, Linna. An Engineering Methodology for the Formal Verification of Function Block Based Systems.

Degree: PhD, 2015, McMaster University

URL: http://hdl.handle.net/11375/18127

►

Many industrial control systems use programmable logic controllers (PLCs) since they provide a highly reliable, off-the-shelf hardware platform. On the programming side, function blocks (FBs)… (more)

▼

Many industrial control systems use programmable logic controllers (PLCs) since they provide a highly reliable, off-the-shelf hardware platform. On the programming side, function blocks (FBs) are reusable PLC components that can be composed to implement the required system behaviour. A higher quality system may be realized if the FBs are pre-certified to be compliant with an international standard such as IEC 61131-3. Unfortunately, the set of programming notations defined in IEC 61131-3 lack well-defined formal semantics. As a result, tool vendors and users of PLCs may have inconsistent interpretations of the expected system behaviour. To address this issue, we propose an engineering method for formally verifying the conformance of candidate implementations of FBs (and their compositions) to their high-level, input-output requirements. The proposed method is sufficiently general to handle FBs supplied by IEC 61131-3, and industrial FB applications involving real-time requirements. Our method involves several steps. First, we use tabular expressions to ensure the completeness and disjointness of the requirements for the FB. Second, we formalize the candidate implementation(s) of the FB in question. Third, we state and prove theorems regarding the consistency and correctness of the FB. All three steps are performed using the Prototype Verification Systems (PVS) proof assistant. As a first case study, we apply our approach to the IEC 61131-3 standard to examine the entire library of FBs and their supplied implementations described in structured text (ST) and function block diagrams (FBDs). As a second case study, we apply our approach to two realistic sub-systems taken from the nuclear domain. Applying the proposed method, we identified three kinds of issues: ambiguous behavioural descriptions, missing assumptions, and erroneous implementations. Furthermore, we suggest solutions to these issues.

Thesis

Doctor of Philosophy (PhD)

A formal verification approach for the function block based control systems

Advisors/Committee Members: Wassyng, Alan, Lawford, Mark, Computing and Software.

Subjects/Keywords: Critical systems; Formal specification; Formal verification; Function blocks; Tabular expressions; IEC 61131-3; PVS

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

Pang, L. (2015). An Engineering Methodology for the Formal Verification of Function Block Based Systems. (Doctoral Dissertation). McMaster University. Retrieved from http://hdl.handle.net/11375/18127

Chicago Manual of Style (16^th Edition):

Pang, Linna. “An Engineering Methodology for the Formal Verification of Function Block Based Systems.” 2015. Doctoral Dissertation, McMaster University. Accessed January 21, 2021. http://hdl.handle.net/11375/18127.

MLA Handbook (7^th Edition):

Pang, Linna. “An Engineering Methodology for the Formal Verification of Function Block Based Systems.” 2015. Web. 21 Jan 2021.

Vancouver:

Pang L. An Engineering Methodology for the Formal Verification of Function Block Based Systems. [Internet] [Doctoral dissertation]. McMaster University; 2015. [cited 2021 Jan 21]. Available from: http://hdl.handle.net/11375/18127.

Council of Science Editors:

Pang L. An Engineering Methodology for the Formal Verification of Function Block Based Systems. [Doctoral Dissertation]. McMaster University; 2015. Available from: http://hdl.handle.net/11375/18127

INP Toulouse

7. Aubin, Antoine. Optimisation des opérations de séchage dans la chaîne de fabrication du PVC en poudre. Expérimentation, simulation et modélisation. : Optimization of drying operations in powder PVC production line. Experimentation, simulation and modeling.

Degree: Docteur es, Génie des procédés et de l'environnement, 2014, INP Toulouse

URL: http://www.theses.fr/2014INPT0048

►

Lors de la production du PVC en poudre, après l’étape de polymérisation en suspension, on obtient une bouillie constituée d’un mélange de grains macroporeux de… (more)

▼

Lors de la production du PVC en poudre, après l’étape de polymérisation en suspension, on obtient une bouillie constituée d’un mélange de grains macroporeux de taille comprise entre 100 et 200 μm et d’eau. L’étape de centrifugation permet la séparation de la phase liquide exprimable et la production d’un milieu poreux humide appelé « gâteau ». La teneur en eau du gâteau ainsi formé est de 30 % de la masse du produit anhydre. Le séchage du gâteau de filtration se fait dans un séchoir Flash (séchoir pneumatique) couplé à un séchoir à lit fluidisé. Cette opération, très gourmande en énergie et donc très impactante en termes d’émission de Gaz à Effet de Serre (GES), représente 30% du coût de fabrication et 50% des émissions de CO2. Ce travail, réalisé dans le cadre d’une collaboration avec le groupe INEOS ChlorVinyls, est consacrée à l’étude de l’étape de séchage thermique, et à la réalisation d’outils expérimentaux et théoriques permettant d’optimiser le fonctionnement et de réduire la consommation énergétique de cette étape. Dans ce but, l’étude du séchage du PVC est réalisée à l’échelle d’une particule isolée d’une part, et à l’échelle du procédé industriel d’autre part. La détermination expérimentale de la cinétique de séchage est effectuée en immergeant une quantité de produit humide (gâteau de filtration) dans un lit fluidisé de grosses particules inertes et chaudes (billes de verre), et permet d’étudier l’influence de différents paramètres sur la cinétique d’évaporation. Les résultats ont montré que cette cinétique est limitée par les processus d’évaporation à l’intérieur et à la surface des particules. Du point de vue théorique, un modèle dont le principe repose sur les bilans de matière et de chaleur à l’échelle du grain de PVC, couplés aux bilans sur le séchoir à lit fluidisé, a été élaboré. La comparaison des résultats de ce modèle avec les résultats expérimentaux a permis de vérifier la validité de la loi cinétique ainsi établie. Finalement, cette loi a été intégrée dans un modèle simulant le séchoir pneumatique industriel. Les résultats théoriques sont comparés à des mesures réalisées sur un séchoir pneumatique industriel équipé de capteurs de pression, d’humidité et de température. Les résultats de cette étude ont permis de proposer une nouvelle stratégie de régulation du séchoir pneumatique ainsi que des modifications du procédé, ne nécessitant pas d’investissement. L’ensemble de ces propositions a permis de réduire d’environ 30% la consommation énergétique pour un rendement de séchage équivalent.

In a PVC powder production line, the step of suspension polymerization produces a mixture of macroporous particles and water, called “slurry”. The mean particle size varies between 100 and 200 µm. The centrifugation step eliminates most of water content and produces a wet porous medium called “cake”. The water content of the cake is about 30% of the dry product mass. Drying operations take place in a Flash dryer (pneumatic dryer) coupled with a fluidized bed dryer. These operations, which consume a lot of…

Advisors/Committee Members: Hemati, Mehrdji (thesis director).

Subjects/Keywords: PVC; Séchage; Fluidisation; Cinétique; Séchoir pneumatique; PVS; Drying; Fluidization; Kinetic; Pneumatic dryer

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

Aubin, A. (2014). Optimisation des opérations de séchage dans la chaîne de fabrication du PVC en poudre. Expérimentation, simulation et modélisation. : Optimization of drying operations in powder PVC production line. Experimentation, simulation and modeling. (Doctoral Dissertation). INP Toulouse. Retrieved from http://www.theses.fr/2014INPT0048

Chicago Manual of Style (16^th Edition):

Aubin, Antoine. “Optimisation des opérations de séchage dans la chaîne de fabrication du PVC en poudre. Expérimentation, simulation et modélisation. : Optimization of drying operations in powder PVC production line. Experimentation, simulation and modeling.” 2014. Doctoral Dissertation, INP Toulouse. Accessed January 21, 2021. http://www.theses.fr/2014INPT0048.

MLA Handbook (7^th Edition):

Aubin, Antoine. “Optimisation des opérations de séchage dans la chaîne de fabrication du PVC en poudre. Expérimentation, simulation et modélisation. : Optimization of drying operations in powder PVC production line. Experimentation, simulation and modeling.” 2014. Web. 21 Jan 2021.

Vancouver:

Aubin A. Optimisation des opérations de séchage dans la chaîne de fabrication du PVC en poudre. Expérimentation, simulation et modélisation. : Optimization of drying operations in powder PVC production line. Experimentation, simulation and modeling. [Internet] [Doctoral dissertation]. INP Toulouse; 2014. [cited 2021 Jan 21]. Available from: http://www.theses.fr/2014INPT0048.

Council of Science Editors:

Aubin A. Optimisation des opérations de séchage dans la chaîne de fabrication du PVC en poudre. Expérimentation, simulation et modélisation. : Optimization of drying operations in powder PVC production line. Experimentation, simulation and modeling. [Doctoral Dissertation]. INP Toulouse; 2014. Available from: http://www.theses.fr/2014INPT0048

McMaster University

8. Deng, Honghan. Formal Verification of FPGA Based Systems.

Degree: MASc, 2011, McMaster University

URL: http://hdl.handle.net/11375/11188

►

In design verication, although simulation is still a widely used verication technique in FPGA design, formal verication is obtaining greater acceptance as the complexity… (more)

Subjects/Keywords: Formal method; PVS; Hardware verification; FPGA; HDL.; Digital Circuits; Hardware Systems; Other Computer Engineering; Digital Circuits

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

Deng, H. (2011). Formal Verification of FPGA Based Systems. (Masters Thesis). McMaster University. Retrieved from http://hdl.handle.net/11375/11188

Chicago Manual of Style (16^th Edition):

Deng, Honghan. “Formal Verification of FPGA Based Systems.” 2011. Masters Thesis, McMaster University. Accessed January 21, 2021. http://hdl.handle.net/11375/11188.

MLA Handbook (7^th Edition):

Deng, Honghan. “Formal Verification of FPGA Based Systems.” 2011. Web. 21 Jan 2021.

Vancouver:

Deng H. Formal Verification of FPGA Based Systems. [Internet] [Masters thesis]. McMaster University; 2011. [cited 2021 Jan 21]. Available from: http://hdl.handle.net/11375/11188.

Council of Science Editors:

Deng H. Formal Verification of FPGA Based Systems. [Masters Thesis]. McMaster University; 2011. Available from: http://hdl.handle.net/11375/11188

University of Colorado

9. Su, Zhenbi. Numerical Evaluating Pulmonary Hemodynamics and RV Afterload in Pulmonary Arterial Hypertension Progression.

Degree: PhD, Mechanical Engineering, 2010, University of Colorado

URL: https://scholar.colorado.edu/mcen_gradetds/10

► Pulmonary arterial hypertension (PAH) is an important determinant of morbidity and mortality in children with congenital heart disease. Previous and current investigations on pulmonary… (more)

▼ Pulmonary arterial hypertension (PAH) is an important determinant of morbidity and mortality in children with congenital heart disease. Previous and current investigations on pulmonary vascular stiffness (PVS), input impedance and right ventricular (RV) power have found PVS to be an important contributor to flow energy power, and thus, afterload. However these investigations focus on the analysis of clinical data, which requires long term observation and inspection of a great number of individuals, whose clinical pathogenesis may not be the same. It is difficult if not impossible to vary stiffness/resistance in an example system within clinical or animal studies, and it is difficult to separate the contributing effects of stiffness and flow from clinical results. Here we proposed numerical artery models based on the clinically and experimentally measured parameters for children and calves, to determine if they could offer clinically relevant hemodynamic information on the circulation. With non-specific on pulmonary vascular structure information, we can create a realistic computational simulation environment, which can be used to test our theories regarding various associations between hemodynamic and mechanical variables in the human or animal pulmonary vasculature. These models could be useful in helping evaluate the efficacy of newly designed therapies that may target particular components of RV afterload such as proximal vascular stiffness or distal vasoconstriction, and as a tool to examine disease progression, and others. Through these types of studies, we will obtain a better understanding of how structural adaptations that occur in pulmonary vascular disease affect hemodynamics, vascular function and subsequently impedance and right ventricular (RV) afterload. Several achievements are obtained: 1) effect of these experimental measurable parameters on hemodynamics when PAH progresses to worsen; 2) hemodynamics play an important role in progressing PAH; 3) provide possible prediction of WSS, impedance, RV power and pulsatility of hemodynamics based on easily obtained measurable parameters; 4) decreasing or reversing proximal vascular remodeling can provide treatment of PAH as well as decrease mean pressures (mPAP). Overall, these results suggest a close association between PVS, PVR and hemodynamics, that hemodynamics may play an important role in progressing PAH, and that treatments should target decreasing or reversing upstream vascular remodeling in addition to decreasing mean pressures. Advisors/Committee Members: Robin Shandas, Kendall S. Hunter, Wei Tan.

Subjects/Keywords: Pulmonary Arterial Hypertension (PAH); pulmonary vascular resistance (PVR); pulmonary vascular stiffness (PVS); right ventricular (RV) power; Vasodilator treatment; Biomechanical Engineering

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

Su, Z. (2010). Numerical Evaluating Pulmonary Hemodynamics and RV Afterload in Pulmonary Arterial Hypertension Progression. (Doctoral Dissertation). University of Colorado. Retrieved from https://scholar.colorado.edu/mcen_gradetds/10

Chicago Manual of Style (16^th Edition):

Su, Zhenbi. “Numerical Evaluating Pulmonary Hemodynamics and RV Afterload in Pulmonary Arterial Hypertension Progression.” 2010. Doctoral Dissertation, University of Colorado. Accessed January 21, 2021. https://scholar.colorado.edu/mcen_gradetds/10.

MLA Handbook (7^th Edition):

Su, Zhenbi. “Numerical Evaluating Pulmonary Hemodynamics and RV Afterload in Pulmonary Arterial Hypertension Progression.” 2010. Web. 21 Jan 2021.

Vancouver:

Su Z. Numerical Evaluating Pulmonary Hemodynamics and RV Afterload in Pulmonary Arterial Hypertension Progression. [Internet] [Doctoral dissertation]. University of Colorado; 2010. [cited 2021 Jan 21]. Available from: https://scholar.colorado.edu/mcen_gradetds/10.

Council of Science Editors:

Su Z. Numerical Evaluating Pulmonary Hemodynamics and RV Afterload in Pulmonary Arterial Hypertension Progression. [Doctoral Dissertation]. University of Colorado; 2010. Available from: https://scholar.colorado.edu/mcen_gradetds/10

10. Martinoia, Diego. Proving Correctness within an Access Control Evaluation Framework.

Degree: 2013, University of Illinois – Chicago

URL: http://hdl.handle.net/10027/10132

► This thesis presents the proofs developed to demonstrate correctness of a case study within the Access Control Evaluation Framework (ACEF). ACEF is a theoretical framework… (more)

Subjects/Keywords: Access Control; Formal Methods; Correctness; PVS; Verification

…study ACEF case studies within the Prototype Verification System (PVS). PVS was… …can easily be translated into other systems. Within PVS I also formalized the intuitive… …using PVS, or another generic theorem prover, to prove ACEF correctness can be challenging: as… …study. After that, I’ll describe the choices taken in the development of the PVS structure and… …details, he can consult the original full paper on ACEF [11] . CHAPTER 3 PVS…

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

Martinoia, D. (2013). Proving Correctness within an Access Control Evaluation Framework. (Thesis). University of Illinois – Chicago. Retrieved from http://hdl.handle.net/10027/10132

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Chicago Manual of Style (16^th Edition):

Martinoia, Diego. “Proving Correctness within an Access Control Evaluation Framework.” 2013. Thesis, University of Illinois – Chicago. Accessed January 21, 2021. http://hdl.handle.net/10027/10132.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

MLA Handbook (7^th Edition):

Martinoia, Diego. “Proving Correctness within an Access Control Evaluation Framework.” 2013. Web. 21 Jan 2021.

Vancouver:

Martinoia D. Proving Correctness within an Access Control Evaluation Framework. [Internet] [Thesis]. University of Illinois – Chicago; 2013. [cited 2021 Jan 21]. Available from: http://hdl.handle.net/10027/10132.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Council of Science Editors:

Martinoia D. Proving Correctness within an Access Control Evaluation Framework. [Thesis]. University of Illinois – Chicago; 2013. Available from: http://hdl.handle.net/10027/10132

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Halmstad University

11. Holm, Anders. CATIA V5 SOM KONCEPTGENERERINGSVERKTYG.

Degree: Business and Engineering (SET), 2007, Halmstad University

URL: http://urn.kb.se/resolve?urn=urn:nbn:se:hh:diva-771

► Att ta fram en ny bilmodell är ett tidskrävande och omfattande arbete där många olika kunskapsområden måste samspela. En del i utvecklingsprocessen som får… (more)

▼ Att ta fram en ny bilmodell är ett tidskrävande och omfattande arbete där många olika kunskapsområden måste samspela. En del i utvecklingsprocessen som får allt större betydelse är designarbetet. Om bilens utförande och design inte tilltalar konsumenterna innebär detta låga försäljningssiffror och därmed förlorade intäkter för företaget. Det huvudsakliga syftet med detta arbete är att grundligt undersöka om och hur CAD-programmet Catia V5 med modulen Imagine & Shape (IMA) skulle kunna användas på Volvo Car Corporations designavdelning (PVS). Syftet är också att granska vad en implementering av Catia V5 med IMA-modulen skulle innebära för produktutvecklingsprocessen, samt att undersöka vilka som skulle kunna använda sig av programmet. För att undersöka hur Catia V5:s IMA-modul skulle kunna fungera på PVS har vi i samarbete med designstuderande Pontus Ny modellerat en konceptbil, komplett med exteriör, instrumentpanel, mittkonsol, ratt, stolar, baksäte, fälgar och hjul. Vi har även modellerat en växelspak och en backspegel som först har tagits fram i Alias, vilket har möjliggjort en jämförelse mellan Alias och Catia V5:s IMA-modul. Modellerna har sedan utvärderats genom enkäter med uppföljande intervjuer. Urvalsguppen utgörs av ett antal anställda hos PVS som har haft möjlighet att sätta sig in i IMA-modulen. Respondenterna uppgav fördelar som anmärkningsvärd snabbhet vid framtagning av 3D-modeller i de fall där ytan inte behöver vara perfekt. Dock krävs stor erfarenhet för att skapa en bra renhet och ytjämnhet vid stora ytor. Samtliga involverade i detta projekt anser också att Catia V5 med IMA-modulen skulle kunna fungera som ett konceptgenereringsverktyg i ett tidigt skede. Att använda IMA-modulen i den första förberedande fasen skulle enligt vår mening innebära tidsbesparingar, eftersom användaren snabbt kan genomföra förändringar på en modell redan på möten. I dagsläget måste en Alias-modellör samla in alla ändringar, genomföra dessa snabbast möjligt och därefter bestämma en tid för ett nytt möte då alla inblandade kan närvara, vilket sällan är enkelt. IMA-modulen skulle även kunna vara ett bra hjälpmedel för en designer, som själv kan modellera sina idéer och därigenom lättare åskådliggöra och diskutera sitt koncept vid möten. I många fall är det enklare att förstå en 3D-modell som man kan vrida och vända på, än en ritning på ett papper. Utifrån IMA-modellen skulle det vara möjligt att fräsa ut en lermodell, vilken kan finjusteras och sedan åter scannas in och bearbetas vidare i Alias.

Subjects/Keywords: Catia V5; Imagine and Shape; Volvo personvagnar; PVS

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

Holm, A. (2007). CATIA V5 SOM KONCEPTGENERERINGSVERKTYG. (Thesis). Halmstad University. Retrieved from http://urn.kb.se/resolve?urn=urn:nbn:se:hh:diva-771

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Chicago Manual of Style (16^th Edition):

Holm, Anders. “CATIA V5 SOM KONCEPTGENERERINGSVERKTYG.” 2007. Thesis, Halmstad University. Accessed January 21, 2021. http://urn.kb.se/resolve?urn=urn:nbn:se:hh:diva-771.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

MLA Handbook (7^th Edition):

Holm, Anders. “CATIA V5 SOM KONCEPTGENERERINGSVERKTYG.” 2007. Web. 21 Jan 2021.

Vancouver:

Holm A. CATIA V5 SOM KONCEPTGENERERINGSVERKTYG. [Internet] [Thesis]. Halmstad University; 2007. [cited 2021 Jan 21]. Available from: http://urn.kb.se/resolve?urn=urn:nbn:se:hh:diva-771.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Council of Science Editors:

Holm A. CATIA V5 SOM KONCEPTGENERERINGSVERKTYG. [Thesis]. Halmstad University; 2007. Available from: http://urn.kb.se/resolve?urn=urn:nbn:se:hh:diva-771

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

12. SHI LING. Comparative Studies, Formal Semantics and PVS Encoding of CSP#.

Degree: 2014, National University of Singapore

URL: http://scholarbank.nus.edu.sg/handle/10635/113265

Subjects/Keywords: Concurrency; Shared Variables; Denotational Semantics; UTP; Encoding; PVS

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

LING, S. (2014). Comparative Studies, Formal Semantics and PVS Encoding of CSP#. (Thesis). National University of Singapore. Retrieved from http://scholarbank.nus.edu.sg/handle/10635/113265

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Chicago Manual of Style (16^th Edition):

LING, SHI. “Comparative Studies, Formal Semantics and PVS Encoding of CSP#.” 2014. Thesis, National University of Singapore. Accessed January 21, 2021. http://scholarbank.nus.edu.sg/handle/10635/113265.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

MLA Handbook (7^th Edition):

LING, SHI. “Comparative Studies, Formal Semantics and PVS Encoding of CSP#.” 2014. Web. 21 Jan 2021.

Vancouver:

LING S. Comparative Studies, Formal Semantics and PVS Encoding of CSP#. [Internet] [Thesis]. National University of Singapore; 2014. [cited 2021 Jan 21]. Available from: http://scholarbank.nus.edu.sg/handle/10635/113265.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Council of Science Editors:

LING S. Comparative Studies, Formal Semantics and PVS Encoding of CSP#. [Thesis]. National University of Singapore; 2014. Available from: http://scholarbank.nus.edu.sg/handle/10635/113265

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

13. YUAN LING. Generic fault tolerant software architecture: Modeling, customization and verification.

Degree: 2008, National University of Singapore

URL: http://scholarbank.nus.edu.sg/handle/10635/13267

Subjects/Keywords: GFTSA; Fault Tolerance; Object-Z; XVCL; PVS; ProofLite

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

LING, Y. (2008). Generic fault tolerant software architecture: Modeling, customization and verification. (Thesis). National University of Singapore. Retrieved from http://scholarbank.nus.edu.sg/handle/10635/13267

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Chicago Manual of Style (16^th Edition):

LING, YUAN. “Generic fault tolerant software architecture: Modeling, customization and verification.” 2008. Thesis, National University of Singapore. Accessed January 21, 2021. http://scholarbank.nus.edu.sg/handle/10635/13267.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

MLA Handbook (7^th Edition):

LING, YUAN. “Generic fault tolerant software architecture: Modeling, customization and verification.” 2008. Web. 21 Jan 2021.

Vancouver:

LING Y. Generic fault tolerant software architecture: Modeling, customization and verification. [Internet] [Thesis]. National University of Singapore; 2008. [cited 2021 Jan 21]. Available from: http://scholarbank.nus.edu.sg/handle/10635/13267.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Council of Science Editors:

LING Y. Generic fault tolerant software architecture: Modeling, customization and verification. [Thesis]. National University of Singapore; 2008. Available from: http://scholarbank.nus.edu.sg/handle/10635/13267

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

14. SIVANESAN KAILASH PRABHU. Design of adaptive and hybrid energy & QOS aware heterogeneous multiprocessor scheduling strategies for embedded systems.

Degree: 2009, National University of Singapore

URL: https://scholarbank.nus.edu.sg/handle/10635/16564

Subjects/Keywords: BSN; PVS; multiprocessor; scheduling; battery; power-aware

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

PRABHU, S. K. (2009). Design of adaptive and hybrid energy & QOS aware heterogeneous multiprocessor scheduling strategies for embedded systems. (Thesis). National University of Singapore. Retrieved from https://scholarbank.nus.edu.sg/handle/10635/16564

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Chicago Manual of Style (16^th Edition):

PRABHU, SIVANESAN KAILASH. “Design of adaptive and hybrid energy & QOS aware heterogeneous multiprocessor scheduling strategies for embedded systems.” 2009. Thesis, National University of Singapore. Accessed January 21, 2021. https://scholarbank.nus.edu.sg/handle/10635/16564.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

MLA Handbook (7^th Edition):

PRABHU, SIVANESAN KAILASH. “Design of adaptive and hybrid energy & QOS aware heterogeneous multiprocessor scheduling strategies for embedded systems.” 2009. Web. 21 Jan 2021.

Vancouver:

PRABHU SK. Design of adaptive and hybrid energy & QOS aware heterogeneous multiprocessor scheduling strategies for embedded systems. [Internet] [Thesis]. National University of Singapore; 2009. [cited 2021 Jan 21]. Available from: https://scholarbank.nus.edu.sg/handle/10635/16564.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Council of Science Editors:

PRABHU SK. Design of adaptive and hybrid energy & QOS aware heterogeneous multiprocessor scheduling strategies for embedded systems. [Thesis]. National University of Singapore; 2009. Available from: https://scholarbank.nus.edu.sg/handle/10635/16564

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Brno University of Technology

15. Havlena, Jan. Modul pro komunikaci s portálem České daňové správy: Module for Electronic Communication with the Czech Tax Administration.

Degree: 2019, Brno University of Technology

URL: http://hdl.handle.net/11012/55497

► Bachelor thesis "Module for Electronic Communication with the Czech Tax Administration" has aim at the creation of module for electronic communication with the Czech Tax… (more)

Subjects/Keywords: Elektronická komunikace; elektronické podání; protokol pro komunikaci s PVS; mechanizmus elektronického podpisu; certifikát; certifikační autority; jazyk XML; protokol HTTPS; Electronic communication; electronic filing; protocol for communication with PVS; mechanism of electronic signature; certificate; certification authority; language XML; protocol HTTPS

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

Havlena, J. (2019). Modul pro komunikaci s portálem České daňové správy: Module for Electronic Communication with the Czech Tax Administration. (Thesis). Brno University of Technology. Retrieved from http://hdl.handle.net/11012/55497

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Chicago Manual of Style (16^th Edition):

Havlena, Jan. “Modul pro komunikaci s portálem České daňové správy: Module for Electronic Communication with the Czech Tax Administration.” 2019. Thesis, Brno University of Technology. Accessed January 21, 2021. http://hdl.handle.net/11012/55497.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

MLA Handbook (7^th Edition):

Havlena, Jan. “Modul pro komunikaci s portálem České daňové správy: Module for Electronic Communication with the Czech Tax Administration.” 2019. Web. 21 Jan 2021.

Vancouver:

Havlena J. Modul pro komunikaci s portálem České daňové správy: Module for Electronic Communication with the Czech Tax Administration. [Internet] [Thesis]. Brno University of Technology; 2019. [cited 2021 Jan 21]. Available from: http://hdl.handle.net/11012/55497.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Council of Science Editors:

Havlena J. Modul pro komunikaci s portálem České daňové správy: Module for Electronic Communication with the Czech Tax Administration. [Thesis]. Brno University of Technology; 2019. Available from: http://hdl.handle.net/11012/55497

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

16. Duruisseau, Kévin. Transition énergétique et géographie : le photovoltaïque au sol dans le sud de la France : Energy transition and geography : the photovoltaic ground in the south of France.

Degree: Docteur es, Géographie, 2016, Aix Marseille Université

URL: http://www.theses.fr/2016AIXM3050

►

Amorcée en 2002 avec la mise en place d’un régime financier d’encadrement basé sur un système de tarifs de rachat de l’électricité, la politique photovoltaïque… (more)

▼

Amorcée en 2002 avec la mise en place d’un régime financier d’encadrement basé sur un système de tarifs de rachat de l’électricité, la politique photovoltaïque au sol (PVS) vient enrichir les politiques énergie-climat françaises, devenues depuis des politiques publiques de transition énergétique. Ces politiques se déploient dans un contexte d’ouverture à la concurrence associée à la libéralisation des marchés de l’électricité, de fractionnement des moyens de production et de dévolution croissante de compétences « électriciennes » aux acteurs territoriaux publics favorisant une multiplication et une diversification des acteurs intervenants dans le système électrique français. Ces mutations ont amorcé un processus de territorialisation des EnR et dessinent une nouvelle géographie de l’électricité. Cette thèse interroge la place des territoires dans la transition énergétique, dans une analyse du processus de territorialisation de la politique publique PVS en France, et discute de l’émergence d’une nouvelle géographie de l’électricité. Elle articule une étude de la géographie des unités PVS en activité au 31 décembre 2015 dans les territoires du sud de la France avec une analyse actorielle de la diffusion spatiale de ces nouvelles infrastructures industrielles. Elle propose pour ce faire une typologie des acteurs-initiateurs PVS et une typologie des opérateurs-exploitants PVS permettant de mettre en évidence les nouveaux acteurs électriciens du système électrique français métropolitain. Elle propose plus largement une étude des systèmes de régulation et des jeux d’acteurs à l’œuvre dans les territoires PVS révélant le processus de territorialisation de cette EnR.

Began in 2002 with the establishment of a financial supervisory regime based on a system of feed-in tariffs, the photovoltaic public policy on the ground enriches French energy and climate public policy, which have since become public policies for “low carbon” energy transition. These policies are deployed in a context of openness to competition associated with the liberalization of the European national markets for electricity, means splitting production and increasing devolution of "Electricians" powers to public territorial players favoring multiplication and diversification of actors involved in the metropolitan French electrical system. These changes have initiated a process of territorialization of renewable energy and create a new geography of electricity.This thesis questions the place of the territories in the "low carbon" energy transition, in an analysis of regionalization of public policy photovoltaic ground process in France, and discusses the emergence of a new geography of electricity. It articulates a study of the geography of photovoltaic ground units in operation on 31 December 2015 in the southern territories of France with an actorial analysis of the spatial distribution of these new industrial infrastructures. It proposes to do this a typology of photovoltaic ground initiators-actors and a typology of photovoltaic ground…

Advisors/Committee Members: Daviet, Sylvie (thesis director).

Subjects/Keywords: Transition énergétique « bas carbone »; Territorialisation; Photovoltaïque au sol (PVS); Politique publique; Système d’acteurs; Dépendance au sentier; "low carbon" energy transition; Territorialization; Photovoltaic ground; Public policy; System of actors; Path dependency

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

Duruisseau, K. (2016). Transition énergétique et géographie : le photovoltaïque au sol dans le sud de la France : Energy transition and geography : the photovoltaic ground in the south of France. (Doctoral Dissertation). Aix Marseille Université. Retrieved from http://www.theses.fr/2016AIXM3050

Chicago Manual of Style (16^th Edition):

Duruisseau, Kévin. “Transition énergétique et géographie : le photovoltaïque au sol dans le sud de la France : Energy transition and geography : the photovoltaic ground in the south of France.” 2016. Doctoral Dissertation, Aix Marseille Université. Accessed January 21, 2021. http://www.theses.fr/2016AIXM3050.

MLA Handbook (7^th Edition):

Duruisseau, Kévin. “Transition énergétique et géographie : le photovoltaïque au sol dans le sud de la France : Energy transition and geography : the photovoltaic ground in the south of France.” 2016. Web. 21 Jan 2021.

Vancouver:

Duruisseau K. Transition énergétique et géographie : le photovoltaïque au sol dans le sud de la France : Energy transition and geography : the photovoltaic ground in the south of France. [Internet] [Doctoral dissertation]. Aix Marseille Université 2016. [cited 2021 Jan 21]. Available from: http://www.theses.fr/2016AIXM3050.

Council of Science Editors:

Duruisseau K. Transition énergétique et géographie : le photovoltaïque au sol dans le sud de la France : Energy transition and geography : the photovoltaic ground in the south of France. [Doctoral Dissertation]. Aix Marseille Université 2016. Available from: http://www.theses.fr/2016AIXM3050

Brno University of Technology

17. Kovaľ, Nikodém. Posouzení návrhu malé fotovoltaické elektrárny pro rodinný dům a zpracování postupu její revize: Assessment of the design of a small photovoltaic power plant for a family house and elaboration of its revision process.

Degree: 2020, Brno University of Technology

URL: http://hdl.handle.net/11012/190390

► The bachelor's thesis deals with the assessment of a domestic photovoltaic power plant for a family house and the processing of its revision. At the… (more)

Subjects/Keywords: fotovoltaická elektráreň; slnečná energia; fotovoltaický panel; sieťová fotovoltaická elektráreň; revízia FVE; photovoltaic power plant; sun energy; photovoltaic panel; on-grid photovoltaic system; revision of PVS

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

Kovaľ, N. (2020). Posouzení návrhu malé fotovoltaické elektrárny pro rodinný dům a zpracování postupu její revize: Assessment of the design of a small photovoltaic power plant for a family house and elaboration of its revision process. (Thesis). Brno University of Technology. Retrieved from http://hdl.handle.net/11012/190390

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Chicago Manual of Style (16^th Edition):

Kovaľ, Nikodém. “Posouzení návrhu malé fotovoltaické elektrárny pro rodinný dům a zpracování postupu její revize: Assessment of the design of a small photovoltaic power plant for a family house and elaboration of its revision process.” 2020. Thesis, Brno University of Technology. Accessed January 21, 2021. http://hdl.handle.net/11012/190390.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

MLA Handbook (7^th Edition):

Kovaľ, Nikodém. “Posouzení návrhu malé fotovoltaické elektrárny pro rodinný dům a zpracování postupu její revize: Assessment of the design of a small photovoltaic power plant for a family house and elaboration of its revision process.” 2020. Web. 21 Jan 2021.

Vancouver:

Kovaľ N. Posouzení návrhu malé fotovoltaické elektrárny pro rodinný dům a zpracování postupu její revize: Assessment of the design of a small photovoltaic power plant for a family house and elaboration of its revision process. [Internet] [Thesis]. Brno University of Technology; 2020. [cited 2021 Jan 21]. Available from: http://hdl.handle.net/11012/190390.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Council of Science Editors:

Kovaľ N. Posouzení návrhu malé fotovoltaické elektrárny pro rodinný dům a zpracování postupu její revize: Assessment of the design of a small photovoltaic power plant for a family house and elaboration of its revision process. [Thesis]. Brno University of Technology; 2020. Available from: http://hdl.handle.net/11012/190390

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Queensland University of Technology

18. Shahnia, Farhad. Analysis and correction of voltage profile in low voltage distribution networks containing photovoltaic cells and electric vehicles.

Degree: 2011, Queensland University of Technology

URL: https://eprints.qut.edu.au/50834/

► Voltage drop and rise at network peak and off–peak periods along with voltage unbalance are the major power quality problems in low voltage distribution networks.… (more)

▼ Voltage drop and rise at network peak and off–peak periods along with voltage unbalance are the major power quality problems in low voltage distribution networks. Usually, the utilities try to use adjusting the transformer tap changers as a solution for the voltage drop. They also try to distribute the loads equally as a solution for network voltage unbalance problem. On the other hand, the ever increasing energy demand, along with the necessity of cost reduction and higher reliability requirements, are driving the modern power systems towards Distributed Generation (DG) units. This can be in the form of small rooftop photovoltaic cells (PV), Plug–in Electric Vehicles (PEVs) or Micro Grids (MGs). Rooftop PVs, typically with power levels ranging from 1–5 kW installed by the householders are gaining popularity due to their financial benefits for the householders. Also PEVs will be soon emerged in residential distribution networks which behave as a huge residential load when they are being charged while in their later generation, they are also expected to support the network as small DG units which transfer the energy stored in their battery into grid. Furthermore, the MG which is a cluster of loads and several DG units such as diesel generators, PVs, fuel cells and batteries are recently introduced to distribution networks. The voltage unbalance in the network can be increased due to the uncertainties in the random connection point of the PVs and PEVs to the network, their nominal capacity and time of operation. Therefore, it is of high interest to investigate the voltage unbalance in these networks as the result of MGs, PVs and PEVs integration to low voltage networks. In addition, the network might experience non–standard voltage drop due to high penetration of PEVs, being charged at night periods, or non–standard voltage rise due to high penetration of PVs and PEVs generating electricity back into the grid in the network off–peak periods. In this thesis, a voltage unbalance sensitivity analysis and stochastic evaluation is carried out for PVs installed by the householders versus their installation point, their nominal capacity and penetration level as different uncertainties. A similar analysis is carried out for PEVs penetration in the network working in two different modes: Grid to vehicle and Vehicle to grid. Furthermore, the conventional methods are discussed for improving the voltage unbalance within these networks. This is later continued by proposing new and efficient improvement methods for voltage profile improvement at network peak and off–peak periods and voltage unbalance reduction. In addition, voltage unbalance reduction is investigated for MGs and new improvement methods are proposed and applied for the MG test bed, planned to be established at Queensland University of Technology (QUT). MATLAB and PSCAD/EMTDC simulation softwares are used for verification of the analyses and the proposals.

Subjects/Keywords: low voltage distribution networks; voltage profile; voltage unbalance; photovoltaic cells; single–phase rooftop PVs; plug–in electric vehicles; micro grid; DSTATCOM; DVR; sensitivity analysis; stochastic evaluation

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

Shahnia, F. (2011). Analysis and correction of voltage profile in low voltage distribution networks containing photovoltaic cells and electric vehicles. (Thesis). Queensland University of Technology. Retrieved from https://eprints.qut.edu.au/50834/

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Chicago Manual of Style (16^th Edition):

Shahnia, Farhad. “Analysis and correction of voltage profile in low voltage distribution networks containing photovoltaic cells and electric vehicles.” 2011. Thesis, Queensland University of Technology. Accessed January 21, 2021. https://eprints.qut.edu.au/50834/.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

MLA Handbook (7^th Edition):

Shahnia, Farhad. “Analysis and correction of voltage profile in low voltage distribution networks containing photovoltaic cells and electric vehicles.” 2011. Web. 21 Jan 2021.

Vancouver:

Shahnia F. Analysis and correction of voltage profile in low voltage distribution networks containing photovoltaic cells and electric vehicles. [Internet] [Thesis]. Queensland University of Technology; 2011. [cited 2021 Jan 21]. Available from: https://eprints.qut.edu.au/50834/.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Council of Science Editors:

Shahnia F. Analysis and correction of voltage profile in low voltage distribution networks containing photovoltaic cells and electric vehicles. [Thesis]. Queensland University of Technology; 2011. Available from: https://eprints.qut.edu.au/50834/

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Università Cattolica del Sacro Cuore

19. GAMA, ISA. Dinamiche Interculturali e Sviluppo: Mozambico e Cooperazione Internazionale Italiana.

Degree: 2011, Università Cattolica del Sacro Cuore

URL: http://hdl.handle.net/10280/987

►

Questo studio tratta dei rapporti della cooperazione internazionale per lo sviluppo che favorisce lo scambio tra culture. Si tratta di una ricerca socio-antropologica sull’orientamento cognitivo… (more)

▼

Questo studio tratta dei rapporti della cooperazione internazionale per lo sviluppo che favorisce lo scambio tra culture. Si tratta di una ricerca socio-antropologica sull’orientamento cognitivo di entrambi gli attori della cooperazione: chi fornisce e chi riceve l’aiuto. Lo studio è realizzato su due fronti: in Mozambico, in un progetto di cooperazione, e in Italia con membri delle ONG. La tesi sostiene che la cooperazione non solo propone progetti atti a modificare una situazione nei PVS, ma unisce culture favorendo lo scambio di contenuti, opinioni divergenti, abitudini, ecc., trasformandoli in un continuo processo di ‘miscegenation’. La maggior parte delle ONG implementa progetti sul principio della sussidiarietà affrontando difficoltà per stimolare l’‘azione’ per apportare cambiamenti dal basso. La cooperazione è anche fautrice della fusione di culture che genera nuove correnti di pensiero, creando opinioni critiche nei confronti delle idee prevalenti, e provvede voce a movimenti sociali dal basso. In una macro-prospettiva, la globalizzazione continua ad avere un ruolo preponderante nei PVS: il Mozambico non è ancora decolonizzato. Il termine ‘sviluppo’ mantiene tuttora un pregiudizio evolutivo Eurocentrico, e non dovrebbe essere più associato alla crescita economica, e per ottenere un mondo equo non basta ‘empower’ i poveri, è necessario ‘disempower’ i ricchi.

This study addresses the relationships on international cooperation for development that put cultures into motion. This is a socio-anthropological research that outlines the cognitive orientation of both sides in the international cooperation: who provides and who receives Aid. The locus of the investigation is an international cooperation project in Mozambique, along with interviews with Italian NGOs practitioners. The thesis argues that international cooperation not only provides projects apt to change situation in developing countries, but unites cultures that mutually exchange meanings, disagreements, habits, etc., in a continuous process of cultural ‘miscegenation’. Although most NGOs propose bottom-up approach to development, usually projects start from the top, and they face difficulties to stimulate the agency to change from below. International cooperation also generates new lines of though, and usually gives voice to counter-current social movements. In a macro perspective, globalization continues to play a dominant role in the poorest countries, and Mozambique has not been fully decolonized yet. The meaning of the term Development still maintains an Eurocentric and evolutionary bias. However, development should not be anymore associated to economic growth and if we really want to achieve an equal world, there is also the need to ‘disempower’ the rich.

Advisors/Committee Members: BOVONE, LAURA, ROVATI, GIANCARLO, CASELLA PALTRINIERI, ANNA.

Subjects/Keywords: M-DEA/01: DISCIPLINE DEMOETNOANTROPOLOGICHE; SPS/07: SOCIOLOGIA GENERALE; Relazioni Culturali, Sviluppo, Cooperazione Internazionale, Pasei in via di Sviluppo(PVS), Cultural Relations, Development, International Cooperation, Developing Countries

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

GAMA, I. (2011). Dinamiche Interculturali e Sviluppo: Mozambico e Cooperazione Internazionale Italiana. (Doctoral Dissertation). Università Cattolica del Sacro Cuore. Retrieved from http://hdl.handle.net/10280/987

Chicago Manual of Style (16^th Edition):

GAMA, ISA. “Dinamiche Interculturali e Sviluppo: Mozambico e Cooperazione Internazionale Italiana.” 2011. Doctoral Dissertation, Università Cattolica del Sacro Cuore. Accessed January 21, 2021. http://hdl.handle.net/10280/987.

MLA Handbook (7^th Edition):

GAMA, ISA. “Dinamiche Interculturali e Sviluppo: Mozambico e Cooperazione Internazionale Italiana.” 2011. Web. 21 Jan 2021.

Vancouver:

GAMA I. Dinamiche Interculturali e Sviluppo: Mozambico e Cooperazione Internazionale Italiana. [Internet] [Doctoral dissertation]. Università Cattolica del Sacro Cuore; 2011. [cited 2021 Jan 21]. Available from: http://hdl.handle.net/10280/987.

Council of Science Editors:

GAMA I. Dinamiche Interculturali e Sviluppo: Mozambico e Cooperazione Internazionale Italiana. [Doctoral Dissertation]. Università Cattolica del Sacro Cuore; 2011. Available from: http://hdl.handle.net/10280/987

20. CHEN CHUNQING. A verification system for interval-based specification languages with its application to simulink.

Degree: 2009, National University of Singapore

URL: http://scholarbank.nus.edu.sg/handle/10635/12960

Subjects/Keywords: Real-time computing systems; Interval-based specification languages; Formal verification; PVS; Simulink

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

CHUNQING, C. (2009). A verification system for interval-based specification languages with its application to simulink. (Thesis). National University of Singapore. Retrieved from http://scholarbank.nus.edu.sg/handle/10635/12960

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Chicago Manual of Style (16^th Edition):

CHUNQING, CHEN. “A verification system for interval-based specification languages with its application to simulink.” 2009. Thesis, National University of Singapore. Accessed January 21, 2021. http://scholarbank.nus.edu.sg/handle/10635/12960.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

MLA Handbook (7^th Edition):

CHUNQING, CHEN. “A verification system for interval-based specification languages with its application to simulink.” 2009. Web. 21 Jan 2021.

Vancouver:

CHUNQING C. A verification system for interval-based specification languages with its application to simulink. [Internet] [Thesis]. National University of Singapore; 2009. [cited 2021 Jan 21]. Available from: http://scholarbank.nus.edu.sg/handle/10635/12960.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Council of Science Editors:

CHUNQING C. A verification system for interval-based specification languages with its application to simulink. [Thesis]. National University of Singapore; 2009. Available from: http://scholarbank.nus.edu.sg/handle/10635/12960

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Brandeis University

21. Cypess, Joshua. Jewish Medical Culture: Case Studies in End-of-Life Decision Making.

Degree: 2015, Brandeis University

URL: http://hdl.handle.net/10192/31050

► As the technology of medical care has advanced in recent years, the ethical, religious, and legal problems and questions surrounding it have multiplied. This principle… (more)

▼ As the technology of medical care has advanced in recent years, the ethical, religious, and legal problems and questions surrounding it have multiplied. This principle is nowhere more true than in decision making in the care of patients at the end of life. Increasingly, scholars in the fields of ethics, sociology, and the sciences are beginning to recognize that the definitions of life and death and the necessary responses to various medical conditions at the end of life are often culturally contingent rather than strictly objective and verifiable. Within Jewish practice, end-of-life decision making takes on a singular character. Responses by Jewish patients, rabbinic authorities, and caregivers to issues as fundamental as the definition of death are inflected by the particular history of Judaism in the modern age. Taken together, those responses constitute what I call “Jewish Medical Culture,” the concept that lies at the heart of this work. What is Jewish Medical Culture? It is a subset of Jewish culture that deals with health, the body, and issues of life and death. For Americans who associate with the constellation of symbols and definitions that come from a lived experience of the ethno-religious community of Judaism, behavior is often guided by principles that may be traced to that community. This is especially true in cases at the end of life, when the turn to religious principles may become most pronounced. Thus analysis of particular cases in end-of-life decision making represents a means for elucidating this highly charged manifestation of Jewish Medical Culture. My aim is not to prescribe a Jewish bioethics or to determine the halakhic (Jewish legal) response to end-of-life cases. Instead, I study Jewish Medical Culture from a sociological perspective—how it manifests itself in actual practice. Drawing on literature dealing with cultural differences toward American medical care, as well as the history and ethics of Jews and medicine, this study considers three significant cases related to end-of-life medical issues—two within Orthodox Judaism and one outside of it: the cases are those of Mordechai Dov Brody, the conjoined twins of 1977, and Terri Schiavo. These three cases in succession highlight complex medical issues around the end of life. Using a variety of source bases—including academic case reports, newspaper articles, websites, and halakhic writings—I propose to explicate the Jewish themes that are implicit in the American Jewish community’s responses to major issues in medical decision-making. Although there is no single, unified Jewish American voice on medical care or ethics, I will argue that many of the responses to these cases from within the Jewish community—from patients, doctors, rabbinic leaders, and lay observers—had their underpinnings in Jewish tradition and Jewish concepts—that is, in Jewish Medical Culture. These manifestations of Jewish Medical Culture, I argue, reveal a great deal about contemporary Jewish ideas and practices, the extent to which Jewish identity is rooted in or…

Subjects/Keywords: Jewish Studies; Sociology; End of Life; Death; Medical Ethics; Medical Sociology; Sociology of Health; Sociology of Religion; Orthodox Judaism; Halakhah; PVS; conjoined twins; Terri Schiavo; brain death

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

Cypess, J. (2015). Jewish Medical Culture: Case Studies in End-of-Life Decision Making. (Thesis). Brandeis University. Retrieved from http://hdl.handle.net/10192/31050

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Chicago Manual of Style (16^th Edition):

Cypess, Joshua. “Jewish Medical Culture: Case Studies in End-of-Life Decision Making.” 2015. Thesis, Brandeis University. Accessed January 21, 2021. http://hdl.handle.net/10192/31050.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

MLA Handbook (7^th Edition):

Cypess, Joshua. “Jewish Medical Culture: Case Studies in End-of-Life Decision Making.” 2015. Web. 21 Jan 2021.

Vancouver:

Cypess J. Jewish Medical Culture: Case Studies in End-of-Life Decision Making. [Internet] [Thesis]. Brandeis University; 2015. [cited 2021 Jan 21]. Available from: http://hdl.handle.net/10192/31050.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Council of Science Editors:

Cypess J. Jewish Medical Culture: Case Studies in End-of-Life Decision Making. [Thesis]. Brandeis University; 2015. Available from: http://hdl.handle.net/10192/31050

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Brno University of Technology

22. Nohál, Libor. Připojení vyvrtávacích hlav s CNC řízenou U-osou na horizontálních centrech Tajmac-ZPS: Boring and facing head with CNC U-axis interfacing on Horizontal machining centres Tajmac-ZPS.

Degree: 2019, Brno University of Technology

URL: http://hdl.handle.net/11012/1671

► The subject of this thesis is a suggestion on mechanism for automatic interfacing of boring and facing heads with CNC U-axis on horizontal machining centres… (more)

Subjects/Keywords: Horizontální obráběcí centrum; CNC vyvrtávací hlava; H 80; PVS; modální analýza; Horizontal machining centre; CNC boring and facing head; H 80; FMS; modal analysis.

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

Nohál, L. (2019). Připojení vyvrtávacích hlav s CNC řízenou U-osou na horizontálních centrech Tajmac-ZPS: Boring and facing head with CNC U-axis interfacing on Horizontal machining centres Tajmac-ZPS. (Thesis). Brno University of Technology. Retrieved from http://hdl.handle.net/11012/1671

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Chicago Manual of Style (16^th Edition):

Nohál, Libor. “Připojení vyvrtávacích hlav s CNC řízenou U-osou na horizontálních centrech Tajmac-ZPS: Boring and facing head with CNC U-axis interfacing on Horizontal machining centres Tajmac-ZPS.” 2019. Thesis, Brno University of Technology. Accessed January 21, 2021. http://hdl.handle.net/11012/1671.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

MLA Handbook (7^th Edition):

Nohál, Libor. “Připojení vyvrtávacích hlav s CNC řízenou U-osou na horizontálních centrech Tajmac-ZPS: Boring and facing head with CNC U-axis interfacing on Horizontal machining centres Tajmac-ZPS.” 2019. Web. 21 Jan 2021.

Vancouver:

Nohál L. Připojení vyvrtávacích hlav s CNC řízenou U-osou na horizontálních centrech Tajmac-ZPS: Boring and facing head with CNC U-axis interfacing on Horizontal machining centres Tajmac-ZPS. [Internet] [Thesis]. Brno University of Technology; 2019. [cited 2021 Jan 21]. Available from: http://hdl.handle.net/11012/1671.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Council of Science Editors:

Nohál L. Připojení vyvrtávacích hlav s CNC řízenou U-osou na horizontálních centrech Tajmac-ZPS: Boring and facing head with CNC U-axis interfacing on Horizontal machining centres Tajmac-ZPS. [Thesis]. Brno University of Technology; 2019. Available from: http://hdl.handle.net/11012/1671

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Queens University

23. Avni, Shachar. Frontier Sets in Large Terrain Environments with Applications to Decentralized Online Games .

Degree: Computing, 2010, Queens University

URL: http://hdl.handle.net/1974/5688

► In current online games, player positions are synchronized by means of continual broadcasts through the server. This solution is expensive, forcing any server to limit… (more)

Subjects/Keywords: Computer Graphics ; Visibility ; PVS ; Frontier Sets ; Terrains ; Game Programming ; Computer Science

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

Avni, S. (2010). Frontier Sets in Large Terrain Environments with Applications to Decentralized Online Games . (Thesis). Queens University. Retrieved from http://hdl.handle.net/1974/5688

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Chicago Manual of Style (16^th Edition):

Avni, Shachar. “Frontier Sets in Large Terrain Environments with Applications to Decentralized Online Games .” 2010. Thesis, Queens University. Accessed January 21, 2021. http://hdl.handle.net/1974/5688.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

MLA Handbook (7^th Edition):

Avni, Shachar. “Frontier Sets in Large Terrain Environments with Applications to Decentralized Online Games .” 2010. Web. 21 Jan 2021.

Vancouver:

Avni S. Frontier Sets in Large Terrain Environments with Applications to Decentralized Online Games . [Internet] [Thesis]. Queens University; 2010. [cited 2021 Jan 21]. Available from: http://hdl.handle.net/1974/5688.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Council of Science Editors:

Avni S. Frontier Sets in Large Terrain Environments with Applications to Decentralized Online Games . [Thesis]. Queens University; 2010. Available from: http://hdl.handle.net/1974/5688

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

24. Marti, Alexander M. Comparison of digital scanning and polyvinyl siloxane impression techniques by DMD students : instructional efficiency and attitudes toward technology.

Degree: MS, 2015, University of Louisville

URL: 10.18297/etd/2338 ; https://ir.library.louisville.edu/etd/2338

► The aim of this research was compare the ability of dental students to learn an digital scanner (3M LAVA) and material-based (PVS) impression techniques… (more)

Subjects/Keywords: Lava C.O.S.; digital impression; dental education; PVS; Learning curve; Prosthodontics and Prosthodontology

…scanning (3M ESPE, St. Paul, MN, USA) and polyvinyl siloxane (PVS) (3M… …siloxane [PVS]) dual-tray impression technique and chairside digital scanning… …x28;polyvinyl siloxane [PVS]) dual-tray impression technique and chairside… …polyvinyl siloxane [PVS]) dual-tray technique and chairside digital scanning… …siloxane [PVS]) dual-tray technique and chairside digital scanning technique (…

5 more images…

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

Marti, A. M. (2015). Comparison of digital scanning and polyvinyl siloxane impression techniques by DMD students : instructional efficiency and attitudes toward technology. (Masters Thesis). University of Louisville. Retrieved from 10.18297/etd/2338 ; https://ir.library.louisville.edu/etd/2338

Chicago Manual of Style (16^th Edition):

Marti, Alexander M. “Comparison of digital scanning and polyvinyl siloxane impression techniques by DMD students : instructional efficiency and attitudes toward technology.” 2015. Masters Thesis, University of Louisville. Accessed January 21, 2021. 10.18297/etd/2338 ; https://ir.library.louisville.edu/etd/2338.

MLA Handbook (7^th Edition):

Marti, Alexander M. “Comparison of digital scanning and polyvinyl siloxane impression techniques by DMD students : instructional efficiency and attitudes toward technology.” 2015. Web. 21 Jan 2021.

Vancouver:

Marti AM. Comparison of digital scanning and polyvinyl siloxane impression techniques by DMD students : instructional efficiency and attitudes toward technology. [Internet] [Masters thesis]. University of Louisville; 2015. [cited 2021 Jan 21]. Available from: 10.18297/etd/2338 ; https://ir.library.louisville.edu/etd/2338.

Council of Science Editors:

Marti AM. Comparison of digital scanning and polyvinyl siloxane impression techniques by DMD students : instructional efficiency and attitudes toward technology. [Masters Thesis]. University of Louisville; 2015. Available from: 10.18297/etd/2338 ; https://ir.library.louisville.edu/etd/2338

Università Cattolica del Sacro Cuore

25. CONDOSTA, LUCA. MULTINAZIONALI E PAESI IN VIA DI SVILUPPO: LA RILEVANZA STRATEGICA DEL COMMUNITY INVESTMENT.

Degree: 2010, Università Cattolica del Sacro Cuore

URL: http://hdl.handle.net/10280/755

►

La tesi vuole esaminare il fenomeno dei community investment nei PVS da parte delle multinazionali. Dopo aver studiato la letteratura esistente sul tema della CSR… (more)

▼

La tesi vuole esaminare il fenomeno dei community investment nei PVS da parte delle multinazionali. Dopo aver studiato la letteratura esistente sul tema della CSR della sua applicazione nei PVS da parte delle MNC, la ricerca sul campo è stata articolata in due fasi. Una prima fase, di tipo esplorativa, è stata condotta attraverso un questionario somministrato nei primi sei mesi del 2009 a 100 imprese, selezionate in modo casuale dalla lista del Fortune Global 500 (che include le maggiori imprese mondiali quotate in termini di ricavi e utile netto) al 31/12/2008. Scopo del questionario è stato quello di iniziare ad indagare sul fenomeno degli interventi di CSR fatti dalle multinazionali a favore delle comunità dei PVS. Una volta raccolti ed esaminati i risultati ottenuti dal questionario esplorativo, la seconda fase della ricerca è stata basata sulla selezione e analisi di cinque casi con la tecnica del multiple-case study analysis. Per le cinque imprese selezionate si è proceduto con l’analisi di un’ampia base di fonti primarie, integrata con dati provenienti da altre fonti. Al termine si è proceduto con l’interpretazione dei dati formulando un modello per interpretare le strategie di un’impresa verso le comunità dei PVS in cui opera.

The thesis is aimed at examining the phenomenon of community investments in developing countries by multinationals. After studying existing literature on CSR and its application in developing countries by MNC, the research has been split in two parts. The first past, explorative, has been done through a survey sent in the first 6 months of 2009 to 100 companies, randomly extracted from the Fortune Global 500 at 31/12/2008. The purpose of the survey was to start understanding the phenomenon of CSR activities done by MNC to communities in developing countries. Once surveys have been collected, the second part of the research has been based on the selection and analysis of 5 cases with the technique of multiple case study analysis. For those 5 companies the work has been done with the analysis of lots of primary source, integrated with data coming from other sources. AT the end data have been interpreted defining a model by which read strategies realized by companies to communities in developing countries.

Advisors/Committee Members: FIOCCA, RENATO, MOLTENI, MARIO.

Subjects/Keywords: SECS-P/08: ECONOMIA E GESTIONE DELLE IMPRESE; SECS-P/07: ECONOMIA AZIENDALE; sostenibilità, bilancio sociale, responsabilità sociale di impresa, paesi in via di sviluppo, corporate social responsibility, CSR, PVS, MNC, strategia sociale, case study, comunità, sviluppo locale

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

CONDOSTA, L. (2010). MULTINAZIONALI E PAESI IN VIA DI SVILUPPO: LA RILEVANZA STRATEGICA DEL COMMUNITY INVESTMENT. (Doctoral Dissertation). Università Cattolica del Sacro Cuore. Retrieved from http://hdl.handle.net/10280/755

Chicago Manual of Style (16^th Edition):

CONDOSTA, LUCA. “MULTINAZIONALI E PAESI IN VIA DI SVILUPPO: LA RILEVANZA STRATEGICA DEL COMMUNITY INVESTMENT.” 2010. Doctoral Dissertation, Università Cattolica del Sacro Cuore. Accessed January 21, 2021. http://hdl.handle.net/10280/755.

MLA Handbook (7^th Edition):

CONDOSTA, LUCA. “MULTINAZIONALI E PAESI IN VIA DI SVILUPPO: LA RILEVANZA STRATEGICA DEL COMMUNITY INVESTMENT.” 2010. Web. 21 Jan 2021.

Vancouver:

CONDOSTA L. MULTINAZIONALI E PAESI IN VIA DI SVILUPPO: LA RILEVANZA STRATEGICA DEL COMMUNITY INVESTMENT. [Internet] [Doctoral dissertation]. Università Cattolica del Sacro Cuore; 2010. [cited 2021 Jan 21]. Available from: http://hdl.handle.net/10280/755.

Council of Science Editors:

CONDOSTA L. MULTINAZIONALI E PAESI IN VIA DI SVILUPPO: LA RILEVANZA STRATEGICA DEL COMMUNITY INVESTMENT. [Doctoral Dissertation]. Università Cattolica del Sacro Cuore; 2010. Available from: http://hdl.handle.net/10280/755

University of Connecticut

26. Shcherbatov, Polina P. Virtual Three-Dimensional Analysis of Dimensional Accuracy of Dental Master Die Models Created by the iTeroTM Electronic Impression Device and Those Made From a Polyvinyl Siloxane Impression Material.

Degree: Master of Dental Science, Dental Science, 2012, University of Connecticut

URL: https://opencommons.uconn.edu/gs_theses/312

Subjects/Keywords: iTero; Digital Scanning; Dental impressions; CAD/CAM; PVS; White Light Scanner; CMM; Coordinate Measuring Machine

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

Shcherbatov, P. P. (2012). Virtual Three-Dimensional Analysis of Dimensional Accuracy of Dental Master Die Models Created by the iTeroTM Electronic Impression Device and Those Made From a Polyvinyl Siloxane Impression Material. (Masters Thesis). University of Connecticut. Retrieved from https://opencommons.uconn.edu/gs_theses/312

Chicago Manual of Style (16^th Edition):

Shcherbatov, Polina P. “Virtual Three-Dimensional Analysis of Dimensional Accuracy of Dental Master Die Models Created by the iTeroTM Electronic Impression Device and Those Made From a Polyvinyl Siloxane Impression Material.” 2012. Masters Thesis, University of Connecticut. Accessed January 21, 2021. https://opencommons.uconn.edu/gs_theses/312.

MLA Handbook (7^th Edition):

Shcherbatov, Polina P. “Virtual Three-Dimensional Analysis of Dimensional Accuracy of Dental Master Die Models Created by the iTeroTM Electronic Impression Device and Those Made From a Polyvinyl Siloxane Impression Material.” 2012. Web. 21 Jan 2021.

Vancouver:

Shcherbatov PP. Virtual Three-Dimensional Analysis of Dimensional Accuracy of Dental Master Die Models Created by the iTeroTM Electronic Impression Device and Those Made From a Polyvinyl Siloxane Impression Material. [Internet] [Masters thesis]. University of Connecticut; 2012. [cited 2021 Jan 21]. Available from: https://opencommons.uconn.edu/gs_theses/312.

Council of Science Editors:

Shcherbatov PP. Virtual Three-Dimensional Analysis of Dimensional Accuracy of Dental Master Die Models Created by the iTeroTM Electronic Impression Device and Those Made From a Polyvinyl Siloxane Impression Material. [Masters Thesis]. University of Connecticut; 2012. Available from: https://opencommons.uconn.edu/gs_theses/312

Georgia Southern University

27. Pulos, James G. Principals and the Professional Victim Syndrome.

Degree: Doctor of Education in Education Administration (EdD), Department of Leadership, Technology, and Human Development, 2012, Georgia Southern University

URL: https://digitalcommons.georgiasouthern.edu/etd/788

► Principals today are constantly in the public eye. Every decision made subjects him/her to the scrutiny of staff and faculty, students, central office personnel,… (more)

▼ Principals today are constantly in the public eye. Every decision made subjects him/her to the scrutiny of staff and faculty, students, central office personnel, parents, community members, and board members. Contemporary principals are asked by their superintendents to lead reform efforts effectively or face the possibility of dismissal. Principals often face the dilemma of balancing politics in an effort to appease board members and the superintendent while simultaneously implementing critical change efforts in their schools. Hess and Kelly (2005) suggested that as principals attempt to lead reform efforts, they often go blindly into these positions unprepared and enter the principalship with a naivety towards the political aspect and importance of relationship building. In 2008, Polka and Litchka used the term “professional victim syndrome” (PVS) to describe the condition confronted by educational leaders, especially superintendents, who experienced a career crisis where their professional and personal reputations were tarnished and they were challenged with navigating political waves in order to survive. In this study, the extent to which the PVS exists among principals was examined, how they came to be professional victims; and what mechanisms were used to cope with the crisis experienced. A mixed-methods approach was used for data collection. Members of the Georgia Association of Middle School Principals (GAMSP) and the Georgia Association of Secondary School Principals (GASSP) were asked to complete the Professional Victim Survey for Middle and Secondary Principals. Out of the 443 total valid responses to the survey, 133 reported serving as a middle school principal, and 310 reported serving as a high school principal. Of the respondents, 11% self-reported being a professional victim. While 9 were extensively, interviewed, 75% (36 out of the 48) volunteered to participate in the qualitative study suggesting a willingness to discuss their crisis. All nine of the victims interviewed were involved in implementing change suggesting this to be a contributing factor for PVS. All nine reported having relationship issues and reported that politics played a major role in their crisis. All nine stated that their family, friends, and spirituality made the difference in how they coped with the crisis. Advisors/Committee Members: Linda M. Arthur, Ralph P. Gornto.

Subjects/Keywords: ETD; Professional Victim Syndrome; PVS; Tenure; Reform; Change Agents; Politics; Zone of Acceptance; Elementary and Middle and Secondary Education Administration; Jack N. Averitt College of Graduate Studies, Electronic Theses & Dissertations, ETDs, Student Research

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

Pulos, J. G. (2012). Principals and the Professional Victim Syndrome. (Doctoral Dissertation). Georgia Southern University. Retrieved from https://digitalcommons.georgiasouthern.edu/etd/788

Chicago Manual of Style (16^th Edition):

Pulos, James G. “Principals and the Professional Victim Syndrome.” 2012. Doctoral Dissertation, Georgia Southern University. Accessed January 21, 2021. https://digitalcommons.georgiasouthern.edu/etd/788.

MLA Handbook (7^th Edition):

Pulos, James G. “Principals and the Professional Victim Syndrome.” 2012. Web. 21 Jan 2021.

Vancouver:

Pulos JG. Principals and the Professional Victim Syndrome. [Internet] [Doctoral dissertation]. Georgia Southern University; 2012. [cited 2021 Jan 21]. Available from: https://digitalcommons.georgiasouthern.edu/etd/788.

Council of Science Editors:

Pulos JG. Principals and the Professional Victim Syndrome. [Doctoral Dissertation]. Georgia Southern University; 2012. Available from: https://digitalcommons.georgiasouthern.edu/etd/788

University of Helsinki

28. Chiunga, Evangelista. Viruses occurring in potatoes (Solanum tuberosum) in Mbeya region, Tanzania.

Degree: Department of Agricultural Sciences; Helsingfors universitet, Agrikultur- och forstvetenskapliga fakulteten, Institutionen för lantsbruksvetenskaper, 2013, University of Helsinki

URL: http://hdl.handle.net/10138/39459

► Potato leaf roll virus (PLRV), Potato virus Y (PVY), Potato virus X (PVX), Potato virus S (PVS), Potato virus A (PVA), and Potato virus M… (more)

Subjects/Keywords: potato; potato virus S (PVS); potato virus X (PVX); potato leafroll virus (PLRV); potato virus M (PVM); potato virus A; potato virus Y (PVY); Solanum tuberosum; DAS-ELISA; RT-PCR; Växtproduktionsvetenskap (växtpatologi / växtvirologi); Plant Production Science (Plant pathology / Plant virology); Kasvintuotantotieteet (kasvipatologia / kasvivirologia)

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

Chiunga, E. (2013). Viruses occurring in potatoes (Solanum tuberosum) in Mbeya region, Tanzania. (Masters Thesis). University of Helsinki. Retrieved from http://hdl.handle.net/10138/39459

Chicago Manual of Style (16^th Edition):

Chiunga, Evangelista. “Viruses occurring in potatoes (Solanum tuberosum) in Mbeya region, Tanzania.” 2013. Masters Thesis, University of Helsinki. Accessed January 21, 2021. http://hdl.handle.net/10138/39459.

MLA Handbook (7^th Edition):

Chiunga, Evangelista. “Viruses occurring in potatoes (Solanum tuberosum) in Mbeya region, Tanzania.” 2013. Web. 21 Jan 2021.

Vancouver:

Chiunga E. Viruses occurring in potatoes (Solanum tuberosum) in Mbeya region, Tanzania. [Internet] [Masters thesis]. University of Helsinki; 2013. [cited 2021 Jan 21]. Available from: http://hdl.handle.net/10138/39459.

Council of Science Editors:

Chiunga E. Viruses occurring in potatoes (Solanum tuberosum) in Mbeya region, Tanzania. [Masters Thesis]. University of Helsinki; 2013. Available from: http://hdl.handle.net/10138/39459

Arizona State University

29. Arababadi, Reza Arababadi. Operational and Technological Peak Load Shifting Strategies for Residential Buildings.

Degree: Civil Engineering, 2016, Arizona State University

URL: http://repository.asu.edu/items/38800

Subjects/Keywords: Energy; Sustainability; Energy efficiency; Energy modeling; Peak load; Pre cooling; Residential building; Solar PVs

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

Arababadi, R. A. (2016). Operational and Technological Peak Load Shifting Strategies for Residential Buildings. (Doctoral Dissertation). Arizona State University. Retrieved from http://repository.asu.edu/items/38800

Chicago Manual of Style (16^th Edition):

Arababadi, Reza Arababadi. “Operational and Technological Peak Load Shifting Strategies for Residential Buildings.” 2016. Doctoral Dissertation, Arizona State University. Accessed January 21, 2021. http://repository.asu.edu/items/38800.

MLA Handbook (7^th Edition):

Arababadi, Reza Arababadi. “Operational and Technological Peak Load Shifting Strategies for Residential Buildings.” 2016. Web. 21 Jan 2021.

Vancouver:

Arababadi RA. Operational and Technological Peak Load Shifting Strategies for Residential Buildings. [Internet] [Doctoral dissertation]. Arizona State University; 2016. [cited 2021 Jan 21]. Available from: http://repository.asu.edu/items/38800.

Council of Science Editors:

Arababadi RA. Operational and Technological Peak Load Shifting Strategies for Residential Buildings. [Doctoral Dissertation]. Arizona State University; 2016. Available from: http://repository.asu.edu/items/38800

University of Cincinnati

30. TEICA, ELENA. FORMAL CORRECTNESS AND COMPLETENESS FOR A SET OF UNINTERPRETED RTL TRANSFORMATIONS.

Degree: PhD, Engineering : Computer Science and Engineering, 2001, University of Cincinnati

URL: http://rave.ohiolink.edu/etdc/view?acc_num=ucin1001432470

► The work presented in this thesis is concerned with the correctness of the high-level synthesis process. In particular, it addresses transformational derivation (TD) systems. TD… (more)

▼ The work presented in this thesis is concerned with the correctness of the high-level synthesis process. In particular, it addresses transformational derivation (TD) systems. TD denominates a class of synthesis techniques wherein a register transfer level (RTL) implementation is derived by applying a sequence of behavior-preserving transformations to an initial behavior representation. We present in this thesis a formal treatment of correctness and completeness for a set of ten uninterpreted register transfer level transformations on which a TD system can be based. The formal definitions for RTL transformations are based on an uninterpreted model for RTL designs corresponding to straight-line code behavior descriptions. Our model specifies an abstract RTL design as a set of properties asserted about abstract collections (sets) of components (operators and registers). RTL transformations are functions operating on elements of the set defined by these properties, and the completeness property is a higher-order predicate that defines a complete set of functions. The specification and proof exercise are conducted in the Prototype Verification System (PVS). The use of PVS for the formal treatment presented in this thesis is justified not only by the typed higher-order logic that underlies its specification and proving environment (required by the very nature of the problem we are dealing with), but also by its rich language constructs that allow expressive and efficient specifications. As an alternative to an error prone axiomatic approach, each transformation is specified in a definitional manner. The correctness of each transformation is defined as the behavior preserving property: a transformation is correct if the extracted computational behavior of the output registers is the same in the initial and in the transformed design. Each transformation is mechanically proved correct in PVS based on the assumption that a set of preconditions is satisfied. A finite set of correct RTL transformations is said to be complete if and only if for any two RTL designs that implement the same behavior description, one design can be derived from the other by applying a finite sequence of transformations contained in this set. In other words, any possible implementation of a given behavior can be synthesized by applying only certain transformations to an initial implementation. We formalized and mechanically proved in PVS the completeness property using a constructive approach. The proof is constructive in the sense that a finite sequence of ransformations (belonging to the complete set), that transforms a certain design implementation into another one having the same behavior, is algorithmically defined. Some of the practical uses of the theoretical results formally established are: 1. A transformational derivation synthesis system based on the core set of RTL transformations presented here will yield correct-by-construction designs (if correctly implemented). The completeness property of this set ensures a virtually exhaustive search… Advisors/Committee Members: Vemuri, Dr. Ranga (Advisor).

Subjects/Keywords: RTL Transformations; Formal Synthesis; Correctness Behavior Preserving Completeness; Mechanized in Higher-Order Logics of PVS

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

TEICA, E. (2001). FORMAL CORRECTNESS AND COMPLETENESS FOR A SET OF UNINTERPRETED RTL TRANSFORMATIONS. (Doctoral Dissertation). University of Cincinnati. Retrieved from http://rave.ohiolink.edu/etdc/view?acc_num=ucin1001432470

Chicago Manual of Style (16^th Edition):

TEICA, ELENA. “FORMAL CORRECTNESS AND COMPLETENESS FOR A SET OF UNINTERPRETED RTL TRANSFORMATIONS.” 2001. Doctoral Dissertation, University of Cincinnati. Accessed January 21, 2021. http://rave.ohiolink.edu/etdc/view?acc_num=ucin1001432470.

MLA Handbook (7^th Edition):

TEICA, ELENA. “FORMAL CORRECTNESS AND COMPLETENESS FOR A SET OF UNINTERPRETED RTL TRANSFORMATIONS.” 2001. Web. 21 Jan 2021.

Vancouver:

TEICA E. FORMAL CORRECTNESS AND COMPLETENESS FOR A SET OF UNINTERPRETED RTL TRANSFORMATIONS. [Internet] [Doctoral dissertation]. University of Cincinnati; 2001. [cited 2021 Jan 21]. Available from: http://rave.ohiolink.edu/etdc/view?acc_num=ucin1001432470.

Council of Science Editors:

TEICA E. FORMAL CORRECTNESS AND COMPLETENESS FOR A SET OF UNINTERPRETED RTL TRANSFORMATIONS. [Doctoral Dissertation]. University of Cincinnati; 2001. Available from: http://rave.ohiolink.edu/etdc/view?acc_num=ucin1001432470

		in
And / Or
		in
And / Or
		in
And / Or
		in

Open Access Theses and Dissertations