Abstract
Most model checkers provide a useful simulation mode, that allows users to explore the set of possible behaviours by interactively picking at each state which event to execute next. Traditionally this simulation mode cannot take into consideration additional temporal logic constraints, such as arbitrary fairness restrictions, substantially reducing its usability for debugging the modelled system behaviour. Similarly, when a specification is false, even if all its counter-examples combined also form a set of behaviours, most model checkers only present one of them to the user, providing little or no mechanism to explore alternatives. In this paper, we present a simple on-the-fly verification technique to allow the user to explore the behaviours that satisfy an arbitrary temporal logic specification, with an interactive process akin to simulation. This technique enables a unified interface for simulating the modelled system and exploring its counter-examples. The technique is formalised in the framework of state/event linear temporal logic and a proof of concept was implemented in an event-based variant of the Electrum framework. © J. Brunel, D. Chemouil, A. Cunha, & N. Macedo.

Abstract
Low performance of nontechnical engineering students in programming courses is a problem that remains unsolved. Over the years, many authors have tried to identify the multiple causes for that failure, but there is unanimity on the fact that motivation is a key factor for the acquisition of knowledge by students. To better understand motivation, a new evaluation strategy has been adopted in a second programming course of a nontechnical degree, consisting of 91 students. The goals of the study were to identify if those students felt more motivated to answer multiple-choice questions in comparison to development questions, and what type of question better allows for testing student knowledge acquisition. Possibilities around the motivational qualities of multiple-choice questions in programming courses will be discussed in light of the results. In conclusion, it seems clear that student performance varies according to the type of question. Our study points out that multiple-choice questions can be seen as a motivational factor for engineering students and it might also be a good way to test acquired programming concepts. Therefore, this type of question could be further explored in the evaluation points.

Abstract

Abstract
Optical waveguides directly written in fused silica using a femtosecond laser were characterized from 350 to 1750 nm to gain insight on the waveguide's loss mechanisms and their dependence on processing parameters, such as pulse energy, scan velocity, and annealing temperature. Two major loss mechanisms were identified. In the range of parameters tested, high pulse energy was seen to improve coupling losses at long wavelengths, while high scan velocity has a negative effect in both Rayleigh scattering and coupling losses at long wavelengths. Thermal annealing of the waveguides demonstrated an improvement of the Rayleigh scattering at a cost of higher coupling losses at long wavelengths. Wavelength independent Mie scattering was also observed, evolving negatively with pulse energy. A minimum Rayleigh scattering coefficient of approximate to 0.5 dB.cm(-1).mu m(4) (approximate to 0.08 dB.cm(-1).mu m(4) for thermally treated waveguides) together with a Mie scattering coefficient of approximate to 0.2-0.65 dB/cm are reported.

Abstract
The growth of intermittent renewable power generation has been drawing attention to the design of balancing markets. Portugal is an interesting case study because wind generation already accounts for a high fraction of demand (23% in 2012-2016), but still there are no economic incentives for efficient wind forecasting (wind balancing costs are passed to end consumers). We analyze the evolution of the balancing market from 2012 to 2016. Using actual market data, we find wind balancing costs around 2 euros per MWh of generated energy. One main reason for these low costs is the existence of a robust transmission grid, which allows for the compensation of positive with negative wind imbalances across the system. Nevertheless, the results suggest that final consumers could save several million euros per year if wind generators were made responsible for the economic cost of their imbalances, in line with other European markets.

Abstract
In this study, the operation of an energy system composed of a battery energy storage system (BESS) and a conventional generator to compensate the forecasting error of renewable power production has been analyzed. A scenario with low forecasting error and another with high forecasting error have been synthetically modeled and incorporated to a computational model of the energy system. The results obtained from a case study suggest that a low forecasting error could be compensated by a single BESS. However, a high forecasting error would require the installation of a controllable power source such as a conventional generator.