Abstract
This paper presents the timing analysis methodology developed in the European project P-SOCRATES (Parallel Software Framework for Time-Critical Many-core Systems). This timing analysis methodology is defined for parallel applications that must satisfy both performance and real-time requirements and are executed on modern many-core processor architectures. We discuss the motivation and objectives of the project, the timing analysis flow that we proposed, the tool that has been developed to automatize it, and finally we report on some of the preliminary results that we have obtained when applying this methodology to the three application use-cases of the project.

Abstract
There exist many dataflow applications with timing constraints that require real-time guarantees on safe execution without violating their deadlines. Extraction of timing parameters (offsets, deadlines, periods) from these applications enables the use of real-time scheduling and analysis techniques, and provides guarantees on satisfying timing constraints. However, existing extraction techniques require the transformation of the dataflow application from highly expressive dataflow computational models, for example, Synchronous Dataflow (SDF) and Cyclo-Static Dataflow (CSDF) to Homogeneous Synchronous Dataflow (HSDF). This transformation can lead to an exponential increase in the size of the application graph that significantly increases the runtime of the analysis. In this article, we address this problem by proposing an offline heuristic algorithm called slack-based merging. The algorithm is a novel graph reduction technique that helps in speeding up the process of timing parameter extraction and finding a feasible real-time schedule, thereby reducing the overall design time of the real-time system. It uses two main concepts: (a) the difference between the worst-case execution time of the SDF graph's firings and its timing constraints (slack) to merge firings together and generate a reducedsize HSDF graph, and (b) the novel concept of merging called safe merge, which is a merge operation that we formally prove cannot cause a live HSDF graph to deadlock. The results show that the reduced graph (1) respects the throughput and latency constraints of the original application graph and (2) typically speeds up the process of extracting timing parameters and finding a feasible real-time schedule for real-time dataflow applications. They also show that when the throughput constraint is relaxed with respect to the maximal throughput of the graph, the merging algorithm is able to achieve a larger reduction in graph size, which in turn results in a larger speedup of the real-time scheduling algorithms.

Abstract
The safety-critical real-time embedded domain increasingly demands the use of parallel architectures to fulfill performance requirements. Such architectures require the use of parallel programming models to exploit the underlying parallelism. This paper evaluates the applicability of using OpenMP, a widespread parallel programming model, with Ada, a language widely used in the safety-critical domain. Concretely, this paper shows that applying the OpenMP tasking model to exploit fine-grained parallelism within Ada tasks does not impact on programs safeness and correctness, which is vital in the environments where Ada is mostly used. Moreover, we compare the OpenMP tasking model with the proposal of Ada extensions to define parallel blocks, parallel loops and reductions. Overall, we conclude that the OpenMP tasking model can be safely used in such environments, being a promising approach to exploit fine-grain parallelism in Ada tasks, and we identify the issues which still need to be further researched.

Abstract
The energy consumption of the current building stock represents about 40% of the total final energy consumption in Europe. New gamification techniques may play a significant role in helping users adopt new and more energy efficient behaviours. This paper presents the advances achieved within the context of the EU-funded project EnerGAware - Energy Game for Awareness of energy efficiency in social housing communities. The main objective of the project, funded by the European Union under the Horizon2020 programme, is to reduce the energy consumption and carbon emissions in a sample of European social housing by changing the energy efficiency behaviour of the social tenants through the implementation of a serious game linked to the real energy use of the participants' homes. © 2017 IEEE.

Abstract
The IEC 61499 standard provides means to specify distributed control systems in terms of function blocks. For the deployment, each device may hold one or many logical resources, each consisting of a function block network with service interface blocks at the edges. The execution model is event driven (asynchronous), where triggering events may be associated with data (and seen as messages). In this paper, we propose a low-complexity implementation technique allowing to assess end-to-end response times of event chains spanning over a set of networked devices. Based on a translation of IEC 61499 to RTFM1-tasks and resources, the response time for each task in the system at the device-level can be derived using established scheduling techniques. In this paper, we develop a holistic method to provide safe end-to-end response times taking both intra and interdevice delivery delays into account. The novelty of our approach is the accuracy of the system scheduling overhead characterization. While the device-level (RTFM) scheduling overhead was discussed in previous works, the network-level scheduling overhead for switched Ethernets is discussed in this paper. The approach is generally applicable to a wide range of commercial off-the-shelf Ethernet switches without a need for expensive custom solutions to provide hard real-time performance. A behavior characterization of the utilized switch determines the guaranteed response times. As a use case, we study the implementation onto (single-core) Advanced RISC Machine (ARM)-cortex-based devices communicating over a switched Ethernet network. For the analysis, we define a generic switch model and an experimental setup allowing us to study the impact of network topology as well as 802.1Q quality of service in a mixed critical setting. Our results indicate that safe sub millisecond end-to-end response times can be obtained using the proposed approach.

Abstract
The IEC 61499 standard proposes an event driven execution model for component based (in terms of Function Blocks), distributed industrial automation applications. However, the standard provides only an informal execution semantics, thus in consequence behavior and correctness relies on the design decisions made by the tool vendor. In this paper we present the formalization of a subset of the IEC 61499 standard in order to provide an underpinning for the static verification of Function Block models by means of deductive reasoning. Specifically, we contribute by addressing verification at the component, algorithm, and ECC levels. From Function Block descriptions, enriched with formal contracts, we show that correctness of component compositions, as well as functional and transitional behavior can be ensured. Feasibility of the approach is demonstrated by manually encoding a set of representative use-cases in WhyML, for which the verification conditions are automatically derived (through the Why3 platform) and discharged (using automatic SMT-based solvers). Furthermore, we discuss opportunities and challenges towards deriving certified executables for IEC 61499 models. © 2016 IEEE.