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

Solid phase microextraction as a reliable alternative to conventional extraction techniques to evaluate the pattern of hydrolytically released components in Vitis vinifera L. grapes

In present research, headspace solid-phase microextraction (HS-SPME) followed by gas chromatography–mass spectrometry (GC–qMS), was evaluated as a reliable and improved alternative to the commonly used liquid–liquid extraction (LLE) technique for the establishment of the pattern of hydrolytically released components of 7 Vitis vinifera L. grape varieties, commonly used to produce the world-famous Madeira wine. Since there is no data available on their glycosidic fractions, at a first step, two hydrolyse procedures, acid and enzymatic, were carried out using Boal grapes as matrix. Several parameters susceptible of influencing the hydrolytic process were studied. The best results, expressed as GC peak area, number of identified components and reproducibility, were obtained using ProZym M with b-glucosidase activity at 35 °C for 42 h. For the extraction of hydrolytically released components, HS-SPME technique was evaluated as a reliable and improved alternative to the conventional extraction technique, LLE (ethyl acetate). HS-SPME using DVB/CAR/PDMS as coating fiber displayed an extraction capacity two fold higher than LLE (ethyl acetate). The hydrolyzed fraction was mainly characterized by the occurrence of aliphatic and aromatic alcohols, followed by acids, esters, carbonyl compounds, terpenoids, and volatile phenols. Concerning to terpenoids its contribution to the total hydrolyzed fraction is highest for Malvasia Cândida (23%) and Malvasia Roxa (13%), and their presence according previous studies, even at low concentration, is important from a sensorial point of view (can impart floral notes to the wines), due to their low odor threshold (μg/L). According to the obtained data by principal component analysis (PCA), the sensorial properties of Madeira wines produced by Malvasia Cândida and Malvasia Roxa could be improved by hydrolysis procedure, since their hydrolyzed fraction is mainly characterized by terpenoids (e.g. linalool, geraniol) which are responsible for floral notes. Bual and Sercial grapes are characterized by aromatic alcohols (e.g. benzyl alcohol, 2-phenylethyl alcohol), so an improvement in sensorial characteristics (citrus, sweet and floral odors) of the corresponding wines, as result of hydrolytic process, is expected.