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

JCML: A specification language for the runtime verification of Java Card programs

COSTA, Umberto Souza; MOREIRA, Anamaria Martins; MUSICANTE, Matin A.; SOUZA NETO, Plácido A. JCML: A specification language for the runtime verification of Java Card programs. Science of Computer Programming. [S.l]: [s.n], 2010.

Specification and Runtime Verification of Java Card Programs

COSTA, Umberto Souza da; MOREIRA, Anamaria Martins; MUSICANTE, Martin A. Specification and Runtime Verification of Java Card Programs. Electronic Notes in Theoretical Computer Science. [S.l:s.n], 2009.

The use of software Mapavox for teaching graphics and games to blind and low vision students: a development through practices

Current policies on education to visually impaired point for a growing trend of including students with special educational needs in regular schools. However, most often this inclusion is not accompanied by an appropriate professional trained or infrastructure, which has been presented as a big problem for regular school teachers who have students with visual impairments in their classroom. Based on this situation, the Group of Extension in Tactile Cartography from UNESP - University of the State of São Paulo - Campus de Rio Claro - SP - Brazil has been developing educational material of geography and cartography to blind students at a special school. Among the materials developed in this study highlight the development of graphics and board games provided with sound capabilities through MAPAVOX, software developed in partnership with UFRJ - Federal University from Rio de Janeiro - RJ - Brazil. Through this software, sound capabilities can be inserted into built materials, giving them a multi-sensory character. In most cases the necessary conditions for building specific materials to students with visual impairments is expensive and beyond the reach of features from a regular school, so the survey sought to use easy access and low cost materials like Cork, leaf aluminum, material for fixing and others. The development of these materials was supported by preparation in laboratory and its subsequent test through practices involving blind students. The methodology used on the survey is based on qualitative research and non comparative analysis of the results. In other words, the material is built based on the special students perception and reality construction, not being mere adaptations of visual materials, but a construction focused on the reality of the visually impaired. The results proved were quite successful as the materials prepared were effective on mediating the learning process of students with disabilities. Geographical and cartographic concepts were seized by the students through the technology used, associated with the use of materials that took into account in its building process the perception of the students.

e-Pontos: Uma solução embarcada de automação comercial aplicada a clubes de fidelidade baseado em tecnologia RFID e esmart card

In practically all vertical markets and in every region of the planet, loyalty marketers have adopted the tactic of recognition and reward to identify, maintain and increase the yield of their customers. Several strategies have been adopted by companies, and the most popular among them is the loyalty program, which displays a loyalty club to manage these rewards. But the problem with loyalty programs is that customer identification and transfer of loyalty points are made in a semiautomatic. Aiming at this, this paper presents a master's embedded business automation solution called e-Points. The goal of e-Points is munir clubs allegiances with fully automated tooling technology to identify customers directly at the point of sales, ensuring greater control over the loyalty of associate members. For this, we developed a hardware platform with embedded system and RFID technology to be used in PCs tenant, a smart card to accumulate points with every purchase and a web server, which will provide services of interest to retailers and customers membership to the club

Brazilian Students and Working Capital: An Analysis of Their Decisions When Using Virtual Market Business Games

This study aims to demonstrate that data from business games can be an important resource for improving efficiency and effectiveness of learning. The proposal presented here was developed from preliminary studies of data from Virtual Market games that pointed the possibility of identifying gaps in learning by analyzing the decisions of students. This proposal helps students to refine their learning processes and equips tutors with strategies for teaching and student assessment. The proposal also complements the group discussion and/or debriefing, which are widely used to enhance learning mediated by games. However, from a management perspective the model has the potential to be erroneous and miss opportunities, which cannot be detected because of the dependence on the characteristics of the individual, such as ability to communicate and work together. To illustrate the proposed technique, data sets from two business games were analyzed with the focus on managing working capital and it was found that students had difficulties managing this task. Similar trends were observed in all categories of students in the study-undergraduate, postgraduate and specialization. This discovery led us to the analysis of data for decisions made in the performance of the games, and it was determined that indicators could be developed that were capable of indentifying inconsistencies in the decisions. It was decided to apply some basic concepts of the finance management, such as management of the operational and non-operational expenditures, as well as production management concepts, such as the use of the production capacity. By analyzing the data from the Virtual Market games using the indicator concept, it was possible to detect the lack of domain knowledge of the students. Therefore, these indicators can be used to analyze the decisions of the players and guide them during the game, increasing their effectiveness and efficiency. As these indicators were developed from specific content, they can also be used to develop teaching materials to support learning. Viewed in this light, the proposal adds new possibilities for using business games in learning. In addition to the intrinsic learning that is achieved through playing the games, they also assist in driving the learning process. This study considers the applications and the methodology used.

JCML - Java Card Modeling Language: Definição e Implementação

Formal methods should be used to specify and verify on-card software in Java Card applications. Furthermore, Java Card programming style requires runtime verification of all input conditions for all on-card methods, where the main goal is to preserve the data in the card. Design by contract, and in particular, the JML language, are an option for this kind of development and verification, as runtime verification is part of the Design by contract method implemented by JML. However, JML and its currently available tools for runtime verification were not designed with Java Card limitations in mind and are not Java Card compliant. In this thesis, we analyze how much of this situation is really intrinsic of Java Card limitations and how much is just a matter of a complete re-design of JML and its tools. We propose the requirements for a new language which is Java Card compliant and indicate the lines on which a compiler for this language should be built. JCML strips from JML non-Java Card aspects such as concurrency and unsupported types. This would not be enough, however, without a great effort in optimization of the verification code generated by its compiler, as this verification code must run on the card. The JCML compiler, although being much more restricted than the one for JML, is able to generate Java Card compliant verification code for some lightweight specifications. As conclusion, we present a Java Card compliant variant of JML, JCML (Java Card Modeling Language), with a preliminary version of its compiler

BSmart: desenvolvimento rigoroso de aplicações Java Card com base no método formal B

Java Card technology allows the development and execution of small applications embedded in smart cards. A Java Card application is composed of an external card client and of an application in the card that implements the services available to the client by means of an Application Programming Interface (API). Usually, these applications manipulate and store important information, such as cash and confidential data of their owners. Thus, it is necessary to adopt rigor on developing a smart card application to improve its quality and trustworthiness. The use of formal methods on the development of these applications is a way to reach these quality requirements. The B method is one of the many formal methods for system specification. The development in B starts with the functional specification of the system, continues with the application of some optional refinements to the specification and, from the last level of refinement, it is possible to generate code for some programming language. The B formalism has a good tool support and its application to Java Card is adequate since the specification and development of APIs is one of the major applications of B. The BSmart method proposed here aims to promote the rigorous development of Java Card applications up to the generation of its code, based on the refinement of its formal specification described in the B notation. This development is supported by the BSmart tool, that is composed of some programs that automate each stage of the method; and by a library of B modules and Java Card classes that model primitive types, essential Java Card API classes and reusable data structures

KitSmart: Uma biblioteca de componentes para o desenvolvimento rigoroso de aplicações Java Card com o método B

The development of smart card applications requires a high level of reliability. Formal methods provide means for this reliability to be achieved. The BSmart method and tool contribute to the development of smart card applications with the support of the B method, generating Java Card code from B specifications. For the development with BSmart to be effectively rigorous without overloading the user it is important to have a library of reusable components built in B. The goal of KitSmart is to provide this support. A first research about the composition of this library was a graduation work from Universidade Federal do Rio Grande do Norte, made by Thiago Dutra in 2006. This first version of the kit resulted in a specification of Java Card primitive types byte, short and boolean in B and the creation of reusable components for application development. This work provides an improvement of KitSmart with the addition of API Java Card specification made in B and a guide for the creation of new components. The API Java Card in B, besides being available to be used for development of applications, is also useful as a documentation of each API class. The reusable components correspond to modules to manipulate specific structures, such as date and time. These structures are not available for B or Java Card. These components for Java Card are generated from specifications formally verified in B. The guide contains quick reference on how to specify some structures and how some situations were adapted from object-orientation to the B Method. This work was evaluated through a case study made through the BSmart tool, that makes use of the KitSmart library. In this case study, it is possible to see the contribution of the components in a B specification. This kit should be useful for B method users and Java Card application developers

Educative games and expositive lesson: Comparison of educational techniques on sitting posture

Introduction: Studies on education in health are important for the concretion of action of promotion of the health. Objective: To verify the changes of theoretical knowledge on sitting posture, evaluated at two moments (initial and final,) considering two programs of education (expositive lesson and operative groups). Methods: 75 pupils had been citizens, of both the sexes, three 4as series of a public school, evaluated previously (A1) on seated position; group 1 was submitted to a procedure of expositive education, the 2 educative games in the 2 and, the 3 to no intervention. After one week they had been reevaluated (A2). For the moments the test of Wilcoxon was applied and between the Kruskal groups Wallis. Results: In the comparison inside of the groups, of 2 and 3 they had presented increase in the number of rightness on position seated in the after-test, with statistical significant difference, whereas in the group has controlled, such fact did not occur. In the comparison between groups, at the first moment (A1), 2 groups e 3 had not presented significant difference statistical (p > 0,05), however, in as moment notices that it had difference statistics between the three groups (p < 0,01), being that the G3 presented minor frequency of errors (md = 5) in relation to the g2 (md = 8) and g1 (md = 10). Conclusions: It can be affirmed that educative techniques that supply information and promote debates and exchanges of experiences between the participants increase the possibilities of incorporation of the contents related to the sitting posture.

Bibliographic record card of CARISPLAN

Includes bibliography