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.

What children learn from adults’ utterances: an ephemeral lexical boost and persistent syntactic priming in adult–child dialogue

We show that children’s syntactic production is immediately affected by individual experiences of structures and verb–structure pairings within a dialogue, but that these effects have different timecourses. In a picture-matching game, three- to four-year-olds were more likely to describe a transitive action using a passive immediately after hearing the experimenter produce a passive than an active (abstract priming), and this tendency was stronger when the verb was repeated (lexical boost). The lexical boost disappeared after two intervening utterances, but the abstract priming effect persisted. This pattern did not differ significantly from control adults. Children also showed a cumulative priming effect. Our results suggest that whereas the same mechanism may underlie children’s immediate syntactic priming and long-term syntactic learning, different mechanisms underlie the lexical boost versus long-term learning of verb–structure links. They also suggest broad continuity of syntactic processing in production between this age group and adults.

Memory retrieval as temporal discrimination

Temporal distinctiveness models of memory retrieval claim that memories are organised partly in terms of their positions along a temporal dimension, and suggest that memory retrieval involves temporal discrimination. According to such models the retrievability of memories should be related to the discriminability of their temporal distances at the time of retrieval. This prediction is tested directly in three pairs of experiments that examine (a) memory retrieval and (b) identification of temporal durations that correspond to the temporal distances of the memories. Qualitative similarities between memory retrieval and temporal discrimination are found in probed serial recall (Experiments 1 and 2), immediate and delayed free recall (Experiments 3 and 4) and probed serial recall of grouped lists (Experiments 5 and 6). The results are interpreted as consistent with the suggestion that memory retrieval is indeed akin to temporal discrimination. (C) 2008 Elsevier Inc. All rights reserved.

The Sacred and the Obscure: Greek in the Carolingian Reception of Martianus Capella

Carolingian scholars paid considerable attention to the Greek found in Martianus Capella’s De nuptiis Philologiae et Mercurii, a late antique Latin work full of obscurities in language and imagery. This article, focusing on glosses on De nuptiis from the oldest gloss tradition, demonstrates that a range of material was available to ninth-century scholars to elucidate Martianus’s Greek and that Greek seems, at times, to have served as a means to obscure. I argue that their interest in obscurity reflects a widespread epistemology and strategy of concealment, hence their intellectual investment in Martianus. For ninth-century readers, then, the Greek in the glossed Martianus manuscripts, however decorative it may have been, also operated at the core of medieval hermeneutics.

Variable binding and coreference in sentence comprehension: evidence from eye movements

The hypothesis that pronouns can be resolved via either the syntax or the discourse representation has played an important role in linguistic accounts of pronoun interpretation (e.g. Grodzinsky & Reinhart, 1993). We report the results of an eye-movement monitoring study investigating the relative timing of syntactically-mediated variable binding and discourse-based coreference assignment during pronoun resolution. We examined whether ambiguous pronouns are preferentially resolved via either the variable binding or coreference route, and in particular tested the hypothesis that variable binding should always be computed before coreference assignment. Participants’ eye movements were monitored while they read sentences containing a pronoun and two potential antecedents, a c-commanding quantified noun phrase and a non c-commanding proper name. Gender congruence between the pronoun and either of the two potential antecedents was manipulated as an experimental diagnostic for dependency formation. In two experiments, we found that participants’ reading times were reliably longer when the linearly closest antecedent mismatched in gender with the pronoun. These findings fail to support the hypothesis that variable binding is computed before coreference assignment, and instead suggest that antecedent recency plays an important role in affecting the extent to which a variable binding antecedent is considered. We discuss these results in relation to models of memory retrieval during sentence comprehension, and interpret the antecedent recency preference as an example of forgetting over time.

Coargumenthood and the processing of reflexives

We report three eye-movement experiments and an antecedent choice task investigating the interpretation of reflexives in different syntactic contexts. This included contexts in which the reflexive and a local antecedent were coarguments of the same verbal predicate (John heard that the soldier had injured himself), and also so-called picture noun phrases, either with a possessor (John heard about the soldier’s picture of himself) or without (John heard that the soldier had a picture of himself). While results from the antecedent choice task indicated that comprehenders would choose a nonlocal antecedent (‘John’ above) for reflexives in either type of picture noun phrase, the eye-movement experiments suggested that participants preferred to initially interpret the reflexive in each context as referring to the local antecedent (‘the soldier’), as indexed by longer reading times when it mismatched in gender with the reflexive. We also observed a difference in the time-course of this effect. While it was observed during first-pass processing at the reflexive for coargument reflexives and those in picture noun phrases with a possessor, it was comparatively delayed for reflexives in possessorless picture noun phrases. These results suggest that locality constraints are more strongly weighted cues to retrieval than gender agreement for both coargument reflexives and those inside picture noun phrases. We interpret the observed time-course differences as indexing the relative ease of accessing the local antecedent in different syntactic contexts.

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.

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

Contribuições para verificação automática de applets javacard

The widespread growth in the use of smart cards (by banks, transport services, and cell phones, etc) has brought an important fact that must be addressed: the need of tools that can be used to verify such cards, so to guarantee the correctness of their software. As the vast majority of cards that are being developed nowadays use the JavaCard technology as they software layer, the use of the Java Modeling Language (JML) to specify their programs appear as a natural solution. JML is a formal language tailored to Java. It has been inspired by methodologies from Larch and Eiffel, and has been widely adopted as the de facto language when dealing with specification of any Java related program. Various tools that make use of JML have already been developed, covering a wide range of functionalities, such as run time and static checking. But the tools existent so far for static checking are not fully automated, and, those that are, do not offer an adequate level of soundness and completeness. Our objective is to contribute to a series of techniques, that can be used to accomplish a fully automated and confident verification of JavaCard applets. In this work we present the first steps to this. With the use of a software platform comprised by Krakatoa, Why and haRVey, we developed a set of techniques to reduce the size of the theory necessary to verify the specifications. Such techniques have yielded very good results, with gains of almost 100% in all tested cases, and has proved as a valuable technique to be used, not only in this, but in most real world problems related to automatic verification

Estudios corológicos de plantas vasculares en la cuenca media del Tajo

Se ha realizado un estudio de la distribución de plantas vasculares en un territorio situado entre las provincias de Cuenca, Guadalajara, Madrid y Toledo (España). El territorio estudiado está en la Submeseta Sur de la península ibérica, al sur del Sistema Central, norte de los Montes de Toledo y oeste del Sistema Ibérico, en zonas sedimentarias con poco relieve y clima mediterráneo, con grandes contrastes de temperatura y precipitaciones muy irregulares. Coincide con las regiones naturales llamadas: “Alcarrias”, “Campiñas de Madrid y Guadalajara” y “Vegas de los ríos de la Cuenca del Tajo”. Es lo que he llamado Cuenca Media del Tajo. En una primera fase se ha estudiado la flora regional para adquirir conocimientos previos mediante las consultas bibliográficas y de herbarios, se ha contado con bases de datos disponibles para MA, MACB, MAF, JACA, AH, ABH, VAL, SALA y EMMA. Se han revisado las aportaciones propias que en los últimos años he realizado en el territorio en relación a los temas tratados en la tesis. El trabajo de campo ha consistido en la realización de inventarios de presencia de flora. Ha sido muy importante la tarea herborizadora para llegar a la correcta identificación de las especies colectadas en los inventarios. De esta forma el autor ha confeccionado un herbario propio JML que en el territorio muestreado ha reunido cerca de 15000 números en las cuatro provincias estudiadas. Se ha hecho un muestreo sistemático del territorio con unos 6000 listados de plantas. Se ha tomado como unidad de muestreo la cuadrícula de UTM de 1 km de lado incluida como una centésima parte de la cuadrícula de UTM de 10 km. Se han seguido criterios para uniformizar el muestreo. Se ha apuntado el tiempo empleado y la superficie muestreada estimada en cada toma de datos. El criterio mínimo que tienen que cumplir todas las cuadrículas en el área estudiada ha sido que para cada cuadrícula de UTM de 5 km se han realizado al menos 5 inventarios en 5 cuadrículas diferentes de UTM de 1 km y al menos en una hora de tiempo. La unidad de comparación ha sido la cuadrícula UTM de 5 km. Se han informatizado los inventarios de campo, para ello se ha creado la base de datos TESIS en Microsoft office –Access-. Las principales tablas son LOCALIDAD, en la que se anotan las características del lugar muestreado y ESPECIES, que lista las especies de flora consideradas en las cuatro provincias del estudio. Por medio de formularios se han rellenado las tablas; destaca la tabla ESPECIE INVENTARIO que relaciona las tablas ESPECIES y LOCALIDAD; esta tabla cuenta en este momento con unos 165.000 registros. En la tabla ESPECIES_FPVI se visualizan las especies recopiladas. Se ha creado un indicador llamado FPVI “Flora permanentemente visible identificable” que consiste en atribuir a cada especie unos índices que nos permiten saber si una determinada planta se puede detectar en cualquier época del año. Los resultados presentados son: Creación de la base de datos TESIS. El Catálogo Florístico de la Cuenca Media del Tajo, que es el catálogo de la flora de las cuatro provincias desde el principio de la sistemática hasta las Saxifragáceas. En total se han recopilado 1028 taxones distribuidos en 77 familias. Se ha calculado el índice FPVI, para las especies del catálogo. La finalidad para la que se ha diseñado este índice es para poder comparar territorios. Para el desarrollo de ambos resultados ha sido fundamental el desarrollo de la tabla ESPECIES_PVI de la base de datos TESIS. En la tabla ESPECIES_PVI se han apuntado las características ecológicas y se revisa la información bibliográfica disponible para cada especie; las principales fuentes de información consultadas han sido Flora iberica, el proyecto “Anthos” y las bases de datos de los herbarios. Se ha apuntado sí se ha visto, sí está protegida o sí en un endemismo. Otros resultados son: la localización de las cuadrículas de UTM de 10 km, con mayor número de endemismos o especies singulares, con mayor valor botánico. Se ha realizado un par de ejemplos de estudios de autoecología de especie, en concreto Teucrium pumilum y Clematis recta. Se han confeccionando salidas cartográficas de distribución de especies. Se ha elaborado el herbario JML. Se ha presentado una sencilla herramienta para incluir inventarios florísticos, citas corológicas, consultas de autoecología o etiquetado de pliegos de herbario. Como colofón, se ha colaborado para desarrollar una aplicación informática de visualización, análisis y estudio de la distribución de taxones vegetales, que ha utilizado como datos de partida un porcentaje importante de los obtenidos para esta tesis. ABSTRACT I have made a study of the distribution of vascular plants in a territory located between the provinces of Cuenca, Guadalajara, Madrid and Toledo (Spain). The studied area is in the “Submeseta” South of the Iberian Peninsula, south of the Central System, north of the Montes de Toledo and west of the Iberian System, in sedimentary areas with little relief and Mediterranean climate, with big temperature contrasts and irregular rainfall. Coincides with the natural regions called "Alcarrias", "countryside of Madrid and Guadalajara" and “Vegas River Tagus Basin”. This is what I have called Middle Tagus Basin. In a first step we have studied the regional flora to acquire prior knowledge through the literature and herbaria consultations, it has had available databases for MA, MACB, MAF, JACA, AH, ABH, VAL, SALA and EMMA herbaria. The contributions I have made in the last years in the territory in relation to the topics discussed in the thesis have been revised. The field work consisted of conducting inventories presence of flora. Botanize was a very important task to get to the correct identification of the species collected in inventories. In this way the author has made his own herbarium JML in the sampled area has met at least 15000 samples in the four studied provinces. There has been a systematic sampling of the territory with nearly 6,000 listings of plants. Was taken as the sampling unit grid UTM 1 km side included as a hundredth of the UTM grid of 10 km from side. Criteria have been taken to standardize the sampling. Data were taken of the time spent and the estimated sampled surface. The minimum criteria they have to meet all the grids in the study area has been that for each UTM grid of 5 km have been made at least 5 stocks in 5 different grids UTM 1 km and at least one hour of time. The unit of comparison was the UTM grid of 5 km. I have computerized inventories of field, for it was created a database in Access- Microsoft office -TESIS. The main tables are LOCALIDAD, with caracteristics of the sampled location and ESPECIES, which lists the plant species considered in the four provinces of the study, is. Through forms I filled in the tables; highlights ESPECIE INVENTARIO table that relates the tables ESPECIES and LOCALIDAD, this table is counted at the moment with about 165,000 records. The table ESPECIES FPVI visualizes all recollected species. We have created an indicator called FPVI "Flora permanently visible identifiable" that attributes to each species indices that allow us to know whether a given plant can be detected in any season. The results presented are: Creating data base TESIS. The Floristic Books Middle Tagus Basin, which is a catalog of the flora of the four provinces since the beginning of the systematic until Saxifragaceae. In total 1028 collected taxa in 77 families. We calculated FPVI index for species catalog. The purpose for which this index designed is, to compare territories. For the development of both results, it was essential to develop the table ESPECIES_PVI TESIS data base. Table ESPECIES_PVI has signed the ecological characteristics and bibliographic information available for each species is revised; the main sources of information has been Flora iberica, the Anthos project databases of herbaria. Targeted species has been recorded, when seen, protected or endemism. Have also been located UTM grids of 10 km, with the largest number of endemic or unique species and more botanical value. There have been a couple of species autecology studies, namely Teucrium pumilum and Clematis recta, as an example of this type of study. They have been putting together maps of species distribution. We made herbarium JML. I have presented a simple tool to include floristic inventories, chorological appointments, consultations or to tag autoecology herbarium specimens. To cap it has worked to develop a computer application for visualization, analysis and study of the distribution of plant taxa, which has used as input data a significant percentage of those obtained for this thesis.