A JML-Based strategy for incorporating formal specifications into the software development process

This thesis presents a JML-based strategy that incorporates formal specifications into the software development process of object-oriented programs. The strategy evolves functional requirements into a “semi-formal” requirements form, and then expressing them as JML formal specifications. The strategy is implemented as a formal-specification pseudo-phase that runs in parallel with the other phase of software development. What makes our strategy different from other software development strategies used in literature is the particular use of JML specifications we make all along the way from requirements to validation-and-verification.

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

Non-invasive strategy in assessing asthma through biofluids metabolomics exploration: exhaled breath and urine potentialities

Asthma is a significant health issue in the pediatric population with a noteworthy growth over the years. The proposed challenge for this PhD thesis was the development of advanced methodologies to establish metabolomic patterns in urine and exhaled breath associated with asthma whose applicability was subsequently exploited to evaluate the disease state, the therapy adhesion and effect and for diagnostic purposes. The volatile composition of exhaled breath was studied combining headspace solid phase microextraction (HS-SPME) with gas chromatography coupled to mass spectrometry or with comprehensive two-dimensional gas chromatography coupled to mass spectrometry with a high resolution time of flight analyzer (GC×GC–ToFMS). These methodologies allowed the identification of several hundred compounds from different chemical families. Multivariate analysis (MVA) led to the conclusion that the metabolomic profile of asthma individuals is characterized by higher levels of compounds associated with lipid peroxidation, possibly linked to oxidative stress and inflammation (alkanes and aldehydes) known to play an important role in asthma. For future applications in clinical settings a set of nine compounds was defined and the clinical applicability was proven in monitoring the disease status and in the evaluation of the effect and / or adherence to therapy. The global volatile metabolome of urine was also explored using an HSSPME/GC×GC–ToFMS method and c.a. 200 compounds were identified. A targeted analysis was performed, with 78 compounds related with lipid peroxidation and consequently to oxidative stress levels and inflammation. The urinary non-volatile metabolomic pattern of asthma was established using proton nuclear magnetic resonance (1H NMR). This analysis allowed identifying central metabolic pathways such as oxidative stress, amino acid and lipid metabolism, gut microflora alterations, alterations in the tricarboxylic acid (TCA) cycle, histidine metabolism, lactic acidosis, and modification of free tyrosine residues after eosinophil stimulation. The obtained results allowed exploring and demonstrating the potential of analyzing the metabolomic profile of exhaled air and urine in asthma. Besides the successful development of analysis methodologies, it was possible to explore through exhaled air and urine biochemical pathways affected by asthma, observing complementarity between matrices, as well as, verify the clinical applicability.

A new and improved strategy combining a dispersive-solid phase extraction-based multiclass method with ultra high pressure liquid chromatography for analysis of low molecular weight polyphenols in vegetables

This paper reports on the development and optimization of a modified Quick, Easy, Cheap Effective, Rugged and Safe (QuEChERS) based extraction technique coupled with a clean-up dispersive-solid phase extraction (dSPE) as a new, reliable and powerful strategy to enhance the extraction efficiency of free low molecular-weight polyphenols in selected species of dietary vegetables. The process involves two simple steps. First, the homogenized samples are extracted and partitioned using an organic solvent and salt solution. Then, the supernatant is further extracted and cleaned using a dSPE technique. Final clear extracts of vegetables were concentrated under vacuum to near dryness and taken up into initial mobile phase (0.1% formic acid and 20% methanol). The separation and quantification of free low molecular weight polyphenols from the vegetable extracts was achieved by ultrahigh pressure liquid chromatography (UHPLC) equipped with a phodiode array (PDA) detection system and a Trifunctional High Strength Silica capillary analytical column (HSS T3), specially designed for polar compounds. The performance of the method was assessed by studying the selectivity, linear dynamic range, the limit of detection (LOD) and limit of quantification (LOQ), precision, trueness, and matrix effects. The validation parameters of the method showed satisfactory figures of merit. Good linearity (View the MathML sourceRvalues2>0.954; (+)-catechin in carrot samples) was achieved at the studied concentration range. Reproducibility was better than 3%. Consistent recoveries of polyphenols ranging from 78.4 to 99.9% were observed when all target vegetable samples were spiked at two concentration levels, with relative standard deviations (RSDs, n = 5) lower than 2.9%. The LODs and the LOQs ranged from 0.005 μg mL−1 (trans-resveratrol, carrot) to 0.62 μg mL−1 (syringic acid, garlic) and from 0.016 μg mL−1 (trans-resveratrol, carrot) to 0.87 μg mL−1 ((+)-catechin, carrot) depending on the compound. The method was applied for studying the occurrence of free low molecular weight polyphenols in eight selected dietary vegetables (broccoli, tomato, carrot, garlic, onion, red pepper, green pepper and beetroot), providing a valuable and promising tool for food quality evaluation.