Sistemas de Tipos para Verificación de Programas Concurrentes. Type Systems for Concurrent Programs Verification.

La programación concurrente es una tarea difícil aún para los más experimentados programadores. Las investigaciones en concurrencia han dado como resultado una gran cantidad de mecanismos y herramientas para resolver problemas de condiciones de carrera de datos y deadlocks, problemas que surgen por el mal uso de los mecanismos de sincronización. La verificación de propiedades interesantes de programas concurrentes presenta dificultades extras a los programas secuenciales debido al no-determinismo de su ejecución, lo cual resulta en una explosión en el número de posibles estados de programa, haciendo casi imposible un tratamiento manual o aún con la ayuda de computadoras. Algunos enfoques se basan en la creación de lenguajes de programación con construcciones con un alto nivel de abstración para expresar concurrencia y sincronización. Otros enfoques tratan de desarrollar técnicas y métodos de razonamiento para demostrar propiedades, algunos usan demostradores de teoremas generales, model-checking o algortimos específicos sobre un determinado sistema de tipos. Los enfoques basados en análisis estático liviano utilizan técnicas como interpretación abstracta para detectar ciertos tipos de errores, de una manera conservativa. Estas técnicas generalmente escalan lo suficiente para aplicarse en grandes proyectos de software pero los tipos de errores que pueden detectar es limitada. Algunas propiedades interesantes están relacionadas a condiciones de carrera y deadlocks, mientras que otros están interesados en problemas relacionados con la seguridad de los sistemas, como confidencialidad e integridad de datos. Los principales objetivos de esta propuesta es identificar algunas propiedades de interés a verificar en sistemas concurrentes y desarrollar técnicas y herramientas para realizar la verificación en forma automática. Para lograr estos objetivos, se pondrá énfasis en el estudio y desarrollo de sistemas de tipos como tipos dependientes, sistema de tipos y efectos, y tipos de efectos sensibles al flujo de datos y control. Estos sistemas de tipos se aplicarán a algunos modelos de programación concurrente como por ejemplo, en Simple Concurrent Object-Oriented Programming (SCOOP) y Java. Además se abordarán propiedades de seguridad usando sistemas de tipos específicos. Concurrent programming has remained a dificult task even for very experienced programmers. Concurrency research has provided a rich set of tools and mechanisms for dealing with data races and deadlocks that arise of incorrect use of synchronization. Verification of most interesting properties of concurrent programs is a very dificult task due to intrinsic non-deterministic nature of concurrency, resulting in a state explosion which make it almost imposible to be manually treat and it is a serious challenge to do that even with help of computers. Some approaches attempts create programming languages with higher levels of abstraction for expressing concurrency and synchronization. Other approaches try to develop reasoning methods to prove properties, either using general theorem provers, model-checking or specific algorithms on some type systems. The light-weight static analysis approach apply techniques like abstract interpretation to find certain kind of bugs in a conservative way. This techniques scale well to be applied in large software projects but the kind of bugs they may find are limited. Some interesting properties are related to data races and deadlocks, while others are interested in some security problems like confidentiality and integrity of data. The main goals of this proposal is to identify some interesting properties to verify in concurrent systems and develop techniques and tools to do full automatic verification. The main approach will be the application of type systems, as dependent types, type and effect systems, and flow-efect types. Those type systems will be applied to some models for concurrent programming as Simple Concurrent Object-Oriented Programming (SCOOP) and Java. Other goals include the analysis of security properties also using specific type systems.

Automating the testing process of image processing algorithms

As digital imaging processing techniques become increasingly used in a broad range of consumer applications, the critical need to evaluate algorithm performance has become recognised by developers as an area of vital importance. With digital image processing algorithms now playing a greater role in security and protection applications, it is of crucial importance that we are able to empirically study their performance. Apart from the field of biometrics little emphasis has been put on algorithm performance evaluation until now and where evaluation has taken place, it has been carried out in a somewhat cumbersome and unsystematic fashion, without any standardised approach. This paper presents a comprehensive testing methodology and framework aimed towards automating the evaluation of image processing algorithms. Ultimately, the test framework aims to shorten the algorithm development life cycle by helping to identify algorithm performance problems quickly and more efficiently.

Optimising the design and manufacture of a customised, prescription fit, Maxillo-facial prosthesis

This thesis is a continuation of the Enterprise-Ireland Research Innovation Fund (RIF) Project entitled’ "Design and Manufacturing of Customised Maxillo-Facial Prostheses" The primary objective of this Internal Research Development Program (IRDP) project was to investigate two fundamental design changes 1 To incorporate the over-denture abutments directly into the implant. 2 To remove the restraining wings by the addition of screws, which affix the. implant to the dense material of the jawbone. The prosthetic was redesigned using the ANSYS Finite Element Analysis software program and analysed to* • Reduce the internal von Mises stress distribution The new prosthetic had a -63.63 % lower von Mises stress distribution when compared with the original prosthetic. • Examine the screw preload effects. A maximum relative displacement of 22 6 * lO^mm between the bone and screw was determined, which is well below the critical threshold of micromotion which prevents osseointegration • Investigate the prosthetic-bone contact interface. Three models of the screw, prosthesis, and bone, were studied. (Axisymmetnc, quarter volume, and full volume), a recommended preload torque of 0 32 Nm was applied to the prosthetic and a maximum von Mises stress of 1.988 MPa was predicted • Study the overdenture removal forces. This analysis could not be completed because the correct plastic multilinear properties of the denture material could not be established The redesigned prosthetic was successfully manufactured on a 3-axis milling machine with an indexing system The prosthetic was examined for dimensional quality and strength The research established the feasibility of the new design and associated manufacturing method.

An investigation into system security requirements and implementation in an Application Service Provider (ASP) environment

Although the ASP model has been around for over a decade, it has not achieved the expected high level of market uptake. This research project examines the past and present state of ASP adoption and identifies security as a primary factor influencing the uptake of the model. The early chapters of this document examine the ASP model and ASP security in particular. Specifically, the literature and technology review chapter analyses ASP literature, security technologies and best practices with respect to system security in general. Based on this investigation, a prototype to illustrate the range and types of technologies that encompass a security framework was developed and is described in detail. The latter chapters of this document evaluate the practical implementation of system security in an ASP environment. Finally, this document outlines the research outputs, including the conclusions drawn and recommendations with respect to system security in an ASP environment. The primary research output is the recommendation that by following best practices with respect to security, an ASP application can provide the same level of security one would expect from any other n-tier client-server application. In addition, a security evaluation matrix, which could be used to evaluate not only the security of ASP applications but the security of any n-tier application, was developed by the author. This thesis shows that perceptions with regard to fears of inadequate security of ASP solutions and solution data are misguided. Finally, based on the research conducted, the author recommends that ASP solutions should be developed and deployed on tried, tested and trusted infrastructure. Existing Application Programming Interfaces (APIs) should be used where possible and security best practices should be adhered to where feasible.

Instrumentation and software for the VERITAS Project and the detection of TeV Gamma-Ray Emission from the BL Lacertae Object 1ES1959+650

Transmission of Cherenkov light through the atmosphere is strongly influenced by the optical clarity of the atmosphere and the prevailing weather conditions. The performance of telescopes measuring this light is therefore dependent on atmospheric effects. This thesis presents software and hardware developed to implement a prototype sky monitoring system for use on the proposed next-generation gamma-ray telescope array, VERITAS. The system, consisting of a CCD camera and a far-infrared pyrometer, was successfully installed and tested on the ten metre atmospheric Cherenkov imaging telescope operated by the VERITAS Collaboration at the F.L. Whipple Observatory in Arizona. The thesis also presents the results of observations of the BL Lacertae object, 1ES1959+650, made with the Whipple ten metre telescope. The observations provide evidence for TeV gamma-ray emission from the BL Lacertae object, 1ES1959+650, at a level of more than 15 standard deviations above background. This represents the first unequivocal detection of this object at TeV energies, making it only the third extragalactic source seen at such levels of significance in this energy range. The flux variability of the source on a number of timescales is also investigated.

Design, development and testing of a CAD integrated design for environment software tool.

The research described in this thesis was developed as part o f the Information Management for Green Design (IMA GREE) Project. The 1MAGREE Project was founded by Enterprise Ireland under a Strategic Research Grant Scheme as a partnership project between Galway Mayo Institute o f Technology and C1MRU University College Galway. The project aimed to develop a CAD integrated software tool to support environmental information management for design, particularly for the electronics-manufacturing sector in Ireland.

Georgia: National Security Concept Versus National Security

საქართველოს ეროვნული უსაფრთხოების კონცეფციის განახლებული ვერსიის გამოჩენა შესაძლებლობას იძლევა საიმისოდ, რომ გადავხედოთ საქართველოს ოფიციალურ შეხედულებას უსაფრთხოების შესახებ და შევაფასოთ ქვეყნის დამოკიდებულება საშინაო თუ საგარეო უსაფრთხოების გარემოსადმი;სტატია, პირველ რიგში, განიხილავს საქართველოს ეროვნული უსაფრთხოების დაგეგმვის გარემოებებს. შემდეგ ჩამოთვლილია კონცეფიციის პოზიტიური ასპექტები. ანალიზის ძირითადი ნაწილი მოიცავს ხუთ პრობლემატურ საკითხს. პირველი არის შიდა არასტაბილურობის შესაძლებლობა, რომლის შესახებ კონცეფციაში არაფერია ნათქვამი. მეორე საკითხი ეხება გლობალიზაციისა და ურთიერთდამოკიდებულების უსაფრთხოების ასპექტებს. მესამე საკითხი მოიცავს სამხრეთ კავკასიის რეგიონში არსებულ საფრთხეებს, კერძოდ კი, მთიანი ყარაბახის კონფლიქტს და არასტაბილურ მდგომარეობას ჩრდილოეთ კავკასიაში. მეოთხე საკითხი არის რუსეთისგან მომავალი საფრთხე. ბოლოს, განხილულია საქართველოს დასავლური ორიენტაცია.

Critical Care in in Neurology

Neurocritical care is an ever-changing field. The publishers and author of The Flying Publisher Guide to Critical Care in Neurology have made every effort to provide information that is accurate and complete as of the date of publication. However, in view of the rapid changes occurring in medical science, as well as the possibility of human error, this site may contain technical inaccuracies, typographical or other errors. It is the responsibility of the reading physician who must rely on experience and knowledge about the patient to determine the best treatment and care pathway. The information contained herein is provided “as is”, without warranty of any kind. The contributors to this book, including Flying Publisher & Kamps, disclaim responsibility for any errors or omissions or for results obtained from the use of information contained herein.

Software livre e de código aberto para avaliação de imagens de angiotomografia de coronárias

FUNDAMENTO: A estandardização do padrão de imagens utilizada dentro da medicina foi realizada em 1993 por meio do padrão DICOM (Digital Imaging and Communications in Medicine). Diversos exames utilizam esse padrão e cada vez mais são necessários softwares capazes de manipular esse tipo de imagem, porém esses softwares geralmente não têm o formato livre e de código aberto, e isso dificulta o seu ajuste para os mais diferentes interesses. OBJETIVO: Desenvolver e validar um software livre e de código aberto capaz de manipular imagens DICOM de exames de angiotomografia de coronárias. MÉTODOS: Desenvolvemos e testamos o software intitulado ImageLab na avaliação de 100 exames selecionados de forma randômica por meio de um banco de dados. Foram realizadas 600 análises divididas por dois observadores utilizando o ImageLab e um outro software comercializado junto a aparelhos de tomografia computadorizada Philips Brilliance, na avaliação da presença de lesões e placas coronarianas nos territórios do Tronco da Coronária Esquerda (TCE) e na Artéria Descendente Anterior (ADA). Para avaliar as concordâncias intraobservador, interobservadores e intersoftware, utilizamos concordância simples e estatística Kappa. RESULTADOS: As concordâncias observadas entre os softwares foram em geral classificadas como substancial ou quase perfeitas na maioria das comparações. CONCLUSÃO: O software ImageLab concordou com o software Philips na avaliação de exames de angiotomografia de coronárias especialmente em pacientes sem lesões, com lesões inferiores a 50% no TCE e inferiores a 70% na ADA. A concordância para lesão >70% na ADA foi menor, porém isso também é observado quando se utiliza o padrão de referência anatômico.

Composition and construction of embedded software families

Feature modeling, embebbed software, software product lines, tool support

Towards flexible feature composition : static and dynamic binding in software product lines

Magdeburg, Univ., Fak. für Informatik, Diss., 2011

Reflective and adaptive middleware for software evolution of information systems

Magdeburg, Univ., Fak. für Informatik, Diss., 2007

role of features and aspects in software development

Feature-Oriented Programming, Aspect-Oriented Programming, Software Product Lines, Stepwise Development

SMPI model : a stepwise process model to facilitate software measurement process improvement along the measurement paradigms

Software engineering, software measurement, software process engineering, capability, maturity