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

Teamwork in academia: an empirical study

The Bologna Process introduced some changes in the curriculum of higher education institutions (HEIs) and defined that academic learning should consider the needs of the labour market. HEIs and employers agree that personal skills are the most important set of competence of graduates (Pavlin, Akkuyunlu, Kovacic, & Svetlik, 2009). The goals of this work were to explore how the work experienced by teams of students in HEIs might help them improve their personal skills, namely empirically explore the perception of teamwork and personality into two groups of students. The study was based on the theoretical model of Team Evolution and Maturation (TEAM, Fransen, 2012). The sample consisted of 99 students of the 3rd year of the degree (1st cycle) in Computer Science (49 students) and the 2nd year of the Bachelor's Degree (1st cycle) in Psychology (50 students), from the University of Madeira, Portugal. Areas of personality and team collaboration were evaluated with a Pre- and Post-test. Findings show that the perception of the teamwork collaboration of students in Computer Science and Psychology majors seems to be influenced by their scientific area, by gender, by the selection method of the time-organiser, the self-perceived personality of the time-organiser, the self perceived personality of the non-time-organiser, and the size of the team. It is expected that this data will contribute to further theoretical and practical reflection on the teamwork among college students and their performance in the labour market.