Constraint-based verification of imperative programs

work presented in the context of the European Master’s program in Computational Logic, as the partial requirement for obtaining Master of Science degree in Computational Logic

Synthesis about a collaborative project on “Technology Assessment of Autonomous System

The project started in 2009 with the support of DAAD in Germany and CRUP in Portugal under the “Collaborative German-Portuguese University Actions” programme. One central goal is the further development of a theory of technology assessment applied to robotics and autonomous systems in general that reflects in its methodology the changing conditions of knowledge production in modern societies and the emergence of new robotic technologies and of associated disruptive changes. Relevant topics here are handling broadened future horizons and new clusters of science and technology (medicine, engineering, interfaces, industrial automation, micro-devices, security and safety), as well as new governance structures in policy decision making concerning research and development (R

Verification of analog circuits in power-down mode

Dissertação para obtenção do Grau de Mestre em Engenharia Eletrotécnica e Computadores

A comparison between digital breast tomosynthesis and mammography: dosimetric and image quality characterization of clinical system

Dissertação para obtenção do Grau de Mestre em Engenharia Biomédica

Planning and verification of multipath routing protocols

Conventionally the problem of the best path in a network refers to the shortest path problem. However, for the vast majority of networks present nowadays this solution has some limitations which directly affect their proper functioning, as well as an inefficient use of their potentialities. Problems at the level of large networks where graphs of high complexity are commonly present as well as the appearing of new services and their respective requirements, are intrinsically related to the inability of this solution. In order to overcome the needs present in these networks, a new approach to the problem of the best path must be explored. One solution that has aroused more interest in the scientific community considers the use of multiple paths between two network nodes, where they can all now be considered as the best path between those nodes. Therefore, the routing will be discontinued only by minimizing one metric, where only one path between nodes is chosen, and shall be made by the selection of one of many paths, thereby allowing the use of a greater diversity of the present paths (obviously, if the network consents). The establishment of multi-path routing in a given network has several advantages for its operation. Its use may well improve the distribution of network traffic, improve recovery time to failure, or it can still offer a greater control of the network by its administrator. These factors still have greater relevance when networks have large dimensions, as well as when their constitution is of high complexity, such as the Internet, where multiple networks managed by different entities are interconnected. A large part of the growing need to use multipath protocols is associated to the routing made based on policies. Therefore, paths with different characteristics can be considered with equal level of preference, and thus be part of the solution for the best way problem. To perform multi-path routing using protocols based only on the destination address has some limitations but it is possible. Concepts of graph theory of algebraic structures can be used to describe how the routes are calculated and classified, enabling to model the routing problem. This thesis studies and analyzes multi-path routing protocols from the known literature and derives a new algebraic condition which allows the correct operation of these protocols without any network restriction. It also develops a range of software tools that allows the planning and the respective verification/validation of new protocols models according to the study made.

A proof system for lock-free concurrency

Dissertação para obtenção do Grau de Mestre em Engenharia Informática

Integration of a mobile autonomous robot in a surveillance multi-agent system

This dissertation aims to guarantee the integration of a mobile autonomous robot equipped with many sensors in a multi-agent distributed and georeferenced surveillance system. The integration of a mobile autonomous robot in this system leads to new features that will be available to clients of surveillance system may use. These features may be of two types: using the robot as an agent that will act in the environment or by using the robot as a mobile set of sensors. As an agent in the system, the robot can move to certain locations when alerts are received, in order to acknowledge the underlying events or take to action in order to assist in resolving this event. As a sensor platform in the system, it is possible to access information that is read from the sensors of the robot and access complementary measurements to the ones taken by other sensors in the multi-agent system. To integrate this mobile robot in an effective way it is necessary to extend the current multi-agent system architecture to make the connection between the two systems and to integrate the functionalities provided by the robot into the multi-agent system.

Design, implementation, and performance of a distributed and scalable sensor system for critical distance measurements in the CMS detector at LHC

The “CMS Safety Closing Sensors System” (SCSS, or CSS for brevity) is a remote monitoring system design to control safety clearance and tight mechanical movements of parts of the CMS detector, especially during CMS assembly phases. We present the different systems that makes SCSS: its sensor technologies, the readout system, the data acquisition and control software. We also report on calibration and installation details, which determine the resolution and limits of the system. We present as well our experience from the operation of the system and the analysis of the data collected since 2008. Special emphasis is given to study positioning reproducibility during detector assembly and understanding how the magnetic fields influence the detector structure.

Technical optimization of the synthesis of flavours

The goal of this thesis is the investigation and optimization of the synthesis of potential fragrances. This work is projected as collaboration between the University of Applied Sciences in Merseburg and the company Miltitz Aromatics GmbH in Bitterfeld‐Wolfen (Germany). Flavoured compounds can be synthesized in different ways and by various methods. In this work, methods like the phase transfer catalysis and the Cope‐rearrangement were investigated and applied, for getting a high yield and quantity of the desired substances and without any by‐products or side reactions. This involved the study of syntheses with different process parameters such as temperature, solvent, pressure and reaction time. The main focus was on Cope‐rearrangement, which is a common method in the synthesis of new potential fragrance compounds. The substances synthesized in this work have a hepta‐1,5‐diene‐structure and that is why they can easily undergo this [3,3]‐sigma tropic rearrangement. The lead compound of all research was 2,5‐dimethyl‐2‐vinyl‐4‐hexenenitrile (Neronil). Neronil is synthesized by an alkylation of 2‐methyl‐3‐butenenitrile with prenylchloride under basic conditions in a phase‐transfer system. In this work the yield of isolated Neronil is improved from about 35% to 46% by according to the execution conditions of the reaction. Additionally the amount of side product was decreased. This synthesized hexenenitrile involved not only the aforementioned 1,5‐diene‐structure, but also a cyano group, that makes this structure a suitable base for the synthesis of new potential fragrance compounds. It was observed that Neronil can be transferred into 2,5‐dimethyl‐2‐vinyl‐4‐hexenoic acid by a hydrolysis under basic conditions. After five hours the acid can be obtained with a yield of 96%. The following esterification is realized with isobutanol to produce 2,5‐dimethyl‐2‐vinyl‐4‐hexenoic acid isobutyl ester with quantitative conversion. It was observed that the Neronil and the corresponding ester can be converted into the corresponding Cope‐product, with a conversion of 30 % and 80%. Implementing the Cope‐rearrangement, the acid was heated and an unexpected decarboxylated product is formed. To achieve the best verification of reaction development and structure, scrupulous analyses were done using GC‐MS, 1H‐NMR and 13C‐ NMR.