Abstract
Smart grids play an important role in the modernization and optimization of the existing electrical grid, to accomplish the current European Union Energy and Climate targets. Smart grids require distributed applications to manage the grid more efficiently. The performance of the distributed applications impacts on the communications delay time and on the timely interaction with the devices located in the users' Home Area Networks. This paper presents the results of the ENCOURAGE project related to the development of a software platform to support smart grids. The work presented in this paper assesses four different middleware configurations and analyses the results on the delay performance tests. The results show that the mean end-to-end delay is between 310 ms and 453 ms in proper conditions. In terms of operational costs, the optimal configuration enables managing houses with less than 0.25 Euros per month per house. This paper justifies the maturity of the technology to support smart grids, and the possibility to transfer the ENCOURAGE project results to the industry.

Abstract
The need for maintenance is based on the wear of components of machinery. If this need can be defined reliably beforehand so that no unpredicted failures take place then the maintenance actions can be carried out economically with minimum disturbance to production. There are two basic challenges in solving the above. First understanding the development of wear and failures, and second managing the measurement and diagnosis of such parameters that can reveal the development of wear. In principle the development of wear and failures can be predicted through monitoring time, load or wear as such. Monitoring time is not very efficient, as there are only limited numbers of components that suffer from aging which as such is result of chemical wear i.e. changes in the material. In most cases the loading of components influences their wear. In principle the loading can be stable or varying in nature. Of these two cases the varying load case is much more challenging than the stable one. The monitoring of wear can be done either directly e.g. optical methods or indirectly e.g. vibration. Monitoring actual wear is naturally the most reliable approach, but it often means that additional investments are needed. The paper discusses the above issues and what are the requirements that follow from these for optimising maintenance based of the use of Cyber Physical Systems.

Abstract
The first session of the 18th International Real Time Ada Workshop discussed two aspects of parallel programming in real-time systems, the use of executors in parallel systems, and syntax to guide the reduction of parallel computations to return a correct single answer. This report captures the discussions held and the decisions and recommendations of the workshop on these topics.

Abstract
The main goals of this conference session was to present an overview of a model for fine-grained parallelism in Ada based on the notion of tasklets. The session presented and discussed a general execution model that would support parallelism constructs being considered for possible inclusion in a future version of the Ada standard. The session also presented and discussed a real-time model that provided consistency with the general model while providing enough flexibility to accommodate a wide range of real-time systems with the intent supporting real-time analysis and maintaining or improving the safety features of the language.

Abstract

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.