Development of a Real-time Formative Feedback Student Response System

This paper is focusing IT-supported real-time formative feedback in a classroom context. The development of a Student and Teacher Response System (STRS) is described. Since there are a number of obstacles for effective interaction in large classes, IT can be used to support the teachers aim to find out if students understand the lecture and accordingly adjust the content and design of the lecture. The system can be used for formative assessment before, during, and after a lecture. It is also possible for students to initiate interaction during lectures by posing questions anonymously. The main contributions of the paper are a) the description of the interactive real-time system and b) the development process behind it.

Building an Interactive, Three-dimensional Virtual World

The movement of graphics and audio programming towards three dimensions is to better simulate the way we experience our world. In this project I looked to use methods for coming closer to such simulation via realistic graphics and sound combined with a natural interface. I did most of my work on a Dell OptiPlex with an 800 MHz Pentium III processor and an NVIDlA GeForce 256 AGP Plus graphics accelerator -high end products in the consumer market as of April 2000. For graphics, I used OpenGL [1], an open·source, multi-platform set of graphics libraries that is relatively easy to use, coded in C . The basic engine I first put together was a system to place objects in a scene and to navigate around the scene in real time. Once I accomplished this, I was able to investigate specific techniques for making parts of a scene more appealing.

Seven stories: location based story-delivery system

Location aware content-based experiences have a substantial tradition in HCI, several projects over the last two decades have explored the association of digital media to specific locations or objects. However, a large portion of the literature has little focus on the creative side of designing of the experience and on the iterative process of user evaluations. In this thesis we present two iterations in the design and evaluation of a location based story delivery system (LBSDS), inspired by local folklore and oral storytelling in Madeira. We started by testing an already existing location based story platform, PlaceWear, with short multimedia clips that recounted local traditions and folktales, to this experience we called iLand. An initial evaluation of iLand, was conducted; we shadowed users during the experience and then they responded to a questionnaire. By analyzing the evaluation results we uncovered several issues that informed the redesign of the system itself as well as part of the story content. The outcome of this re design was the 7Stories experience. In the new experience we performed the integration of visual markers in the interface and the framing of the fragmented story content through the literary technique of the narrator. This was done aiming to improving the connection of the audience to the physical context where the experience is delivered. The 7Stories experience was evaluated following a similar methodology to the iLand evaluation but the user’s experience resulted considerably different; because of the same setting for the experience in both versions and the constancy of the most of the content across the two versions we were able to assess the specific effect of the new design and discuss its strengths and shortcomings. Although we did not run a formal and strict comparative test between the two evaluations, it is evident from the collected data how the specific design changes to our LBSDS influenced the user experience.

ENHANCEMENT OF THE FAA’s ON-LINE WILDLIFE AIRCRAFT STRIKE DATABASE WITH AN INTERACTIVE GRAPHICS CAPABILITY

Embry-Riddle Aeronautical University (Prescott, AZ, USA) was awarded a grant from the William J. Hughes FAA Technical Center in October 1999 to develop and maintain a web site dealing with a wide variety of airport safety wildlife concerns. Initially, the web site enabled users to access related topics such as wildlife management (at/near airports), bird identification information, FAA wildlife management guidelines, education, pictures, current news, upcoming meetings and training, available jobs and discussion/forum sections. In April 2001, the web site was augmented with an on-line wildlife strike report (FAA Form 5200-7). Upon submittal on-line, “quick look” email notifications are sent to concerned government personnel. The distribution of these emails varies as to whether there was damage, human injuries/fatalities, and whether feather remains were collected and will be sent to the Smithsonian Institution for identification. In July 2002, a real-time on-line query system was incorporated to allow federal and local government agencies, airport and operator personnel, and USDA and airport wildlife biologists to access this database (which as of June 2005 contains 68,288 researched strike reports added to at a rate of approximately 500 strike reports/month) to formulate strategies to reduce the hazards wildlife present to aviation. To date (June 2005), over 15,000 on-line real-time queries were processed. In June 2004, ERAU was authorized to develop a graphical interface to this on-line query system. Current capabilities include mapping strikes (by species) on the US map, each of the contiguous 48 state maps (with AK and HI being added), and airport diagrams of the major metropolitan airports as well as the next 46 airports with the most reported strikes The latter capability depicts strikes by runway in plan as well as in elevation view. Currently under development is the ability to view time-sequenced strikes on the US map. This extensive graphical interface will give analysts the ability to view strike patterns with a wide variety of variables including species, seasons, migration patterns, etc. on US and state maps and airport diagrams.

Interactive application in spanish sign language for a public transport environment

[ES] En este trabajo se presenta el diseño de una herramienta multimedia que traduce a la lengua de signos españolas los mensajes de avisos que puede proporcionar un sistema de megafonía. El objetivo del trabajo es proporcionar una herramienta que mejore la inclusión social de las personas con discapacidades auditivas. Con este propósito, se han seleccionado el entorno y los mensajes de audio habituales en un aeropuerto para desarrollar este proyecto piloto. Por último, los audios se han traducido a lengua de signos españolas sintetizando un avatar usando la técnica de animación de rotoscopía a partir de la grabación en vídeo de un traductor. Los resultados finales han sido evaluados por personas sordas.

User interaction widgets for interactive theorem proving

Matita (that means pencil in Italian) is a new interactive theorem prover under development at the University of Bologna. When compared with state-of-the-art proof assistants, Matita presents both traditional and innovative aspects. The underlying calculus of the system, namely the Calculus of (Co)Inductive Constructions (CIC for short), is well-known and is used as the basis of another mainstream proof assistant—Coq—with which Matita is to some extent compatible. In the same spirit of several other systems, proof authoring is conducted by the user as a goal directed proof search, using a script for storing textual commands for the system. In the tradition of LCF, the proof language of Matita is procedural and relies on tactic and tacticals to proceed toward proof completion. The interaction paradigm offered to the user is based on the script management technique at the basis of the popularity of the Proof General generic interface for interactive theorem provers: while editing a script the user can move forth the execution point to deliver commands to the system, or back to retract (or “undo”) past commands. Matita has been developed from scratch in the past 8 years by several members of the Helm research group, this thesis author is one of such members. Matita is now a full-fledged proof assistant with a library of about 1.000 concepts. Several innovative solutions spun-off from this development effort. This thesis is about the design and implementation of some of those solutions, in particular those relevant for the topic of user interaction with theorem provers, and of which this thesis author was a major contributor. Joint work with other members of the research group is pointed out where needed. The main topics discussed in this thesis are briefly summarized below. Disambiguation. Most activities connected with interactive proving require the user to input mathematical formulae. Being mathematical notation ambiguous, parsing formulae typeset as mathematicians like to write down on paper is a challenging task; a challenge neglected by several theorem provers which usually prefer to fix an unambiguous input syntax. Exploiting features of the underlying calculus, Matita offers an efficient disambiguation engine which permit to type formulae in the familiar mathematical notation. Step-by-step tacticals. Tacticals are higher-order constructs used in proof scripts to combine tactics together. With tacticals scripts can be made shorter, readable, and more resilient to changes. Unfortunately they are de facto incompatible with state-of-the-art user interfaces based on script management. Such interfaces indeed do not permit to position the execution point inside complex tacticals, thus introducing a trade-off between the usefulness of structuring scripts and a tedious big step execution behavior during script replaying. In Matita we break this trade-off with tinycals: an alternative to a subset of LCF tacticals which can be evaluated in a more fine-grained manner. Extensible yet meaningful notation. Proof assistant users often face the need of creating new mathematical notation in order to ease the use of new concepts. The framework used in Matita for dealing with extensible notation both accounts for high quality bidimensional rendering of formulae (with the expressivity of MathMLPresentation) and provides meaningful notation, where presentational fragments are kept synchronized with semantic representation of terms. Using our approach interoperability with other systems can be achieved at the content level, and direct manipulation of formulae acting on their rendered forms is possible too. Publish/subscribe hints. Automation plays an important role in interactive proving as users like to delegate tedious proving sub-tasks to decision procedures or external reasoners. Exploiting the Web-friendliness of Matita we experimented with a broker and a network of web services (called tutors) which can try independently to complete open sub-goals of a proof, currently being authored in Matita. The user receives hints from the tutors on how to complete sub-goals and can interactively or automatically apply them to the current proof. Another innovative aspect of Matita, only marginally touched by this thesis, is the embedded content-based search engine Whelp which is exploited to various ends, from automatic theorem proving to avoiding duplicate work for the user. We also discuss the (potential) reusability in other systems of the widgets presented in this thesis and how we envisage the evolution of user interfaces for interactive theorem provers in the Web 2.0 era.

Interactive theorem provers: issues faced as a user and tackled as a developer

Interactive theorem provers (ITP for short) are tools whose final aim is to certify proofs written by human beings. To reach that objective they have to fill the gap between the high level language used by humans for communicating and reasoning about mathematics and the lower level language that a machine is able to “understand” and process. The user perceives this gap in terms of missing features or inefficiencies. The developer tries to accommodate the user requests without increasing the already high complexity of these applications. We believe that satisfactory solutions can only come from a strong synergy between users and developers. We devoted most part of our PHD designing and developing the Matita interactive theorem prover. The software was born in the computer science department of the University of Bologna as the result of composing together all the technologies developed by the HELM team (to which we belong) for the MoWGLI project. The MoWGLI project aimed at giving accessibility through the web to the libraries of formalised mathematics of various interactive theorem provers, taking Coq as the main test case. The motivations for giving life to a new ITP are: • study the architecture of these tools, with the aim of understanding the source of their complexity • exploit such a knowledge to experiment new solutions that, for backward compatibility reasons, would be hard (if not impossible) to test on a widely used system like Coq. Matita is based on the Curry-Howard isomorphism, adopting the Calculus of Inductive Constructions (CIC) as its logical foundation. Proof objects are thus, at some extent, compatible with the ones produced with the Coq ITP, that is itself able to import and process the ones generated using Matita. Although the systems have a lot in common, they share no code at all, and even most of the algorithmic solutions are different. The thesis is composed of two parts where we respectively describe our experience as a user and a developer of interactive provers. In particular, the first part is based on two different formalisation experiences: • our internship in the Mathematical Components team (INRIA), that is formalising the finite group theory required to attack the Feit Thompson Theorem. To tackle this result, giving an effective classification of finite groups of odd order, the team adopts the SSReflect Coq extension, developed by Georges Gonthier for the proof of the four colours theorem. • our collaboration at the D.A.M.A. Project, whose goal is the formalisation of abstract measure theory in Matita leading to a constructive proof of Lebesgue’s Dominated Convergence Theorem. The most notable issues we faced, analysed in this part of the thesis, are the following: the difficulties arising when using “black box” automation in large formalisations; the impossibility for a user (especially a newcomer) to master the context of a library of already formalised results; the uncomfortable big step execution of proof commands historically adopted in ITPs; the difficult encoding of mathematical structures with a notion of inheritance in a type theory without subtyping like CIC. In the second part of the manuscript many of these issues will be analysed with the looking glasses of an ITP developer, describing the solutions we adopted in the implementation of Matita to solve these problems: integrated searching facilities to assist the user in handling large libraries of formalised results; a small step execution semantic for proof commands; a flexible implementation of coercive subtyping allowing multiple inheritance with shared substructures; automatic tactics, integrated with the searching facilities, that generates proof commands (and not only proof objects, usually kept hidden to the user) one of which specifically designed to be user driven.

Interactive simulation of flexible parts

Computer simulations play an ever growing role for the development of automotive products. Assembly simulation, as well as many other processes, are used systematically even before the first physical prototype of a vehicle is built in order to check whether particular components can be assembled easily or whether another part is in the way. Usually, this kind of simulation is limited to rigid bodies. However, a vehicle contains a multitude of flexible parts of various types: cables, hoses, carpets, seat surfaces, insulations, weatherstrips... Since most of the problems using these simulations concern one-dimensional components and since an intuitive tool for cable routing is still needed, we have chosen to concentrate on this category, which includes cables, hoses and wiring harnesses. In this thesis, we present a system for simulating one dimensional flexible parts such as cables or hoses. The modeling of bending and torsion follows the Cosserat model. For this purpose we use a generalized spring-mass system and describe its configuration by a carefully chosen set of coordinates. Gravity and contact forces as well as the forces responsible for length conservation are expressed in Cartesian coordinates. But bending and torsion effects can be dealt with more effectively by using quaternions to represent the orientation of the segments joining two neighboring mass points. This augmented system allows an easy formulation of all interactions with the best appropriate coordinate type and yields a strongly banded Hessian matrix. An energy minimizing process accounts for a solution exempt from the oscillations that are typical of spring-mass systems. The use of integral forces, similar to an integral controller, allows to enforce exactly the constraints. The whole system is numerically stable and can be solved at interactive frame rates. It is integrated in the DaimlerChrysler in-house Virtual Reality Software veo for use in applications such as cable routing and assembly simulation and has been well received by users. Parts of this work have been published at the ACM Solid and Physical Modeling Conference 2006 and have been selected for the special issue of the Computer-Aided-Design Journal to the conference.

A new system for computer-aided preoperative planning and intraoperative navigation during corrective jaw surgery

A new system for computer-aided corrective surgery of the jaws has been developed and introduced clinically. It combines three-dimensional (3-D) surgical planning with conventional dental occlusion planning. The developed software allows simulating the surgical correction on virtual 3-D models of the facial skeleton generated from computed tomography (CT) scans. Surgery planning and simulation include dynamic cephalometry, semi-automatic mirroring, interactive cutting of bone and segment repositioning. By coupling the software with a tracking system and with the help of a special registration procedure, we are able to acquire dental occlusion plans from plaster model mounts. Upon completion of the surgical plan, the setup is used to manufacture positioning splints for intraoperative guidance. The system provides further intraoperative assistance with the help of a display showing jaw positions and 3-D positioning guides updated in real time during the surgical procedure. The proposed approach offers the advantages of 3-D visualization and tracking technology without sacrificing long-proven cast-based techniques for dental occlusion evaluation. The system has been applied on one patient. Throughout this procedure, we have experienced improved assessment of pathology, increased precision, and augmented control.

The exchange of radiotherapy data as part of an electronic patient-referral system

PURPOSE: To describe the implementation and use of an electronic patient-referral system as an aid to the efficient referral of patients to a remote and specialized treatment center. METHODS AND MATERIALS: A system for the exchange of radiotherapy data between different commercial planning systems and a specially developed planning system for proton therapy has been developed through the use of the PAPYRUS diagnostic image standard as an intermediate format. To ensure the cooperation of the different TPS manufacturers, the number of data sets defined for transfer has been restricted to the three core data sets of CT, VOIs, and three-dimensional dose distributions. As a complement to the exchange of data, network-wide application-sharing (video-conferencing) technologies have been adopted to provide methods for the interactive discussion and assessment of treatments plans with one or more partner clinics. RESULTS: Through the use of evaluation plans based on the exchanged data, referring clinics can accurately assess the advantages offered by proton therapy on a patient-by-patient basis, while the practicality or otherwise of the proposed treatments can simultaneously be assessed by the proton therapy center. Such a system, along with the interactive capabilities provided by video-conferencing methods, has been found to be an efficient solution to the problem of patient assessment and selection at a specialized treatment center, and is a necessary first step toward the full electronic integration of such centers with their remotely situated referral centers.

Monitoring protein-protein interactions between the mammalian integral membrane transporters and PDZ-interacting partners using a modified split-ubiquitin membrane yeast two-hybrid system

PDZ-binding motifs are found in the C-terminal tails of numerous integral membrane proteins where they mediate specific protein-protein interactions by binding to PDZ-containing proteins. Conventional yeast two-hybrid screens have been used to probe protein-protein interactions of these soluble C termini. However, to date no in vivo technology has been available to study interactions between the full-length integral membrane proteins and their cognate PDZ-interacting partners. We previously developed a split-ubiquitin membrane yeast two-hybrid (MYTH) system to test interactions between such integral membrane proteins by using a transcriptional output based on cleavage of a transcription factor from the C terminus of membrane-inserted baits. Here we modified MYTH to permit detection of C-terminal PDZ domain interactions by redirecting the transcription factor moiety from the C to the N terminus of a given integral membrane protein thus liberating their native C termini. We successfully applied this "MYTH 2.0" system to five different mammalian full-length renal transporters and identified novel PDZ domain-containing partners of the phosphate (NaPi-IIa) and sulfate (NaS1) transporters that would have otherwise not been detectable. Furthermore this assay was applied to locate the PDZ-binding domain on the NaS1 protein. We showed that the PDZ-binding domain for PDZK1 on NaS1 is upstream of its C terminus, whereas the two interacting proteins, NHERF-1 and NHERF-2, bind at a location closer to the N terminus of NaS1. Moreover NHERF-1 and NHERF-2 increased functional sulfate uptake in Xenopus oocytes when co-expressed with NaS1. Finally we used MYTH 2.0 to demonstrate that the NaPi-IIa transporter homodimerizes via protein-protein interactions within the lipid bilayer. In summary, our study establishes the MYTH 2.0 system as a novel tool for interactive proteomics studies of membrane protein complexes.

Virtual reality ultrasound imaging of the normal and abnormal fetal central nervous system

OBJECTIVES: In fetal ultrasound imaging, teaching and experience are of paramount importance to improve prenatal detection rates of fetal abnormalities. Yet both aspects depend on exposure to normal and, in particular, abnormal 'specimens'. We aimed to generate a number of simple virtual reality (VR) objects of the fetal central nervous system for use as educational tools. METHODS: We applied a recently proposed algorithm for the generation of fetal VR object movies to the normal and abnormal fetal brain and spine. Interactive VR object movies were generated from ultrasound volume data from normal fetuses and fetuses with typical brain or spine anomalies. Pathognomonic still images from all object movies were selected and annotated to enable recognition of these features in the object movies. RESULTS: Forty-six virtual reality object movies from 22 fetuses (two with normal and 20 with abnormal brains) were generated in an interactive display format (QuickTime) and key images were annotated. The resulting .mov files are available for download from the website of this journal. CONCLUSIONS: VR object movies can be generated from educational ultrasound volume datasets, and may prove useful for teaching and learning normal and abnormal fetal anatomy.

How to Improve the Production Process for interactive TV with semi-formal Methods

The central question for this paper is how to improve the production process by closing the gap between industrial designers and software engineers of television(TV)-based User Interfaces (UI) in an industrial environment. Software engineers are highly interested whether one UI design can be converted into several fully functional UIs for TV products with different screen properties. The aim of the software engineers is to apply automatic layout and scaling in order to speed up and improve the production process. However, the question is whether a UI design lends itself for such automatic layout and scaling. This is investigated by analysing a prototype UI design done by industrial designers. In a first requirements study, industrial designers had created meta-annotations on top of their UI design in order to disclose their design rationale for discussions with software engineers. In a second study, five (out of ten) industrial designers assessed the potential of four different meta-annotation approaches. The question was which annotation method industrial designers would prefer and whether it could satisfy the technical requirements of the software engineering process. One main result is that the industrial designers preferred the method they were already familiar with, which therefore seems to be the most effective one although the main objective of automatic layout and scaling could still not be achieved.

Interactive Augmentation of Live Images using a HDR Stereo Camera

Adding virtual objects to real environments plays an important role in todays computer graphics: Typical examples are virtual furniture in a real room and virtual characters in real movies. For a believable appearance, consistent lighting of the virtual objects is required. We present an augmented reality system that displays virtual objects with consistent illumination and shadows in the image of a simple webcam. We use two high dynamic range video cameras with fisheye lenses permanently recording the environment illumination. A sampling algorithm selects a few bright parts in one of the wide angle images and the corresponding points in the second camera image. The 3D position can then be calculated using epipolar geometry. Finally, the selected point lights are used in a multi pass algorithm to draw the virtual object with shadows. To validate our approach, we compare the appearance and shadows of the synthetic objects with real objects.