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

Analysis an development of a prototype based on media wiki and semantic media wiki integrated with a design modeling that allows modeling of organizations based on demo

In a world where organizations are ever more complex the need for the knowledge of the organizational self is a growing necessity. The DEMO methodology sets a goal in achieving the specification of the organizational self capturing the essence of the organization in way independent of its implementation and also coherent, consistent, complete, modular and objective. But having such organization self notion is of little meaning if this notion is not shared by the organization actors. To achieve this goal in a society that has grown attached to technology and where time is of utmost importance, using a tool such as a semantic Wikipedia may be the perfect way of making the information accessible. However, to establish DEMO methodology in such platform there is a need to create bridges between its modeling components and semantic Wikipedia. It’s in that aspect that our thesis focuses, trying to establish and implement, using a study case, the principles of a way of transforming the DEMO methodology diagrams in comprehensive pages on semantic Wikipedia but keeping them as abstract as possible to allow expansibility and generalization to all diagrams without losing any valuable information so that, if that is the wish, those diagrams may be recreated from the semantic pages and make this process a full cycle.

Development of a novel microextraction by packed sorbent-based approach followed by ultrahigh pressure liquid chromatography as a powerful technique for quantification phenolic constituents of biological interest in wines

A novel analytical approach, based on a miniaturized extraction technique, the microextraction by packed sorbent (MEPS), followed by ultrahigh pressure liquid chromatography (UHPLC) separation combined with a photodiode array (PDA) detection, has been developed and validated for the quantitative determination of sixteen biologically active phenolic constituents of wine. In addition to performing routine experiments to establish the validity of the assay to internationally accepted criteria (linearity, sensitivity, selectivity, precision, accuracy), experiments are included to assess the effect of the important experimental parameters on the MEPS performance such as the type of sorbent material (C2, C8, C18, SIL, and M1), number of extraction cycles (extract-discard), elution volume, sample volume, and ethanol content, were studied. The optimal conditions of MEPS extraction were obtained using C8 sorbent and small sample volumes (250 μL) in five extraction cycle and in a short time period (about 5 min for the entire sample preparation step). The wine bioactive phenolics were eluted by 250 μL of the mixture containing 95% methanol and 5% water, and the separation was carried out on a HSS T3 analytical column (100 mm × 2.1 mm, 1.8 μm particle size) using a binary mobile phase composed of aqueous 0.1% formic acid (eluent A) and methanol (eluent B) in the gradient elution mode (10 min of total analysis). The method gave satisfactory results in terms of linearity with r2-values > 0.9986 within the established concentration range. The LOD varied from 85 ng mL−1 (ferulic acid) to 0.32 μg mL−1 ((+)-catechin), whereas the LOQ values from 0.028 μg mL−1 (ferulic acid) to 1.08 μg mL−1 ((+)-catechin). Typical recoveries ranged between 81.1 and 99.6% for red wines and between 77.1 and 99.3% for white wines, with relative standard deviations (RSD) no larger than 10%. The extraction yields of the MEPSC8/UHPLC–PDA methodology were found between 78.1 (syringic acid) and 99.6% (o-coumaric acid) for red wines and between 76.2 and 99.1% for white wines. The inter-day precision, expressed as the relative standard deviation (RSD%), varied between 0.2% (p-coumaric and o-coumaric acids) and 7.5% (gentisic acid) while the intra-day precision between 0.2% (o-coumaric and cinnamic acids) and 4.7% (gallic acid and (−)-epicatechin). On the basis of analytical validation, it is shown that the MEPSC8/UHPLC–PDA methodology proves to be an improved, reliable, and ultra-fast approach for wine bioactive phenolics analysis, because of its capability for determining simultaneously in a single chromatographic run several bioactive metabolites with high sensitivity, selectivity and resolving power within only 10 min. Preliminary studies have been carried out on 34 real whole wine samples, in order to assess the performance of the described procedure. The new approach offers decreased sample preparation and analysis time, and moreover is cheaper, more environmentally friendly and easier to perform as compared to traditional methodologies.