No description available.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Cette thèse s'inscrit dans le domaine de la vérification formelle de programmes parallèles. L'enjeu de la vérification formelle est de s'assurer qu'un programme va bien fonctionner comme il le devrait, sans commettre d'erreur, se bloquer, ou se terminer anormalement. Cela est d'autant plus important dans le domaine du calcul parallèle, où le coût des calculs est parfois très élevé. Le modèle BSP (Bulk Synchronous Parallelism) est un modèle de parallélisme bien adapté à l'utilisation des méthodes formelles. Il garantit une forme de structure dans le programme parallèle, en l'organisant en super-étapes où chacune d'entre elle est composées d'une phase de calculs, puis d'une phase de communications entre les unités de calculs. Dans cette thèse, nous avons choisi d'étendre un outil actuel pour l'adapter à la preuve de programmes BSP. Nous nous sommes basés sur Why, un VCG (générateur de condition de vérification) qui a l'avantage de pouvoir s'interfacer avec plusieurs prouveurs automatiques et assistants de preuve pour décharger les obligations de preuves. Les contributions de cette thèse sont multiples. Dans un premier temps, nous présentons une comparaison des différentes librairies BSP disponibles, afin de mettre en évidence les primitives de programmation BSP les plus utilisées, donc les plus intéressantes à formaliser. Nous présentons ensuite BSP-Why, notre outil de preuve des programmes BSP. Cet outil se repose sur une génération d'un programme séquentiel qui simule le programme parallèle entré permettant ainsi d'utiliser Why et les nombreux prouveurs automatiques associés pour prouver les obligations de preuves. Nous montrons ensuite comment BSP-Why peut-être utilisé pour prouver la correction de quelques algorithmes BSP simples, mais aussi pour un exemple plus complexe qu'est la construction distribuée de l'espace d'états (model-checking) de systèmes et plus particulièrement dans les protocoles de sécurité. Enfin, afin de garantir la plus grande confiance dans l'outil BSP-Why, nous formalisons les sémantiques du langage, dans l'assistant de preuve Coq. Nous démontrons également la correction de la transformation utilisée pour passer d'un programme parallèle à un programme séquentiel / This thesis takes part in the formal verification of parallel programs. The aim of formal verification is to ensure that a program will run as it should, without making mistakes, blocking, or terminating abnormally. This is even more important in the parallel computation field, where the cost of calculations can be very high. The BSP model (Bulk Synchronous Parallelism) is a model of parallelism well suited for the use of formal methods. It guarantees a structure in the parallel program, by organising it into super-steps, each of them consisting of a phase of computations, then communications between the processes. In this thesis, we chose to extend an existing tool to adapt it for the proof of BSP programs. We based ourselves on Why, a VCG (verification condition generator) that has the advantage of being able to interface with several automatic provers and proof assistants to discharge the proof obligations. There are multiple contributions in this thesis. In a first part, we present a comparison of the existing BSP libraries, in order to show the most used BSP primitives, which are the most interesting to formalise. We then present BSP-Why, our tool for the proof of BSP programs. This tools uses a generation of a sequential program to simulate the parallel program in input, thus allowing the use of Why and the numerous associated provers to prove the proof obligations. We then show how BSP-Why can be used to prove the correctness of some basic BSP algorithms, and also on a more complex example, the generation of the state-space (model-checking) of systems, especially for security protocols. Finally, in order to ensure the greatest confidence in the BSP-Why tool, we give a formalisation of the language semantics, in the Coq proof assistant. We also prove the correctness of the transformation used to go from a parallel program to a sequential program

No description available.

No description available.

No description available.

Thesis advisor: William Ames / This thesis deals with the problem of visibility culling in interactive three-dimensional environments. Included in this thesis is a discussion surrounding the issues involved in both constructing and rendering three-dimensional environments. A renderer must sort the objects in a three-dimensional scene in order to draw the scene correctly. The Binary Space Partitioning (BSP) algorithm can sort objects in three-dimensional space using a tree based data structure. This thesis introduces the BSP algorithm in its original context before discussing its other uses in three-dimensional rendering algorithms. Constructive Solid Geometry (CSG) is an efficient interactive modeling technique that enables an artist to create complex three-dimensional environments by performing Boolean set operations on convex volumes. After providing a general overview of CSG, this thesis describes an efficient algorithm for computing CSG expression trees via the use of a BSP tree. When rendering a three-dimensional environment, only a subset of objects in the environment is visible to the user. We refer to this subset of objects as the Potentially Visible Set (PVS). This thesis presents an algorithm that divides an environment into a network of convex cellular volumes connected by invisible portal regions. A renderer can then utilize this network of cells and portals to compute a PVS via a depth first traversal of the scene graph in real-time. Finally, this thesis discusses how a simulation engine might exploit this data structure to provide dynamic collision detection against the scene graph. / Thesis (BA) — Boston College, 2004. / Submitted to: Boston College. College of Arts and Sciences. / Discipline: Computer Science. / Discipline: College Honors Program.

Made available in DSpace on 2014-06-12T17:40:58Z (GMT). No. of bitstreams: 2 arquivo7283_1.pdf: 2318820 bytes, checksum: de4d377d6069d0d647a95c3b45991629 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2007 / Universidade Federal de Pernambuco / As estruturas estritamente funcionais não demonstravam o que a empresa fazia, para quem fazia e nem como era feito. Esse modelo de gestão, a partir do final da década de oitenta, foi começando a se redirecionar para uma visão mais sistêmica, que propicia enormes ganhos de tempo na análise de resultados das intervenções nos processos organizacionais: a inexistência de uma visão dos processos organizacionais gera atividades redundantes e que não agregam nenhum valor aos seus clientes. A visão por processos prioriza a análise das funções de uma organização, desde uma ótica de atividades sequenciadas lógico-temporalmente. Foi com base nesta visão, que esta pesquisa se propôs a desenvolver um modelo de Sistema de Informação (SI), para cursos de pós-graduação lato sensu. A metodologia utilizada no planejamento dos SI s foi a BSP (Business System Planning), uma abordagem em que a base suporte aos sistemas de informação é o processo do negócio. Para construir a estrutura do SI da organização estudada neste trabalho, fez-se necessário identificar os dados, e como são compartilhados pelas funções e seus respectivos processos. O mapeamento dos processos permitiu a identificação de sistemas interfuncionais. Diante da limitação de recursos, o estudo BSP também viabilizou a ordem de implementação dos módulos de sistemas de informação, identificados com o uso desta metodologia. A utilização da BSP ratificou o consenso na literatura de que nenhum investimento em SI será satisfatório, se o planejamento do SI não estiver alinhado ao planejamento do negócio. Portanto, a tecnologia da informação (TI) e os recursos financeiros de uma organização não podem ser vistos como os seus únicos ingredientes de sucesso. O investimento deve ser decidido, considerando-se não apenas os ganhos financeiros, como também os ganhos estratégicos

Made available in DSpace on 2014-06-12T17:41:06Z (GMT). No. of bitstreams: 2 arquivo7292_1.pdf: 908414 bytes, checksum: 6690db636087abefc12b7e77b8b596e0 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2007 / O cenário atual das organizações tem sido de intensa competitividade impulsionada pelo avanço da tecnologia da informação e globalização da economia. Neste cenário econômico converter conhecimento em vantagem competitiva passa a ser um importante diferencial para organizações públicas ou privadas. Neste contexto, a capacidade de gerar, tratar e transmitir informação é a primeira etapa de uma cadeia de produção que se completa com sua aplicação no processo de agregação de valor a produtos e serviços. Neste sentido, este trabalho traz a proposição de um sistema de informação gerencial na integração dos processos de gestão da cadeia de suprimentos e área administrativo-financeira do DETRAN/AL, objetivando tornar mais eficaz o seu sistema de informação. Para solução da problemática em questão, foi utilizada a metodologia BSP Business System Planning para planejamento de sistema de informação. A escolha da metodologia BSP foi motivada por sua ênfase nos processos de negócio, proporcionado a construção de uma visão integrada da organização e constituindo-se num elo entre a estratégia organizacional, os processos de negócio e o modelo de sistema de informação proposto. Dessa forma, acredita-se que o resultado deste trabalho possa proporcionar aos gestores do DETRAN/AL os subsídios necessários para a tomada de decisão eficaz quanto ao modelo de sistema de informação a ser implantado, como também será de grande utilidade como fonte de pesquisa para outras organizações e demais interessados no tema aqui apresentado

Measuring the amount of bromsulfophthalein (BSP) retained in serum 30 minutes after intravenous injection can be used to evaluate hepatic function. BSP retention of less than 5% 30 minutes after intravenous administration is considered normal in dogs. The BSP retention test fell out of favor due to perceived inaccuracy when compared with bile acid and ammonia testing and a fear of hypersensitivity reactions. BSP was discontinued as a commercially-available drug in 1984. Use of BSP has continued at virginia tech despite the test's reputed disadvantages. The purpose of this study was to evaluate the efficacy of the BSP retention test in dogs with and without histopathologically-confirmed hepatobiliary disease. The medical records of 150 dogs with hepatobiliary disease having both a BSP retention test and hepatic biopsy performed were evaluated. Histopathologic slides were reviewed, and dogs were classified according to one of 11 predetermined histopathologic categories. Twenty-five random-source dogs were used as controls. Adverse effects following BSP administration were not observed in any dog. BSP retention was significantly different between hospitalized and control dogs, but the test could not distinguish between dogs with different types of hepatobiliary disease. Sensitivity, specificity, and predictive values of the BSP retention test were calculated, and its sensitivity was comparable to that of serum bile acid and ammonia testing. Using 6.0% retention as a cut-off for normal retention resulted in a specificity of 100%, sensitivity of 69.8%, positive predictive value of 100%, and negative predictive value of 35.7%. / Master of Science