Abstract
The analytical methods based on evaluation models of interactive systems were proposed as an alternative to user testing in the last stages of the software development due to its costs. However, the use of isolated behavioral models of the system limits the results of the analytical methods. An example of these limitations relates to the fact that they are unable to identify implementation issues that will impact on usability. With the introduction of model-based testing we are enable to test if the implemented software meets the specified model. This paper presents an model-based approach for test cases generation from the static analysis of source code.

Abstract
ARCHERY is an architectural description language for modelling and reasoning about distributed, heterogeneous and dynamically reconfigurable systems. This paper proposes a structural semantics for ARCHERY, and a method for deriving labelled transition systems (LTS) in which states and transitions represent configurations and reconfiguration operations, respectively. Architectures are modelled by bigraphs and their dynamics by parametric reaction rules. The resulting LTSs can be regarded as Kripke frames, appropriate for verifying reconfiguration constraints over architectural patterns expressed in a modal logic. The derivation method proposed here applies the approach in [1] twice, and combines the results of each application to obtain a label representing a reconfiguration operation and its actual parameters. Labels obtained in this way are minimal and yield LTSs in which bisimulation is a congruence.

Abstract
The recognition of human activities through sensors embedded in smart-phone devices, such as iPhone, is attracting researchers due to its relevance. The advances of this kind of technology are making possible the widespread and pervasiveness of sensing technology to take advantage of multiple sources of sensing to enrich users experience or to achieve proactive, context-aware applications and services. Human activity recognition and monitoring involves a continuing analysis of large amounts of data so, any increase or decrease in accuracy results in a wide variation in the number of activities correctly classied and incorrectly classied, so it is very important to increase the rate of correct classication. We have researched on a vector with 159 different features and on the vector subsets in order to improve the human activities recognition. We extracted features from the Magnitude of the Signal, the raw signal data, the vertical acceleration, the Horizontal acceleration, and the ltered Raw data. In the evaluation process we used the classiers: Naive Bayes, K-Nearest Neighbor and Random Forest. The features were extracted using the java programming language and the evaluation was done with WEKA. The maximum accuracy was obtained, as expected, with Random Forest using all the 159 features. The best subset found has twelve features: the Pearson correlation between vertical acceleration and horizontal acceleration, the Pearson correlation between x and y, the Pearson correlation between x and z, the STD of acceleration z, the STD of digital compass y, the STD of digital compass z, the STD of digital compass x, the mean between axis, the energy of digital compass x, the mean of acceleration x, the mean of acceleration z, the median of acceleration z.

Abstract
E-Learning frameworks are conceptual tools to organize networks of elearning services. Most frameworks cover areas that go beyond the scope of e-learning, from course to financial management, and neglects the typical activities in everyday life of teachers and students at schools such as the creation, delivery, resolution and evaluation of assignments. This paper presents the Ensemble framework - an e-learning framework exclusively focused on the teaching-learning process through the coordination of pedagogical services. The framework presents an abstract data, integration and evaluation model based on content and communications specifications. These specifications must base the implementation of networks in specialized domains with complex evaluations. In this paper we specialize the framework for two domains with complex evaluation: computer programming and computer-aided design (CAD). For each domain we highlight two Ensemble hotspots: data and evaluations procedures. In the former we formally describe the exercise and present possible extensions. In the latter, we describe the automatic evaluation procedures.

Abstract
Theoretical standard models and regulatory actions often ignore that firms are competing with other firms in related markets. In these contexts, cross-price relationships should be taken into account. The usual instinct with multiproduct firms would be to use Ramsey prices to find optimal markups. However, this is only applicable in situations with independent demand functions. Literature mostly covers cases where the regulated firm is a natural monopoly and therefore faces a budget constraint. This paper aims to provide conditions under which optimal price caps are set whenever there are related markets and the regulated firm is not a natural monopoly.

Abstract
Birefringence tunability is demonstrated in waveguides formed in bulk fused silica and in the core of single mode fibers, by femtosecond laser writing of stress inducing tracks that are placed with different geometries around the core of the waveguides. The femtosecond laser generated stress effect was probed by the birefringence induced spectral splitting of either Bragg grating waveguides in bulk fused silica or weakly modulated, femtosecond laser induced Bragg gratings in optical fibers. Birefringence values as low as 4 x 10(-6) and up to 2 x 10(-3) were obtained by controlling the fabrication conditions such as the laser pulse energy, the writing femtosecond laser polarization, the number of overwriting exposures, and the geometry of the induced stress tracks. Wave retarders are developed and characterized by a cross polarization technique to provide the spectral response of the stress induced birefringence, offering the convenient fabrication of short length and broadband in-line polarization devices. With this approach, millimeter length tracks provided 10 nm bandwidth polarization retarders in a single mode fiber and a 65 nm bandwidth retarders in bulk fused silica.