The real-time refinement calculus: A foundation for machine-independent real-time programming

The real-time refinement calculus is an extension of the standard refinement calculus in which programs are developed from a precondition plus post-condition style of specification. In addition to adapting standard refinement rules to be valid in the real-time context, specific rules are required for the timing constructs such as delays and deadlines. Because many real-time programs may be nonterminating, a further extension is to allow nonterminating repetitions. A real-time specification constrains not only what values should be output, but when they should be output. Hence for a program to implement such a specification, it must guarantee to output values by the specified times. With standard programming languages such guarantees cannot be made without taking into account the timing characteristics of the implementation of the program on a particular machine. To avoid having to consider such details during the refinement process, we have extended our real-time programming language with a deadline command. The deadline command takes no time to execute and always guarantees to meet the specified time; if the deadline has already passed the deadline command is infeasible (miraculous in Dijkstra's terminology). When such a realtime program is compiled for a particular machine, one needs to ensure that all execution paths leading to a deadline are guaranteed to reach it by the specified time. We consider this checking as part of an extended compilation phase. The addition of the deadline command restores for the real-time language the advantage of machine independence enjoyed by non-real-time programming languages.

Computer-aided programming using formally specificed design templates

This paper describes a formal component language, used to support automated component-based program development. The components, referred to as templates, are machine processable, meaning that appropriate tool support, such as retrieval support, can be developed. The templates are highly adaptable, meaning that they can be applied to a wide range of problems. Some of the main features of the language are described, including: higher-order parameters; state variable declarations; specification statements and conditionals; applicability conditions and theories; meta-level place holders; and abstract data structures.

A formal metamodeling approach to a transformation between the UML state machine and object-z

A significant problem with currently suggested approaches for transforming between models in different languages is that the transformation is often described imprecisely, with the result that the overall transformation task may be imprecise, incomplete and inconsistent. This paper presents a formal metamodeling approach for transforming between UML and Object-Z. In the paper, the two languages are defined in terms of their formal metamodels, and a systematic transformation between the models is provided at the meta-level in terms of formal mapping functions. As a consequence, we can provide a precise, consistent and complete transformation between them.

Critical feature analysis of a radiotherapy machine

The software implementation of the emergency shutdown feature in a major radiotherapy system was analyzed, using a directed form of code review based on module dependences. Dependences between modules are labelled by particular assumptions; this allows one to trace through the code, and identify those fragments responsible for critical features. An `assumption tree' is constructed in parallel, showing the assumptions which each module makes about others. The root of the assumption tree is the critical feature of interest, and its leaves represent assumptions which, if not valid, might cause the critical feature to fail. The analysis revealed some unexpected assumptions that motivated improvements to the code.

A IMPORTÂNCIA DAS TICS E DA EDUCAÇÃO COMO PROCESSO COMUNICACIONAL DIALÓGICO NO ENSINO SUPERIOR: Um Estudo da Universidade Estadual de Mato Grosso do Sul

Esta tese teve por objetivo saber como o corpo docente da Universidade Estadual de Mato Grosso do Sul (UEMS) percebe, entende e reage ante a incorporação e utilização das Tecnologias de Informação e Comunicação (TICs) nos cursos de graduação dessa Instituição, considerando os novos processos comunicacionais dialógicos que elas podem proporcionar na sociedade atual. Metodologicamente, a tese é composta por pesquisa bibliográfica, buscando fundamentar as áreas da Educação e Comunicação, assim como a Educomunicação; pesquisa documental para contextualização do lócus da pesquisa e de uma pesquisa exploratória a partir da aplicação de um questionário online a 165 docentes da UEMS, que responderam voluntariamente. Verificou-se que os professores utilizam as TICs cotidianamente nas atividades pessoais e, em menor escala, nos ambientes profissionais. Os desafios estão em se formar melhor esse docente e oferecer capacitação continuada para que utilizem de forma mais eficaz as TICs nas salas de aula. Destaca-se ainda que os avanços em tecnologia e os novos ecossistemas comunicacionais construíram novas e outras realidades, tornando a aprendizagem um fator não linear, exigindo-se revisão nos projetos pedagógicos na educação superior para que estes viabilizem diálogos propositivos entre a comunicação e a educação. A infraestrutura institucional para as TICs é outro entrave apontado, tanto na aquisição como na manutenção desses aparatos tecnológicos pela Universidade. Ao final, propõe-se realizar estudos e pesquisas que possam discutir alterações nos regimes contratuais de trabalho dos docentes, uma vez que, para atuar com as TICs de maneira apropriada, exige-se mais tempo e dedicação do docente.

Edges and bars: where do people see features in 1-D images?

There have been two main approaches to feature detection in human and computer vision - based either on the luminance distribution and its spatial derivatives, or on the spatial distribution of local contrast energy. Thus, bars and edges might arise from peaks of luminance and luminance gradient respectively, or bars and edges might be found at peaks of local energy, where local phases are aligned across spatial frequency. This basic issue of definition is important because it guides more detailed models and interpretations of early vision. Which approach better describes the perceived positions of features in images? We used the class of 1-D images defined by Morrone and Burr in which the amplitude spectrum is that of a (partially blurred) square-wave and all Fourier components have a common phase. Observers used a cursor to mark where bars and edges were seen for different test phases (Experiment 1) or judged the spatial alignment of contours that had different phases (e.g. 0 degrees and 45 degrees ; Experiment 2). The feature positions defined by both tasks shifted systematically to the left or right according to the sign of the phase offset, increasing with the degree of blur. These shifts were well predicted by the location of luminance peaks (bars) and gradient peaks (edges), but not by energy peaks which (by design) predicted no shift at all. These results encourage models based on a Gaussian-derivative framework, but do not support the idea that human vision uses points of phase alignment to find local, first-order features. Nevertheless, we argue that both approaches are presently incomplete and a better understanding of early vision may combine insights from both. (C)2004 Elsevier Ltd. All rights reserved.