Abstract
This paper describes the use of an automated theorem prover to analyse properties of interactive behaviour. It offers an alternative to model checking for the analysis of interactive systems. There are situations, for example when demonstrating safety, in which alternative complementary analyses provide assurance to the regulator. The rigour and detail offered by theorem proving makes it possible to explore features of the design of the interactive system, as modelled, beyond those that would be revealed using model checking. Theorem proving can also speed up proof in some circumstances. The paper illustrates how a theory generated as a basis for theorem proving (using PVS) was developed systematically from a MAL model used to model check the same properties. It also shows how the CTL properties used to check the original model can be translated into theorems.

Abstract
An intensity-based highly birefringent (Hi-Bi) fiber loop mirror (FLM) sensor is proposed which uses a wavelength-division multiplexing (WDM) fiber coupler. The effect of integrating the WDM coupler in a FLM configuration is first studied. A section of Hi-Bi (bow-tie) fiber of length 0.26 m is then placed in the fiber loop, making the spectral response of the device simultaneously dependent on the Hi-Bi fiber section and WDM coupler characteristics. When strain is applied to the sensing head, the spectral signal is modulated in amplitude, in contrast with the conventional Hi-Bi FLM sensors in which there are wavelength shifts. The sensor was characterized in strain and a sensitivity of (-2.2 +/- 0.4) x 10(-3) mu epsilon(-1) for a range of 300 mu epsilon was attained. The self-referenced character of the sensor is noted. (C) 2013 Optical Society of America

Abstract
To evaluate the in vitro effects of sunitinib malate and meloxicam in isolation, and to analyse the ability of meloxicam to enhance the cytotoxicity of sunitinib malate in three human bladder-cancer call lines. Cell lines were treated with sunitinib malate and meloxicam, either in isolation or combined. Leishman staining, MTT method, comet assay, MDC staining and M30 CytoDEATH antibody were performed. The Chou and Talalay method was applied. Sunitinib malate and meloxicam supressed cell proliferation in bladder-cancer cells in isolation, in a concentration-dependent manner. Treatment of bladder-cancer cells with a combination of sunitinib malate and meloxicam showed a synergistic effect. When exploring the mechanism of this combination by means of comet assay, there is the suggestion that meloxicam increases sunitinib malate cytotoxicity through DNA damage. Autophagic and apoptotic studies show a greater incidence of autophagic vacuoles and early apoptotic cells when the combined treatment was put into use. In isolation, sunitinib malate and meloxicam demonstrated anti-tumor effects in our study. Furthermore, simultaneous exposure of cells to sunitinib malate and meloxicam provided a combinatorial beneficial effect. This hints at the possibility of a new combined therapeutic regimen, which could lead to improvements in the treatment of patients with bladder cancer.

Abstract

Abstract
Serious Games are games where the entertainment aspect is not the most relevant purpose. Beyond the motivation as key for the success, Serious Games have challenging goals; they are fun to play and/or engaging; they incorporate some concepts of scoring; and they impart skills, knowledge and attitudes that can be applied in the real world. The growing interest on this type of game results from several factors such as: the theoretical grounding in different learning theories, the development of high-quality gaming experiences, the increased offer of collaboration and competition in multiplayer modes and the opportunity for integrated assessment. This technology can be applied to aid players developing professional skills, but how do we certify the acquired knowledge and skills? This paper proposes a new approach based on serious game for competencies certification using in-game validation. A new correlation matrix is defined associating the game mechanics of serious games and an array of competences, identifying the most suitable game mechanics for each specific competence. This generic matrix represents the results of the analysis about what the student should learn, understand and be able to do after they complete the learning process for a specific task or job position (competencies) and the most adequate game mechanics. Lominger's set of sixty seven competences becomes a universal common denominator as most of these competencies lead to task success which allowed its author, in collaboration with Microsoft, to create a similar approach, but this one focused solely on education and learning: The Educational Competency Wheel. This new approach is based on a set of success factors which can be mapped into required attributes, behaviors, areas of knowledge, skills and abilities for successful performance. With this paper we describe the strategy used to build the generic correlation. The applicability of this generic matrix will be done in four steps. Firstly it is necessary to identify which specific situations can take advantage from a game learning approach. The second step is the definition of the learning target group competencies profiles. In this step, the Education Competences serves as a reference to identify which one or combination of competencies must be used to obtain the performance success of each situation. The third step is obtaining the correlation matrix from the generic matrix, identifying the required game mechanics and the quantification of minimum uses of each mechanic. The fourth and final step is the game development that includes an assessment competency model to evaluate the learning progression and training competencies, guaranteeing the successful performing of each situation.

Abstract
Patients' privacy is critical in healthcare but users of Electronic Health Records (EHR) frequently circumvent existing security rules to perform their daily work. Users are so-called the weakest link in security but they are, many times, part of the solution when they are involved in systems' design. In the healthcare domain, the focus is to treat patients (many times with scarce technological, time and human resources) and not to secure their information. Therefore, security must not interfere with this process but be present, nevertheless. Security usability issues must also be met with interdisciplinary knowledge from human-computer-interaction, social sciences and psychology. The main goal of this paper is to raise security and usability awareness with the analysis of users' interaction logs of a BreakTheGlass (BTG) feature. This feature is used to restrict access to patient reports to a group of healthcare professionals within an EHR but also permit access control override in emergency and/or unexpected situations. The analysis of BTG user interaction logs allows, in a short time span and transparently to the user, revealing security and usability problems. This log analysis permits a better choice of methodologies to further apply in the investigation and resolution of the encountered problems.