Abstract
A realistic user interface is rigorously developed for the US Food and Drug Administration (FDA) Generic Patient Controlled Analgesia (GPCA) pump prototype. The GPCA pump prototype is intended as a realistic workbench for trialling development methods and techniques for improving the safety of such devices. A model-based approach based on the use of formal methods is illustrated and implemented within the Prototype Verification System (PVS) verification system. The user interface behaviour is formally specified as an executable PVS model. The specification is verified with the PVS theorem prover against relevant safety requirements provided by the FDA for the GPCA pump. The same specification is automatically translated into executable code through the PVS code generator, and hence a high fidelity prototype is then developed that incorporates the generated executable code. © 2013 Springer-Verlag.

Abstract
Assistive Technologies may greatly contribute to give autonomy and independence for individuals with physical limitations. Electric wheelchairs are examples of those assistive technologies and nowadays each time becoming more intelligent due to the use of technology that provides assisted safer driving. Usually, the user controls the electric wheelchair with a conventional analog joystick. However, this implies the need for an appropriate methodology to map the position of the joystick handle, in a Cartesian coordinate system, to the wheelchair wheels intended velocities. This mapping is very important since it will determine the response behavior of the wheelchair to the user manual control. This paper describes the implementation of several joystick mappings in an intelligent wheelchair (IW) prototype. Experiments were performed in a realistic simulator using cerebral palsy users with distinct driving abilities. The users had 6 different joystick control mapping methods and for each user the usability and the users' preference order was measured. The results achieved show that a linear mapping, with appropriate parameters, between the joystick's coordinates and the wheelchair wheel speeds is preferred by the majority of the users.

Abstract
Active pre-main-sequence binaries with separations of around 10 stellar radii present a wealth of phenomena unobserved in common systems. The study of these objects is extended from classical T Tauri stars to the Herbig Ae star HD 104237. The primary has a mass 2.2 +/- 0.2 M-circle dot and secondary 1.4 +/- 0.3 M-circle dot. Spectrointerferometry with the VLTI/AMBER in the K-band continuum and the Br gamma line is presented. It is found that the K-band continuum squared visibilities are compatible with a circumbinary disc with a radius of similar to 0.5 AU. However, a significant fraction (similar to 50 per cent) of the flux is unresolved and not fully accounted by the stellar photospheres. The stars probably do not hold circumstellar discs, in addition to the circumbinary disc, due to the combined effects of inner magnetospheric truncation and outer tidal truncation. This unresolved flux likely arises in compact structures inside the tidally disrupted circumbinary disc. Most (greater than or similar to 90 per cent) of the Br gamma line emission is unresolved. The line-to-continuum spectroastrometry shifts in time, along the direction of the Ly alpha jet known to be driven by the system. The shift is anticorrelated with the Br gamma equivalent width. It is shown that the unresolved Br gamma emission cannot originate in the jet but instead is compatible with stellar emission from the orbiting binary components. The increase in the absolute value of the equivalent width of the line takes place at periastron passage; it could arise in an accretion burst, a flare or in the increase in effective size of the emission region by the interaction of the magnetospheres. The binary longitude of the ascending node is found to be Omega = (235 +/- 3)degrees and the orbit retrograde. The origin of the jet is revisited. The tidal disruption of the circumstellar discs creates difficulties to ejection models that rely on stellar magnetosphere and disc coupling. A scenario of a stellar wind collimated by a circumbinary disc wind is suggested.

Abstract

Abstract
The aim of this paper is to present a cloudlet architecture for dashboard in Cloud and Ubiquitous Manufacturing. In practice means that, with Cloud Computing adoption, Manufacturing requires management applications where ubiquity and effectiveness are enabled. If ubiquity and resources scalability, availability and capacity can be well supported by cloud, pragmatics instruments are required to support effectiveness. The architecture here presented shows the integration of enriched existing (cloud) services, as instances of resources, with layers of new services towards direct and synchronous communication between users. These Rich Internet Application (RIA) components, here named cloudlets, integration, follow dashboards organization patterns and will be supported by emergent web3.0 interaction technologies. In fact, the paper proposes a new Presentation Layer to be used in UMS and (that may be used) in any multi-layer cloud-based web application. (C) 2013 Authors. Published by Elsevier B. V.

Abstract
Pectus Carinatum (PC) is a chest deformity consisting on the anterior protrusion of the sternum and adjacent costal cartilages. Non-operative corrections, such as the orthotic compression brace, require previous information of the patient chest surface, to improve the overall brace fit. This paper focuses on the validation of the Kinect scanner for the modelling of an orthotic compression brace for the correction of Pectus Carinatum. To this extent, a phantom chest wall surface was acquired using two scanner systems - Kinect and Polhemus FastSCAN - and compared through CT. The results show a RMS error of 3.25mm between the CT data and the surface mesh from the Kinect sensor and 1.5mm from the FastSCAN sensor.