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.

Atribuição de turmas para professores via Beam Search em Java

In the universities, before the start of each school year, is held the distribution of classes among available teachers. Therefore, it is necessary to consider the maximum workweek for each teacher and their preferences for each discipline, to prevent a teacher to give lessons in two separate locations at the same time and to avoid some teachers to become overloaded while others with large clearance. This process, manually performed, is time consuming and does not allow the visualization of other combinations of assignment of teachers to classes, besides being liable to error. This work aims to develop a decision support tool for the problem of assigning teachers to classes in college. The project encompasses the development of a computer program using the concepts of object orientation and a tree search algorithm of a combinatorial nature called Beam Search. The programming language used is Java and the program has a graphical interface for entering and manipulating data of the problem. Once obtained the schedule data of classes and teachers is possible, by means of the tool, perform various simulations and manual adjustments to achieve the final result. It is an efficient method of class scheduling, considering the speed of task execution and the fact that it generates only feasible results

UML approach to the generation of test sequences for Java-based concurrent systems

Starting with a UML specification that captures the underlying functionality of some given Java-based concurrent system, we describe a systematic way to construct, from this specification, test sequences for validating an implementation of the system. The approach is to first extend the specification to create UML state machines that directly address those aspects of the system we wish to test. To be specific, the extended UML state machines can capture state information about the number of waiting threads or the number of threads blocked on a given object. Using the SAL model checker we can generate from the extended UML state machines sequences that cover all the various possibilities of events and states. These sequences can then be directly transformed into test sequences suitable for input into a testing tool such as ConAn. As an illustration, the methodology is applied to generate sequences for testing a Java implementation of the producer-consumer system. © 2005 IEEE

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.

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.

An Interactive Theorem Prover for First-Order Dynamic Logic

Dynamic logic is an extension of modal logic originally intended for reasoning about computer programs. The method of proving correctness of properties of a computer program using the well-known Hoare Logic can be implemented by utilizing the robustness of dynamic logic. For a very broad range of languages and applications in program veri cation, a theorem prover named KIV (Karlsruhe Interactive Veri er) Theorem Prover has already been developed. But a high degree of automation and its complexity make it di cult to use it for educational purposes. My research work is motivated towards the design and implementation of a similar interactive theorem prover with educational use as its main design criteria. As the key purpose of this system is to serve as an educational tool, it is a self-explanatory system that explains every step of creating a derivation, i.e., proving a theorem. This deductive system is implemented in the platform-independent programming language Java. In addition, a very popular combination of a lexical analyzer generator, JFlex, and the parser generator BYacc/J for parsing formulas and programs has been used.

Parallel and distributed computing with Java

The Java language first came to public attention in 1995. Within a year, it was being speculated that Java may be a good language for parallel and distributed computing. Its core features, including being objected oriented and platform independence, as well as having built-in network support and threads, has encouraged this view. Today, Java is being used in almost every type of computer-based system, ranging from sensor networks to high performance computing platforms, and from enterprise applications through to complex research-based.simulations. In this paper the key features that make Java a good language for parallel and distributed computing are first discussed. Two Java-based middleware systems, namely MPJ Express, an MPI-like Java messaging system, and Tycho, a wide-area asynchronous messaging framework with an integrated virtual registry are then discussed. The paper concludes by highlighting the advantages of using Java as middleware to support distributed applications.

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.

Desenvolvimento de um aplicativo para processamento de imagens obtidas por fotografias aéreas

Pós-graduação em Agronomia (Energia na Agricultura) - FCA

Desenvolvimento de um aplicativo para processamento de imagens obtidas por fotografias aéreas

Pós-graduação em Agronomia (Energia na Agricultura) - FCA

Content and English Language Integrated Learning: The use of Moodle in Aircraft Maintenance Training Programs

The aim of this work is to develop a prototype of an e-learning environment that can foster Content and Language Integrated Learning (CLIL) for students enrolled in an aircraft maintenance training program, which allows them to obtain a license valid in all EU member states. Background research is conducted to retrace the evolution of the field of educational technology, analyzing different learning theories – behaviorism, cognitivism, and (socio-)constructivism – and reflecting on how technology and its use in educational contexts has changed over time. Particular attention is given to technologies that have been used and proved effective in Computer Assisted Language Learning (CALL). Based on the background research and on students’ learning objectives, i.e. learning highly specialized contents and aeronautical technical English, a bilingual approach is chosen, three main tools are identified – a hypertextbook, an exercise creation activity, and a discussion forum – and the learning management system Moodle is chosen as delivery medium. The hypertextbook is based on the technical textbook written in English students already use. In order to foster text comprehension, the hypertextbook is enriched by hyperlinks and tooltips. Hyperlinks redirect students to webpages containing additional information both in English and in Italian, while tooltips show Italian equivalents of English technical terms. The exercise creation activity and the discussion forum foster interaction and collaboration among students, according to socio-constructivist principles. In the exercise creation activity, students collaboratively create a workbook, which allow them to deeply analyze and master the contents of the hypertextbook and at the same time create a learning tool that can help them, as well as future students, to enhance learning. In the discussion forum students can discuss their individual issues, content-related, English-related or e-learning environment-related, helping one other and offering instructors suggestions on how to improve both the hypertextbook and the workbook based on their needs.

User-definable resource usage bounds analysis for java bytecode

Automatic cost analysis of programs has been traditionally concentrated on a reduced number of resources such as execution steps, time, or memory. However, the increasing relevance of analysis applications such as static debugging and/or certiflcation of user-level properties (including for mobile code) makes it interesting to develop analyses for resource notions that are actually application-dependent. This may include, for example, bytes sent or received by an application, number of files left open, number of SMSs sent or received, number of accesses to a datábase, money spent, energy consumption, etc. We present a fully automated analysis for inferring upper bounds on the usage that a Java bytecode program makes of a set of application programmer-deflnable resources. In our context, a resource is defined by programmer-provided annotations which state the basic consumption that certain program elements make of that resource. From these deflnitions our analysis derives functions which return an upper bound on the usage that the whole program (and individual blocks) make of that resource for any given set of input data sizes. The analysis proposed is independent of the particular resource. We also present some experimental results from a prototype implementation of the approach covering a signiflcant set of interesting resources.

Análisis del software ImageJ para el análisis científico de imágenes

ImageJ es un programa informático de tratamiento digital de imagen orientado principalmente hacia el ámbito de las ciencias de la salud. Se trata de un software de dominio público y de código abierto desarrollado en lenguaje Java en las instituciones del National Institutes of Health de Estados Unidos. Incluye por defecto potentes herramientas para editar, procesar y analizar imágenes de casi cualquier tipo y formato. Sin embargo, su mayor virtud reside en su extensibilidad: las funcionalidades de ImageJ pueden ampliarse hasta resolver casi cualquier problema de tratamiento digital de imagen mediante macros, scripts y, especialmente, plugins programables en lenguaje Java gracias a la API que ofrece. Además, ImageJ cuenta con repositorios oficiales en los que es posible obtener de forma gratuita macros, scripts y plugins aplicables en multitud de entornos gracias a la labor de la extensa comunidad de desarrolladores de ImageJ, que los depura, mejora y amplia frecuentemente. Este documento es la memoria de un proyecto que consiste en el análisis detallado de las herramientas de tratamiento digital de imagen que ofrece ImageJ. Tiene por objetivo determinar si ImageJ, a pesar de estar más enfocado a las ciencias de la salud, puede resultar útil en el entorno de la Escuela Técnica Superior de Ingeniería y Sistemas de Telecomunicación de la Universidad Politécnica de Madrid, y en tal caso, resaltar las características que pudieran resultar más beneficiosas en este ámbito y servir además como guía introductoria. En las siguientes páginas se examinan una a una las herramientas de ImageJ (versión 1.48q), su funcionamiento y los mecanismos subyacentes. Se sigue el orden marcado por los menús de la interfaz de usuario: el primer capítulo abarca las herramientas destinadas a la manipulación de imágenes en general (menú Image); el segundo, las herramientas de procesado (menú Process); el tercero, las herramientas de análisis (menú Analyze); y el cuarto y último, las herramientas relacionadas con la extensibilidad de ImageJ (menú Plugins). ABSTRACT. ImageJ is a digital image processing computer program which is mainly focused at the health sciences field. It is a public domain, open source software developed in Java language at the National Institutes of Health of the United States of America. It includes powerful built-in tools to edit, process and analyze almost every type of image in nearly every format. However, its main virtue is its extensibility: ImageJ functionalities can be widened to solve nearly every situation found in digital image processing through macros, scripts and, specially, plugins programmed in Java language thanks to the ImageJ API. In addition, ImageJ has official repositories where it is possible to freely get many different macros, scripts and plugins thanks to the work carried out by the ImageJ developers community, which continuously debug, improve and widen them. This document is a report which explains a detailed analysis of all the digital image processing tools offered by ImageJ. Its final goal is to determine if ImageJ can be useful to the environment of Escuela Tecnica Superior de Ingenierfa y Sistemas de Telecomunicacion of Universidad Politecnica de Madrid, in spite of being focused at the health sciences field. In such a case, it also aims to highlight the characteristics which could be more beneficial in this field, and serve as an introductory guide too. In the following pages, all of the ImageJ tools (version 1.48q) are examined one by one, as well as their work and the underlying mechanics. The document follows the order established by the menus in ImageJ: the first chapter covers all the tools destined to manipulate images in general (menu Image); the second one covers all the processing tools (menu Process); the third one includes analyzing tools (menu Analyze); and finally, the fourth one contains all those tools related to ImageJ extensibility (menu Plugins).

A WEB-System for Computer Experiments in the Field of Program Transformations

The paper presents basic notions and scientific achievements in the field of program transformations, describes usage of these achievements both in the professional activity (when developing optimizing and unparallelizing compilers) and in the higher education. It also analyzes main problems in this area. The concept of control of program transformation information is introduced in the form of specialized knowledge bank on computer program transformations to support the scientific research, education and professional activity in the field. The tasks that are solved by the knowledge bank are formulated. The paper is intended for experts in the artificial intelligence, optimizing compilation, postgraduates and senior students of corresponding specialties; it may be also interesting for university lecturers and instructors.

Two-Language, Two-Paradigm Introductory Computing Curriculum Model and its Implementation

This paper analyzes difficulties with the introduction of object-oriented concepts in introductory computing education and then proposes a two-language, two-paradigm curriculum model that alleviates such difficulties. Our two-language, two-paradigm curriculum model begins with teaching imperative programming using Python programming language, continues with teaching object-oriented computing using Java, and concludes with teaching object-oriented data structures with Java.