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/.

New metallomolecular wires based on carbon-rich bridging systems: a systematic study

This dissertation presents and discusses the preparation of molecular wires (MW) candidates that would then be probed for electron transfer properties. These wires are bridged by 1,4-diethynylbenzene derivatives with alkoxy side chains with palladium and ruthenium metal complex termini. Characterization of these compounds was performed by usual spectroscopic techniques like 1H, 13C{1H} and 31P{1H} NMR, MS, FTIR and UV-Vis as well as by cyclic voltammetry which allowed classifying the candidates in the Robin–Day system and determination of bridges side chain and length effects on electronic transport. Preparation of the 1,4-diethynylbenzene derivatives was done with synthetic pathways that relied heavily in palladium catalyzed cross-couplings (Sonogashira). A family of single ringed 1,4-diethynylbenzene ligands with different length alkoxy side chains (OCH3, OC2H5, OC7H15) was thus prepared allowing for the influence of these ring decorations to be assessed. The ruthenium binuclear rods showed communication between metal centres only when the shorter ligands were used whereas the longer Ru complexes showed only one redox pair in CV studies which is in agreement to non-communicating metal centres. Cyclic voltammetry studies show irreversible one wave processes for palladium dinuclear complexes, making these rods function as molecular insulators. Fluorescence decay studies performed on the prepared compounds (ligands and complexes) show a pattern of decreasing decay times upon coordination to the metal centres which can due to ligand charge redistribution upon coordination leading to non-radiative relaxation paths. Regarding the X-ray structures, two new ligand related structures were obtained as well as new structure for a palladium rod. The effect of the side chains was observed to be important to the wires’ electronic properties when comparing with the analogues without a side chain. The effect brought by longer chains is nevertheless almost negligible.

Classification of Boal, Malvazia, Sercial and Verdelho wines based on terpenoid patterns

Thirty-six Madeira wine samples from Boal, Malvazia, Sercial and Verdelho white grape varieties were analyzed in order to estimate the free fraction of monoterpenols and C13 norisoprenoids (terpenoid compounds) using dynamic headspace solid phase micro-extraction (HS-SPME) technique coupled with gas chromatography–mass spectrometry (GC–MS). The average values from three vintages (1998–2000) show that these wines have characteristic profiles of terpenoid compounds. Malvazia wines exhibits the highest values of total free monoterpenols, contrary to Verdelho wines which had the lowest levels of terpenoids but produced the highest concentration of farnesol. The use of multivariate analysis techniques allows establishing relations between the compounds and the varieties under investigation. Principal component analysis (PCA) and linear discriminant analysis (LDA) were applied to the obtained matrix data. A good separation and classification power between the four groups as a function of their varietal origin was observed.

Effectiveness of high-throughput miniaturized sorbent- and solid phase microextraction techniques combined with gas chromatography–mass spectrometry analysis for a rapid screening of volatile and semi-volatile composition of wines: a comparative study

In this study the feasibility of different extraction procedures was evaluated in order to test their potential for the extraction of the volatile (VOCs) and semi-volatile constituents (SVOCs) from wines. In this sense, and before they could be analysed by gas chromatography–quadrupole first stage masss spectrometry (GC–qMS), three different high-throughput miniaturized (ad)sorptive extraction techniques, based on solid phase extraction (SPE), microextraction by packed sorbents (MEPS) and solid phase microextraction (SPME), were studied for the first time together, for the extraction step. To achieve the most complete volatile and semi-volatile signature, distinct SPE (LiChrolut EN, Poropak Q, Styrene-Divinylbenzene and Amberlite XAD-2) and MEPS (C2, C8, C18, Silica and M1 (mixed C8-SCX)) sorbent materials, and different SPME fibre coatings (PA, PDMS, PEG, DVB/CAR/PDMS, PDMS/DVB, and CAR/PDMS), were tested and compared. All the extraction techniques were followed by GC–qMS analysis, which allowed the identification of up to 103 VOCs and SVOCs, distributed by distinct chemical families: higher alcohols, esters, fatty acids, carbonyl compounds and furan compounds. Mass spectra, standard compounds and retention index were used for identification purposes. SPE technique, using LiChrolut EN as sorbent (SPELiChrolut EN), was the most efficient method allowing for the identification of 78 VOCs and SVOCs, 63 and 19 more than MEPS and SPME techniques, respectively. In MEPS technique the best results in terms of number of extractable/identified compounds and total peak areas of volatile and semi-volatile fraction, were obtained by using C8 resin whereas DVB/CAR/PDMS was revealed the most efficient SPME coating to extract VOCs and SVOCs from Bual wine. Diethyl malate (18.8 ± 3.2%) was the main component found in wine SPELiChrolut EN extracts followed by ethyl succinate (13.5 ± 5.3%), 3-methyl-1-butanol (13.2 ± 1.7%), and 2-phenylethanol (11.2 ± 9.9%), while in SPMEDVB/CAR/PDMS technique 3-methyl-1-butanol (43.3 ± 0.6%) followed by diethyl succinate (18.9 ± 1.6%), and 2-furfural (10.4 ± 0.4%), are the major compounds. The major VOCs and SVOCs isolated by MEPSC8 were 3-methyl-1-butanol (26.8 ± 0.6%, from wine total volatile fraction), diethyl succinate (24.9 ± 0.8%), and diethyl malate (16.3 ± 0.9%). Regardless of the extraction technique, the highest extraction efficiency corresponds to esters and higher alcohols and the lowest to fatty acids. Despite some drawbacks associated with the SPE procedure such as the use of organic solvents, the time-consuming and tedious sampling procedure, it was observed that SPELiChrolut EN, revealed to be the most effective technique allowing the extraction of a higher number of compounds (78) rather than the other extraction techniques studied.

Low generation triazine-based dendrimers-synthesis, characterzation and in vitro biological activity

In the present study, two low generation triazine-based dendrimers, G1.0(Cl)4 dendrimer and G1.5(OH)8 dendrimer, were synthesized and their cytotoxicity were tested by using the NIH 3T3 and the A2780 cell lines. In the synthesis process of the G1.0(Cl)4 dendrimer, cyanuric chloride (CAC) which has high reactivity chlorine atom was connected to the terminal of triethylene glycol (TEG) via nucleophilic substitution by controlling temperature. The prepared G1.0(Cl)4 dendrimer was purified by silica gel column chromatography. Then the four chlorine atoms in the G1.0(Cl)4 dendrimer were substituted by diethanolamine (DEA) to give dendrimer with the hydroxyl terminal group G1.5(OH)8. The starting materials, CAC, G1.0(Cl)4 dendrimer and G1.5(OH)8 dendrimer were analyzed by one-dimensional NMR, FTIR and MS techniques. The two dendrimers, G1.0(Cl)4 and G1.5(OH)8, showed perfect stability in the air environment at room temperature. However, G1.0(Cl)4 is not soluble in water while the G1.5(OH)8 dendrimer is a water soluble compound. Furthermore, cell biological evaluation at the studied concentrations showed that the CAC, as well as the prepared G1.0(Cl)4 and G1.5(OH)8 dendrimers, have no cytotoxicity towards the NIH 3T3 and A2780 cell lines.