Abstract

Abstract
Most market operators provide daily data on several market processes, including the results of all market transactions. The use of such data by electricity market simulators is essential for simulations quality, enabling the modelling of market behaviour in a much more realistic and efficient way. RealScen (Realistic Scenarios Generator) is a tool that creates realistic scenarios according to the purpose of the simulation: representing reality as it is, or on a smaller scale but still as representative as possible. This paper presents a novel methodology that enables RealScen to collect real electricity markets information and using it to represent market participants, as well as modelling their characteristics and behaviours. This is done using data analysis combined with artificial intelligence. This paper analyses the way players' characteristics are modelled, particularly in their representation in a smaller scale, simplifying the simulation while maintaining the quality of results. A study is also conducted, comparing real electricity market values with the market results achieved using the generated scenarios. The conducted study shows that the scenarios can fully represent the reality, or approximate it through a reduced number of representative software agents. As a result, the proposed methodology enables RealScen to represent markets behaviour, allowing the study and understanding of the interactions between market entities, and the study of new markets by assuring the realism of simulations.

Abstract
The author's wishes to make the following correction: all the IAE values presented in the paper are multiplied by a factor of 100. The authors would like to apologise for any inconvenience caused. © 2015 Elsevier B.V.

Abstract
Concurrent programming is dominated by thread based solutions with lock based critical sections. Careful attention has to be paid to avoid race and deadlock conditions. Real-Time for The Masses (RTFM) takes an alternative language approach, introducing tasks and named critical sections (via resources) natively in the RTFM-core language. RTFM-core programs can be compiled to native C-code, and efficiently executed onto single-core platforms under the Stack Resource Policy (SRP) by the RTFM-kernel. In this paper we formally define the well-formedness criteria for SRP based resource management, and develop a certified (formally proven) implementation of the corresponding compilation from nested critical sections of the input RTFM-core program to a resulting flat sequence of primitive operations and scheduling primitives. Moreover we formalise the properties for resource ceilings under SRP and develop a certified algorithm for their computation. The feasibility of the described approach is shown through the adoption of the Why3 platform, which allows the necessary verification conditions to be automatically generated and discharged through a variety of automatic external SMT-solvers and interactive theorem provers. Moreover, Why3 supports the extraction of certified Ocaml code for proven implementations in WhyML. As a proof of concept the certified extracted development is demonstrated on an example system. © 2016 IEEE.

Abstract
The paper describes a model that includes an explicit description of the information resources that are assumed to guide use, enabling a focus on properties of "plausible interactions". The information resources supported by an interactive system should be designed to encourage the correct use of the system. These resources signpost a user's interaction, helping to achieve desired goals. Analysing assumptions about information resource support is particularly relevant when a system is safety critical that is when interaction failure consequences could be dangerous, or walk-up-and-use where interaction failure may lead to reluctance to use with expensive consequences. The paper shows that expressing these resource constraints still provides a wider set of behaviours than would occur in practice. A resource may be more or less salient at a particular stage of the interaction and as a result potentially overlooked. For example, the resource may be accessible but not used because it does not seem relevant to the current goal. The paper describes how the resource framework can be augmented with additional information about the salience of the assumed resources. A medical device that is in common use in many hospitals is used as illustration.

Abstract
Conventional sleep analysis relies primarily on electroencephalogram (EEG) waveform features assessed in concert with eye movements, respiration and muscle tone. We explore a complementary 'complexity domain' approach based on multiscale entropy (MSE) analysis of EEG signals and discuss its relationships to standard sleep analysis and to that based on electrocardiogram (ECG)-derived cardiopulmonary coupling (CPC). We observe a progressive decrease in complexity associated with decreased arousability, as measured by both conventional sleep scoring and CPC analysis. Furthermore, complexity analysis supports the contention that stage 2 non-REM sleep has distinct sub-phases that map to CPC high- and low-frequency coupled dynamics. © 2016 IEEE.