JML- Based formal development of a Java card application for managing medical appointments

Although formal methods can dramatically increase the quality of software systems, they have not widely been adopted in software industry. Many software companies have the perception that formal methods are not cost-effective cause they are plenty of mathematical symbols that are difficult for non-experts to assimilate. The Java Modelling Language (short for JML) Section 3.3 is an academic initiative towards the development of a common formal specification language for Java programs, and the implementation of tools to check program correctness. This master thesis work shows how JML based formal methods can be used to formally develop a privacy sensitive Java application. This is a smart card application for managing medical appointments. The application is named HealthCard. We follow the software development strategy introduced by João Pestana, presented in Section 3.4. Our work influenced the development of this strategy by providing hands-on insight on challenges related to development of a privacy sensitive application in Java. Pestana’s strategy is based on a three-step evolution strategy of software specifications, from informal ones, through semiformal ones, to JML formal specifications. We further prove that this strategy can be automated by implementing a tool that generates JML formal specifications from a welldefined subset of informal software specifications. Hence, our work proves that JML-based formal methods techniques are cost-effective, and that they can be made popular in software industry. Although formal methods are not popular in many software development companies, we endeavour to integrate formal methods to general software practices. We hope our work can contribute to a better acceptance of mathematical based formalisms and tools used by software engineers. The structure of this document is as follows. In Section 2, we describe the preliminaries of this thesis work. We make an introduction to the application for managing medical applications we have implemented. We also describe the technologies used in the development of the application. This section further illustrates the Java Card Remote Method Invocation communication model used in the medical application for the client and server applications. Section 3 introduces software correctness, including the design by contract and the concept of contract in JML. Section 4 presents the design structure of the application. Section 5 shows the implementation of the HealthCard. Section 6 describes how the HealthCard is verified and validated using JML formal methods tools. Section 7 includes some metrics of the HealthCard implementation and specification. Section 8 presents a short example of how a client-side of a smart card application can be implemented while respecting formal specifications. Section 9 describes a prototype tools to generate JML formal specifications from informal specifications automatically. Section 10 describes some challenges and main ideas came acrorss during the development of the HealthCard. The full formal specification and implementation of the HealthCard smart card application presented in this document can be reached at https://sourceforge.net/projects/healthcard/.

A situation awareness interface for a bi-wheeled industrial hovercraft: design, development and evaluation

The intention of this thesis is to develop a prototype interface that enables an operator to control a bi-wheeled industrial hovercraft that will work within a fusion power plant if the automation system fails. This fusion power plant is part of the ITER project a conjoint effort of various industrialized countries to develop cleaner sources of energy. The development of the interface prototype will be based on situation awareness concepts, which provide a means to understand how human operators perceive the world around, then process that information and make decisions based on the knowledge that they already have and the projected knowledge of the reactions that will occur in the world in response to the actions the operator makes. Two major situation awareness methods will be used, GDTA as a means to discover the requirements the interface needs to solve, and SAGAT to conduct the evaluation on the three interfaces. This technique can isolate the differences an operator has in situation awareness when presented with relevant information given by each of the three interfaces that were built for this thesis. Where the first interface presents the information within the operator’s focal point of view in a pictorial style, the second interface shows the same information within the same point of view has the first interface but only shows it in a textual manner. While the third interface shows the relevant information in the operator’s peripheral field of view. Also SAGAT can provide insight on the question to know if providing the operator with feed-forward information about the stoppage distances of the bi-wheeled industrial hovercraft has any effect on the operator’s decision making.

Finite Element Modeling for Development and Optimization of a Bone Plate for Mandibular Fracture in Dogs

This study aimed to develop a plate to treat fractures of the mandibular body in dogs and to validate the project using finite elements and biomechanical essays. Mandible prototypes were produced with 10 oblique ventrorostral fractures (favorable) and 10 oblique ventrocaudal fractures (unfavorable). Three groups were established for each fracture type. Osteosynthesis with a pure titanium plate of double-arch geometry and blocked monocortical screws offree angulanon were used. The mechanical resistance of the prototype with unfavorable fracture was lower than that of the fcworable fracture. In both fractures, the deflection increased and the relative stiffness decreased proportionally to the diminishing screw number The finite element analysis validated this plate study, since the maximum tension concentration observed on the plate was lower than the resistance limit tension admitted by the titanium. In conclusion, the double-arch geometry plate fixed with blocked monocortical screws has sufficient resistance to stabilize oblique,fractures, without compromising mandibular dental or neurovascular structures. J Vet Dent 24 (7); 212 - 221, 2010

Design, construction, and performance of a real-time holographic refractometry prototype for liquid analysis

Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq)

Development of a low-cost mobile mapping system: A South American experience

This paper presents the prototype of a low-cost terrestrial mobile mapping system (MMS) composed of a van, two digital video cameras, two GPS receivers, a notebook computer, and a sound frame synchronisation system. The imaging sensors are mounted as a stereo video camera on top of the vehicle together with the GPS antennae. The GPS receivers and the notebook computer are configured to record data referred to the vehicle position at a planned time interval. This position is subsequently transferred to the road images. This set of equipment and methods provide the opportunity to merge distinct techniques to make topographic maps and also to build georeferenced road image databases. Both vector maps and raster image databases, when integrated appropriately, can give spatial researchers and engineers a new technique whose application may realise better planning and analysis related to the road environment. The experimental results proved that the MMS developed at the São Paulo State University is an effective approach to inspecting road pavements, to map road marks and traffic signs, electric power poles, telephone booths, drain pipes, and many other applications important to people's safety and welfare. A small number of wad images have already been captured by the prototype as a consequence of its application in distinct projects. An efficient organisation of those images and the prompt access to them justify the need for building a georeferenced image database. By expanding it, both at the hardware and software levels, it is possible for engineers to analyse the entire road environment on their office computers.

Dynamic voltage restorer development and testing

The growing use of sensitive loads in the electric power system, especially in industrial applications, increases voltage sags related production losses considerably, stimulating a demand for power electronics' based solutions to mitigate the effects of such problems. This paper shows the implementation and some industrial certification tests of a power equipment prototype designed to correct sags and swells, a dynamic voltage restorer, which is one of the many possible solutions for voltage sags and swells problems Experimental results of a 75kVA prototype are shown both in laboratory and full load conditions, in a certification institution (IEE-USP). © 2011 IEEE.

Design and development of a low-cost solar tracker

To become competitive, ultimately, photovoltaics should have its costs reduced and use photovoltaic systems of greater efficiency. The main steps in this direction are the use of new materials, the improvement in the manufacture of modules and the adoption of techniques of maximum power point tracking and of solar tracking. This article aims at presenting the project and development of an azimuth and elevation solar tracker, based on a new conception of the positioning sensor, composed of an array of four photoresistors. The two direct current motors that operate in the vertical and horizontal axes are controlled by a proportional-integral microcontroller. The conditions of the project were low cost, small energy consumption and versatility. The microcontroller can also incorporate a maximum power point tracking algorithm. The performance of solar tracker prototype in the initial phase of field tests can be considered appropriate. © Institution of Engineers Australia, 2013.

Development of a knowledge-based system for cogeneration plant design: Verification, validation and lessons learned

This paper presents the development of a knowledge-based system (KBS) prototype able to design natural gas cogeneration plants, demonstrating new features for this field. The design of such power plants represents a synthesis problem, subject to thermodynamic constraints that include the location and sizing of components. The project was developed in partnership with the major Brazilian gas and oil company, and involved interaction with an external consultant as well as an interdisciplinary team. The paper focuses on validation and lessons learned, concentrating on important aspects such as the generation of alternative configuration schemes, breadth of each scheme description created by the system, and its module to support economic feasibility analysis. (C) 2014 Elsevier B.V. All rights reserved.

Development of heat sink device by using topology optimization

Small scale fluid flow systems have been studied for various applications, such as chemical reagent dosages and cooling devices of compact electronic components. This work proposes to present the complete cycle development of an optimized heat sink designed by using Topology Optimization Method (TOM) for best performance, including minimization of pressure drop in fluid flow and maximization of heat dissipation effects, aiming small scale applications. The TOM is applied to a domain, to obtain an optimized channel topology, according to a given multi-objective function that combines pressure drop minimization and heat transfer maximization. Stokes flow hypothesis is adopted. Moreover, both conduction and forced convection effects are included in the steady-state heat transfer model. The topology optimization procedure combines the Finite Element Method (to carry out the physical analysis) with Sequential Linear Programming (as the optimization algorithm). Two-dimensional topology optimization results of channel layouts obtained for a heat sink design are presented as example to illustrate the design methodology. 3D computational simulations and prototype manufacturing have been carried out to validate the proposed design methodology.

SED Stroop Effect Detector prototype

[ES] El Detector de Efectos Stroop (SED - Stroop Effect Detector), es una herramienta informática de asistencia, desarrollada a través del programa de investigación de Desarrollo Tecnológico Social de la Universidad de Las Palmas de Gran Canaria, que ayuda a profesionales del sector neuropsicológico a identificar problemas en la corteza orbitofrontal de un individuo, usándose para ello la técnica ideada por Schenker en 1998. Como base metodológica, se han utilizado los conocimientos adquiridos en las diferentes materias de la adaptación al grado en Ingeniería Informática como Gestión del Software, Arquitectura del Software y Desarrollo de Interfaces de Usuario así como conocimiento adquirido con anterioridad en asignaturas de Programación e Ingeniería del Software I y II. Como para realizar este proyecto sólo el conocimiento informático no era suficiente, he realizado una labor de investigación acerca del problema, teniendo que recopilar información de otros documentos científicos que abordan el tema, consultas a profesionales del sector como son el Doctor Don Ayoze Nauzet González Hernández, neurólogo del hospital Doctor Negrín de Las Palmas de Gran Canaria y el psicólogo Don José Manuel Rodríguez Pellejero que habló de este problema en clase del máster de Formación del Profesorado y que actualmente estoy cursando. Este trabajo presenta el test de Stroop con las dos versiones de Schenker: RCN (Reading Color Names) y NCW (Naming Colored Words). Como norma general, ambas pruebas presentan ante los sujetos estudios palabras (nombres de colores) escritas con la tinta de colores diferentes. De esta forma, el RCN consiste en leer la palabra escrita omitiendo la tonalidad de su fuente e intentando que no nos influya. Por el contrario, el NCW requiere enunciar el nombre del color de la tinta con la que está escrita la palabra sin que nos influya que ésta última sea el nombre de un color.

Development of musculoskeletal models for the design and the pre-clinical validation of hip resurfacing prosthesis

Background. The surgical treatment of dysfunctional hips is a severe condition for the patient and a costly therapy for the public health. Hip resurfacing techniques seem to hold the promise of various advantages over traditional THR, with particular attention to young and active patients. Although the lesson provided in the past by many branches of engineering is that success in designing competitive products can be achieved only by predicting the possible scenario of failure, to date the understanding of the implant quality is poorly pre-clinically addressed. Thus revision is the only delayed and reliable end point for assessment. The aim of the present work was to model the musculoskeletal system so as to develop a protocol for predicting failure of hip resurfacing prosthesis. Methods. Preliminary studies validated the technique for the generation of subject specific finite element (FE) models of long bones from Computed Thomography data. The proposed protocol consisted in the numerical analysis of the prosthesis biomechanics by deterministic and statistic studies so as to assess the risk of biomechanical failure on the different operative conditions the implant might face in a population of interest during various activities of daily living. Physiological conditions were defined including the variability of the anatomy, bone densitometry, surgery uncertainties and published boundary conditions at the hip. The protocol was tested by analysing a successful design on the market and a new prototype of a resurfacing prosthesis. Results. The intrinsic accuracy of models on bone stress predictions (RMSE < 10%) was aligned to the current state of the art in this field. The accuracy of prediction on the bone-prosthesis contact mechanics was also excellent (< 0.001 mm). The sensitivity of models prediction to uncertainties on modelling parameter was found below 8.4%. The analysis of the successful design resulted in a very good agreement with published retrospective studies. The geometry optimisation of the new prototype lead to a final design with a low risk of failure. The statistical analysis confirmed the minimal risk of the optimised design over the entire population of interest. The performances of the optimised design showed a significant improvement with respect to the first prototype (+35%). Limitations. On the authors opinion the major limitation of this study is on boundary conditions. The muscular forces and the hip joint reaction were derived from the few data available in the literature, which can be considered significant but hardly representative of the entire variability of boundary conditions the implant might face over the patients population. This moved the focus of the research on modelling the musculoskeletal system; the ongoing activity is to develop subject-specific musculoskeletal models of the lower limb from medical images. Conclusions. The developed protocol was able to accurately predict known clinical outcomes when applied to a well-established device and, to support the design optimisation phase providing important information on critical characteristics of the patients when applied to a new prosthesis. The presented approach does have a relevant generality that would allow the extension of the protocol to a large set of orthopaedic scenarios with minor changes. Hence, a failure mode analysis criterion can be considered a suitable tool in developing new orthopaedic devices.

Development of screening assays to test novel integrin antagonists in allergic inflammation

Aim of the research: to develop a prototype of homogeneous high-throughput screening (HTS) for identification of novel integrin antagonists for the treatment of ocular allergy and to better understand the mechanisms of action of integrin-mediated levocabastine antiallergic action. Results: This thesis provides evidence that adopting scintillation proximity assay (SPA) levocabastine (IC50=406 mM), but not the first-generation antihistamine chlorpheniramine, displaces [125I]fibronectin (FN) binding to human a4b1 integrin. This result is supported by flow cytometry analysis, where levocabastine antagonizes the binding of a primary antibody to integrin a4 expressed in Jurkat E6.1 cells. Levocabastine, but not chlorpheniramine, binds to a4b1 integrin and prevents eosinophil adhesion to VCAM-1, FN or human umbilical vein endothelial cells (HUVEC) cultured in vitro. Similarly, levocabastine affects aLb2/ICAM-1-mediated adhesion of Jurkat E6.1 cells. Analyzing the supernatant of TNF-a-treated (24h) eosinophilic cells (EoL-1), we report that levocabastine reduces the TNF-a-induced release of the cytokines IL-12p40, IL-8 and VEGF. Finally, in a model of allergic conjunctivitis, levocastine eye drops (0.05%) reduced the clinical aspects of the early and late phase reactions and the conjunctival expression of a4b1 integrin by reducing infiltrated eosinophils. Conclusions: SPA is a highly efficient, amenable to automation and robust binding assay to screen novel integrin antagonists in a HTS setting. We propose that blockade of integrinmediated cell adhesion might be a target of the anti-allergic action of levocabastine and may play a role in preventing eosinophil adhesion and infiltration in allergic conjunctivitis.

Development and evaluation of a 44 Ti, 44 Sc radionuclide generator and labeling of biomolecules with 44 Sc and 68 Ga for PET imaging

Non-invasive molecular-imaging technologies are playing a key role in drug discovery, development and delivery. Positron Emission Tomography (PET) is such a molecular imaging technology and a powerful tool for the observation of various deceases in vivo. However, it is limited by the availability of vectors with high selectivity to the target and radionuclides with a physical half-life which matches the biological half-life of the observed process. The 68Ge/68Ga radionuclide generator makes the PET-nuclide anywhere available without an on-site cyclotron. Besides the perfect availability 68Ga shows well suited nuclide properties for PET, but it has to be co-ordinated by a chelator to introduce it in a radiopharmaceuticals.rnHowever, the physical half-life of 68Ga (67.7 min) might limit the spectrum of clinical applications of 68Ga-labelled radiodiagnostics. Furthermore, 68Ga-labelled analogues of endoradiotherapeuticals of longer biological half-live such as 90Y- or 177Lu-labeled peptides and proteins cannot be used to determine individual radiation dosimetry directly. rnThus, radionuclide generator systems providing positron emitting daughters of extended physical half-life are of renewed interest. In this context, generator-derived positron emitters with longer physical half-life are needed, such as 72As (T½ = 26 h) from the 72Se/72As generator, or 44Sc (T½ = 3.97 h) from the 44Ti/44Sc generator.rnIn this thesis the implementation of radioactive gallium-68 and scandium-44 for molecular imaging and nuclear medical diagnosis, beginning with chemical separation and purification of 44Ti as a radionuclide mother, investigation of pilot generators with different elution mode, building a prototype generator, development and investigation of post-processing of the generator eluate, its concentration and further purification, the labeling chemistry under different conditions, in vitro and in vivo studies of labeled compounds and, finally, in vivo imaging experiments are described.

Technology Development and Consumer Acceptance of Innovation in Fruit Production

Precision Agriculture (PA) and the more specific branch of Precision Horticulture are two very promising sectors. They focus on the use of technologies in agriculture to optimize the use of inputs, so to reach a better efficiency, and minimize waste of resources. This important objective motivated many researchers and companies to search new technology solutions. Sometimes the effort proved to be a good seed, but sometimes an unfeasible idea. So that PA, from its birth more or less 25 years ago, is still a “new” management, interesting for the future, but an actual low adoption rate is still reported by experts and researchers. This work aims to give a contribution in finding the causes of this low adoption rate and proposing a methodological solution to this problem. The first step was to examine prior research about Precision Agriculture adoption, by ex ante and ex post approach. It was supposed as important to find connections between these two phases of a purchase experience. In fact, the ex ante studies dealt with potential consumer’s perceptions before a usage experience occurred, therefore before purchasing a technology, while the ex post studies described the drivers which made a farmer become an end-user of PA technology. Then, an example of consumer research is presented. This was an ex ante research focused on pre-prototype technology for fruit production. This kind of research could give precious information about consumer acceptance before reaching an advanced development phase of the technology, and so to have the possibility to change something with the least financial impact. The final step was to develop the pre-prototype technology that was the subject of the consumer acceptance research and test its technical characteristics.

Development of a microgrid with renewable energy sources and electrochemical storage system integration

Beside the traditional paradigm of "centralized" power generation, a new concept of "distributed" generation is emerging, in which the same user becomes pro-sumer. During this transition, the Energy Storage Systems (ESS) can provide multiple services and features, which are necessary for a higher quality of the electrical system and for the optimization of non-programmable Renewable Energy Source (RES) power plants. A ESS prototype was designed, developed and integrated into a renewable energy production system in order to create a smart microgrid and consequently manage in an efficient and intelligent way the energy flow as a function of the power demand. The produced energy can be introduced into the grid, supplied to the load directly or stored in batteries. The microgrid is composed by a 7 kW wind turbine (WT) and a 17 kW photovoltaic (PV) plant are part of. The load is given by electrical utilities of a cheese factory. The ESS is composed by the following two subsystems, a Battery Energy Storage System (BESS) and a Power Control System (PCS). With the aim of sizing the ESS, a Remote Grid Analyzer (RGA) was designed, realized and connected to the wind turbine, photovoltaic plant and the switchboard. Afterwards, different electrochemical storage technologies were studied, and taking into account the load requirements present in the cheese factory, the most suitable solution was identified in the high temperatures salt Na-NiCl2 battery technology. The data acquisition from all electrical utilities provided a detailed load analysis, indicating the optimal storage size equal to a 30 kW battery system. Moreover a container was designed and realized to locate the BESS and PCS, meeting all the requirements and safety conditions. Furthermore, a smart control system was implemented in order to handle the different applications of the ESS, such as peak shaving or load levelling.