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.

A informática como uma ferramenta de apoio a inclusão do deficiente visual

An inclusive environment has its foundations in the belief that all people are entitled to participate, to live as normal a life as possible, without discrimination, especially in education. This is to ensure equal opportunities. For individuals with special needs, the use of computers and digital materials is not an alternative, but one of the only forms of access to information. For the visually impaired, they start from the beginning to enter the university, through the selection processes, not always accessible. For those who can, other difficulties arise, undermining the initial enthusiasm and generating a large rate of dropouts. In most cases, these students will depend on the goodwill of colleagues and volunteers for the reading of texts in the basic literature of the disciplines studied. The high cost of technology assisted allied to a lack of resources and knowledge of curricular adaptations, prevents many teachers help these students in an appropriate manner. This thesis seeks to contribute to the inclusion of the visually impaired student pointing alternatives that can help in caring education. The research was conducted specifically for the doctorate during the period 2001 to 2006, the cities of Natal, Salvador and Curitiba, and is based mainly on the methodology of action research. The objective was the construction of Virtual Teaching Support Center , structured in a Web portal that can serve as a resource to help support teachers, staff and other users concerned with the process of inclusion of people with needs special education, with the goal of assimilation of educational opportunities, with the support of resources and methods. The inclusion is for everyone because we are all different

Aspectos linguístico-ergonômicos em rótulos: avaliação da linguagem verbo-visual de rótulos de embalagens para alimentos achocolatados

We have been living in a world of packed products. The package and the labels support the companies to communicate with the customers in addition to give protection, storage and convenience in proportion to the products that move in the price list. The labels mainly add up a value which helps the companies differ their products and increase the value of the brands among the final customers. However, the information given in the label are not clear sometimes. It displays a verbal-visual defective language resulted from a poor visibility, legibleness and comprehensibleness of the verbal and visual marks. The aim of this research is to verify, according to the costumers‟ view, the level of the clarity in the informative texts, harmony and ergonomic conformity of the package labels in the chocolate powder of the Claralate brand, considering the linguistic aspects presented on the labels. The criteria to evaluate the chocolate package selected were based on the linguistic field: the organization and the structure of the text derided from the classification of the textual genre; the clarity and the comprehension of the language utilized on those labels. From the ergonomic view, the informative and ergonomic conformity, based on the following requirements: legibility, symbols, characters, reading fields and intermission of the written lines. Therefore, the research done july 2007 and added july 2011 had a structured questionnaire in the interview put to the 118 customers of the chocolate package that go shopping in one of the two supermarkets in Floriano, Piauí São Jorge and/or Super Quaresma. The main results of the investigation show that the linguistic aspects in the informative texts of the labels provide the customers‟ expectancy partially, while the consideration of the informative ergonomic analyzed can contribute to the improvement of the information and consequent visual progress of those, on the labels of chocolate package investigated. As recommendation towards the maker of the product, the outcome of the research indicates: harmonize the proportion of the letters and numbers; enlarge the letters size; make the visual information more comprehensive determined by the reading field; put the expiry date in a better visual place

Metodologia para modelagem, validação e programação de controladores lógicos industriais usando statecharts básicos

Due of industrial informatics several attempts have been done to develop notations and semantics, which are used for classifying and describing different kind of system behavior, particularly in the modeling phase. Such attempts provide the infrastructure to resolve some real problems of engineering and construct practical systems that aim at, mainly, to increase the productivity, quality, and security of the process. Despite the many studies that have attempted to develop friendly methods for industrial controller programming, they are still programmed by conventional trial-and-error methods and, in practice, there is little written documentation on these systems. The ideal solution would be to use a computational environment that allows industrial engineers to implement the system using high-level language and that follows international standards. Accordingly, this work proposes a methodology for plant and control modelling of the discrete event systems that include sequential, parallel and timed operations, using a formalism based on Statecharts, denominated Basic Statechart (BSC). The methodology also permits automatic procedures to validate and implement these systems. To validate our methodology, we presented two case studies with typical examples of the manufacturing sector. The first example shows a sequential control for a tagged machine, which is used to illustrated dependences between the devices of the plant. In the second example, we discuss more than one strategy for controlling a manufacturing cell. The model with no control has 72 states (distinct configurations) and, the model with sequential control generated 20 different states, but they only act in 8 distinct configurations. The model with parallel control generated 210 different states, but these 210 configurations act only in 26 distinct configurations, therefore, one strategy control less restrictive than previous. Lastly, we presented one example for highlight the modular characteristic of our methodology, which it is very important to maintenance of applications. In this example, the sensors for identifying pieces in the plant were removed. So, changes in the control model are needed to transmit the information of the input buffer sensor to the others positions of the cell

Seleção de features guiada por atenção visual em imagens com fóvea

Visual attention is a very important task in autonomous robotics, but, because of its complexity, the processing time required is significant. We propose an architecture for feature selection using foveated images that is guided by visual attention tasks and that reduces the processing time required to perform these tasks. Our system can be applied in bottom-up or top-down visual attention. The foveated model determines which scales are to be used on the feature extraction algorithm. The system is able to discard features that are not extremely necessary for the tasks, thus, reducing the processing time. If the fovea is correctly placed, then it is possible to reduce the processing time without compromising the quality of the tasks outputs. The distance of the fovea from the object is also analyzed. If the visual system loses the tracking in top-down attention, basic strategies of fovea placement can be applied. Experiments have shown that it is possible to reduce up to 60% the processing time with this approach. To validate the method, we tested it with the feature algorithm known as Speeded Up Robust Features (SURF), one of the most efficient approaches for feature extraction. With the proposed architecture, we can accomplish real time requirements of robotics vision, mainly to be applied in autonomous robotics

The influence of visual inter-hemispheric connections on spiking, assembly and LFP activities, and their phase relationship during figure-ground stimulation

Desde os descobrimentos pioneiros de Hubel e Wiesel acumulou-se uma vasta literatura descrevendo as respostas neuronais do córtex visual primário (V1) a diferentes estímulos visuais. Estes estímulos consistem principalmente em barras em movimento, pontos ou grades, que são úteis para explorar as respostas dentro do campo receptivo clássico (CRF do inglês classical receptive field) a características básicas dos estímulos visuais como a orientação, direção de movimento, contraste, entre outras. Entretanto, nas últimas duas décadas, tornou-se cada vez mais evidente que a atividade de neurônios em V1 pode ser modulada por estímulos fora do CRF. Desta forma, áreas visuais primárias poderiam estar envolvidas em funções visuais mais complexas como, por exemplo, a separação de um objeto ou figura do seu fundo (segregação figura-fundo) e assume-se que as conexões intrínsecas de longo alcance em V1, assim como as conexões de áreas visuais superiores, estão ativamente envolvidas neste processo. Sua possível função foi inferida a partir da análise das variações das respostas induzidas por um estímulo localizado fora do CRF de neurônios individuais. Mesmo sendo muito provável que estas conexões tenham também um impacto tanto na atividade conjunta de neurônios envolvidos no processamento da figura quanto no potencial de campo, estas questões permanecem pouco estudadas. Visando examinar a modulação do contexto visual nessas atividades, coletamos potenciais de ação e potenciais de campo em paralelo de até 48 eletrodos implantados na área visual primária de gatos anestesiados. Estimulamos com grades compostas e cenas naturais, focando-nos na atividade de neurônios cujo CRF estava situado na figura. Da mesma forma, visando examinar a influência das conexões laterais, o sinal proveniente da área visual isotópica e contralateral foi removido através da desativação reversível por resfriamento. Fizemos isso devido a: i) as conexões laterais intrínsecas não podem ser facilmente manipuladas sem afetar diretamente os sinais que estão sendo medidos, ii) as conexões inter-hemisféricas compartilham as principais características anatômicas com a rede lateral intrínseca e podem ser vistas como uma continuação funcional das mesmas entre os dois hemisférios e iii) o resfriamento desativa as conexões de forma causal e reversível, silenciando temporariamente seu sinal, permitindo conclusões diretas a respeito da sua contribuição. Nossos resultados demonstram que o mecanismo de segmentação figurafundo se reflete nas taxas de disparo de neurônios individuais, assim como na potência do potencial de campo e na relação entre sua fase e os padrões de disparo produzidos pela população. Além disso, as conexões laterais inter-hemisféricas modulam estas variáveis dependendo da estimulação feita fora do CRF. Observamos também uma influência deste circuito lateral na coerência entre potenciais de campo entre eletrodos distantes. Em conclusão, nossos resultados dão suporte à ideia de um mecanismo complexo de segmentação figura-fundo atuando desde as áreas visuais primárias em diferentes escalas de frequência. Esse mecanismo parece envolver grupos de neurônios ativos sincronicamente e dependentes da fase do potencial de campo. Nossos resultados também são compatíveis com a hipótese que conexões laterais de longo alcance também fazem parte deste mecanismo

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

Visual IMML: um perfil UML para a modelagem de interfaces de usuário

The software development processes proposed by the most recent approaches in Software Engineering make use old models. UML was proposed as the standard language for modeling. The user interface is an important part of the software and has a fundamental importance to improve its usability. Unfortunately the standard UML does not offer appropriate resources to model user interfaces. Some proposals have already been proposed to solve this problem: some authors have been using models in the development of interfaces (Model Based Development) and some proposals to extend UML have been elaborated. But none of them considers the theoretical perspective presented by the semiotic engineering, that considers that, through the system, the designer should be able to communicate to the user what he can do, and how to use the system itself. This work presents Visual IMML, an UML Profile that emphasizes the aspects of the semiotic engineering. This Profile is based on IMML, that is a declarative textual language. The Visual IMML is a proposal that aims to improve the specification process by using a visual modeling (using diagrams) language. It proposes a new set of modeling elements (stereotypes) specifically designed to the specification and documentation of user interfaces, considering the aspects of communication, interaction and functionality in an integrated manner