Chapter 1 Introduction

This thesis is concerned with models, analysis techniques and tools intended to aid hardware and software designers in exploring their systems design space and finding efficient deployments of application programs on multi-processor platforms. The thesis can be viewed as a confluence point between several academic and industrial research currents in a domain which is very important practically and for which no agreed upon unified theoretical framework exists. To better understand the context of this thesis we mention two of the major driving forces behind the thesis.

Formal Analysis of Timed Systems

Formal verification is a kind of exhaustive simulation of abstract automaton-based models of software and hardware that capture mostly concurrency and synchronization features. Timed models such as timed automata, add quantitative timing information to the models and allow to reason about delays, execution times, deadlines and other performance-related measures. Over the years, a lot of work, at Verimag and elsewhere, explored the applicability of these models to scheduling for embedded (and other) systems and circuits. Although the expressivity of timed automata can be used to model more complex situations than what is possible using classical real-time models, their standard analysis technique (forward computation of reachable states and zones) does not scale up and for the the time being cannot be applied to systems beyond a rather low threshold of size and complexity. Moreover, this type of analysis is worst-case oriented and is not always suitable for soft real-time applications where we care more about the average performance. There is a recent trend in verification, sometimes called statistical model checking, which replaces verification-style exhaustive exploration by Monte-Carlo simulation. In the timed context this means, implicitly or explicitly, to refine temporal uncertainty intervals into distributions supported by those intervals, resulting in some kind of continuous-time "non Markovian" stochastic processes. 1 We use such models in this thesis in two ways. First we do statistical simulation on high-level models of applications running on multi-core platforms and secondly, we develop new semi-analytic techniques for performance evaluation and optimization for duration probabilistic automata that can model a class problems of scheduling under stochastic uncertainty.

The ATHOLE Project

The thesis was aligned, temporally and conceptually, with the ATHOLE project, coordinated by ST Microelectronics, with the participation of CEA-LETI, THALES and CWS. Initially the project was focused on the xSTream architecture but around mid-time, xSTream development has been freezed and the project shifted to Plateform 2012 (P2012). The role of Verimag in the project CHAPTER 1. INTRODUCTION was to apply its expertise in timed systems to help automating deployment decisions (mapping, scheduling) and ease the difficult task of exploiting multi-cores efficiently. The exposure to industrial and quasi-industrial practices and cultures was an opportunity to compare the modeling and analysis methods used by system builders (hardware designers and programmers) and those used by model builders (in verification and performance analysis). The tool described in this thesis, which brings abstract modeling concepts and analysis techniques to these application domains, was a major deliverable in the ATHOLE project.

The thesis is organized as follows:

• Chapter 2 is a very non-exhaustive survey on multi-core embedded systems and the modeling approaches used in various levels of abstraction during the design flow, with emphasis on performance evaluation;

• Chapter 3 is a short introduction to timed automata, symbolic reachability computation on zones and the IF toolset on top of which our tool is implemented;

• Chapter 4 develops a new technique for computing the performance (expected termination time) of schedulers for acyclic scheduling problems (such as job-shop or task-graph) where the duration of each task is considered to be uniformly distributed over a finite interval;

• Chapter 5 attacks the more ambitious synthesis problem and develops a dynamic programming approach to derive expected-time optimal schedulers. These two sections constitute the major theoretical contribution of the thesis and are accompanied by a prototype implementation;

• Chapter 6 is the core of the thesis. It presents our abstract modeling framework for application programs (modeled as extended task-graphs), input generators (the processes that generate new tasks instances subject to temporal and logical constraints), execution platforms (very abstract models of processors, data transfer mechanisms and memories) and deployment (mapping and scheduling policies). Each modeled object is transformed into a timed automaton and the composition of these automata represents all the possible systems behavior;

• Chapter 7 describes the tool DESPEX, the DEsign-SPace EXplorer, its architecture and the type of analysis it provides, namely symbolic reachability computation and Monte-Carlo discrete event simulation, followed by statistical and visual trace analysis;

• Chapter 8 describes three case studies treated by the tool. The first is a toy problem used to demonstrate the advantage of timed automata verification over corner-case simulation.

The second is a video application provided by ST, evaluated for power and performance on P2012 using simulation, and the third is a signal processing application provided by Thales and evaluated on xSTream;

• Chapter 9 concludes the thesis and sketches some ideas for future work.

Chapter 2

Multi-core embedded system

Current embedded applications necessitate intensive computation and data communication which are difficult to handle by a single processor architecture. The performance demanded by these applications, like for example multimedia applications, requires the use of multi-processors architectures in a single chip endowed with complex communication infrastructures, such as hierarchical buses or networks on chips (NoCs). That's why Multiprocessors System on Chip (MPSoC) architectures have become a very attractive solution for the consumer multimedia embedded market [START_REF] Wolf | The future of multiprocessor systems-on-chips[END_REF].

System on Chip (SoC) represents the integration of different computing elements and other electronics subsystems into a single integrated circuit. MPSoC [START_REF] Wolf | Multiprocessor system-on-chip (mpsoc) technology[END_REF] are SoC that may contains one or more types of computing subsystems, memories, I/O devices and other peripherals. Additionally, heterogeneous components are exploited to meet the tight performance and cost constraints. This trend of building heterogeneous MPSoC will be even accelerated due to current embedded application requirements. ITRS (International Technology Roadmap for Semiconductors) roadmap [START_REF]The International Technology Roadmap for Semiconductors (ITRS), System Drivers[END_REF] predicts that the number of processing engines on future MPSoC platforms will increase rapidly (Fig- 2.1), which will introduce a huge complexity into the software development process for such complex platforms. Making the potential parallelism of the applications more explicit so as to exploit the available processing engines, and then efficiently deploying it on the underlying hardware are the new and big challenges for MPSoC software developers. Figure 2.1: Consumer Portable Design Complexity Trends [START_REF]The International Technology Roadmap for Semiconductors (ITRS), System Drivers[END_REF] We will discuss current MPSOC architectures and their different components. Then we will survey the typical embedded systems design flow and see that performance evaluation is done at different level of granularity. Here we are more interested in performance estimation at early design stage. We will present typical modeling techniques and discuss their utility for performance estimation.

MPSOC Architecture

Heterogeneous MPSoC architecture can be represented as a set of processing elements (PE) or components which interact via a communication network (Fig- 2.2). The PE can be of different type like processors (DSP, microcontroller, ASIP, . . . ) or memory elements (caches, DRAM . . . ) connected trough different communication schemes. This type of heterogeneous architecture provides highly concurrent computation and flexible programmability. Heterogeneous MPSoC are composed of different kind of PE as opposed to homogeneous MPSoC where the same type of element is instantiated several times. Figure 2.2: MPSOC Architecture Some heterogeneous platforms from the major semiconductor vendors such as NXP Nexperia [START_REF]Nexperia pnx15xx/952x series data book[END_REF], TI OMAP [185] or ST Nomadik [178] are already available. On the other hand, homogeneous ones were pionnered by the Lucent Daytona architecture [START_REF] Ackland | A single-chip 1.6 billion 16-b mac/s multiprocessor dsp[END_REF][START_REF] Wolf | Multiprocessor system-on-chip (mpsoc) technology[END_REF].

The literature relates mainly two kinds of organizations for multiprocessor architectures, shared memory and message passing [START_REF] Culler | Parallel Computer Architecture: A Hardware/-Software Approach[END_REF]. Heterogeneous MPSoCs generally combine both models and integrate a massive number of processors on a single chip. Future heterogeneous MPSoC will be made of few heterogeneous subsystems, where each subsystem includes a massive number of identical processors to run a specific software stack [START_REF] Jerraya | Programming models and hwsw interfaces abstraction for multi-processor soc[END_REF].

We will now give an overview of the different hardware components in MPSoC.

Processing Elements

Processing elements range in a spectrum between generality and specificity. We can classify them into two major type: General Purpose Processor (GPP) and Application Specific Processors (ASP). GPPs are flexible because they are built to be used in a variety of applications with different specifications. Changing functionalities or improving a system becomes relatively easy when you only need to change a software program. On the other hand ASPs are designed to execute exactly one program, increasing performance and reducing power consumption. However, flexibility and reprogramming is limited because it is designed as a custom digital circuit dedicate to restricted application range. We can distinguish different sub-classes of ASP, such as ASIC (Application Specific Integrated Circuit) where algorithms are completely implemented in hardware and programmable microprocessors like DSP (Digital Signal Processor) for extensive numerical real-time computation, or ASIP (Application Specific Instruction Set Processor) where hardware and instruction set are designed together for one particular application.

Memory Organization

The memory subsystem is an important component of system designs that can benefit from customization. Unlike general purpose processors where a standard cache hierarchy is employed, the memory hierarchy of embedded systems can be tailored in various ways. The memory can be selectively cached. The cache line size can be determined by the application. The designer can opt to discard the cache completely and choose specialized memory configurations such as FIFOs and stream buffers and so on.

The memory is a bottleneck in a computer system since the memory speed cannot keep up with the processor speed and the gap is becoming larger and larger. Memory hierarchy issues are among the most important concerns in designing application-driven embedded systems. A typical embedded system architecture consists of processor cores, reconfigurable hardware, instruction cache, data cache, on-chip scratch memory and on-chip or off-chip DRAM.

The cache is a special high-speed, low volume memory that is in close proximity to the processing hardware that it is reserved for. It can be seen as an interface between the processor and the off-chip memory. Embedded architectures include both data and instruction caches.

Scratch-Pad memory refers to data memory residing on-chip, that is mapped into an address space disjoint from the off-chip memory, but connected to the same address and data buses. Both the cache and Scratch-Pad memory (usually SRAM) allow fast access to their residing data, much faster than accessing off-chip memory. Off-chip memory (usually DRAM) refers to a highest volume memory residing far from the processing element. The main difference between the Scratch-Pad SRAM and data cache is that the SRAM guarantees a single-cycle access time, whereas an access to the cache is subject to cache misses.

Interconnect

The interconnect is a resource shared between various hardware components. Its role is to transmit data from a source to a destination component, thus implementing the communication network. Basically the network component is characterized by two metrics:

• Latency: total time to transfer a quantity of data from the source to the destination component;

• Bandwidth: amount of data that can be transmitted per time unit.

On-chip communication architectures can be divided into the following three main classes [START_REF] Kulmala | Distributed bus arbitration algorithm comparison on fpga-based mpeg-4 multiprocessor system on chip[END_REF]:

1. Point to point interconnect: pairs of processing elements communicate directly over dedicated physically-wired connections [START_REF] Bergamaschi | Designing systems-on-chip using cores[END_REF];

2. Bus architectures [START_REF] Mitic | An overview of on-chip buses[END_REF] : long wires are grouped together to form a single physical entity.

One can find different bus based architecture:

• FPGA-like Bus [START_REF] Cherepacha | Dp-fpga: An fpga architecture optimized for datapaths[END_REF] with programmable interconnects using static network;

• Arbitrated Bus [START_REF]IDT. Idt peripheral bus (ipbus). intermodule connection technology enables broad range of system-level integration[END_REF] with time-shared multiple core connectivity;

• Hierarchical Bus [11,[START_REF] Arm | Multi-layer ahb overview[END_REF][START_REF] Wodey | Lotos code generation for model checking of stbus based soc: the stbus interconnect[END_REF] combining multiple buses using bus bridges.

3. Network on Chip (NoC): Communication is achieved by sending message packets between blocs using an on-chip packet-switched network. NoC is a relatively new chip design paradigm concurrently proposed by many research group [START_REF] Sgroi | Addressing the system-on-a-chip interconnect woes through communicationbased design[END_REF][START_REF] Kumar | A network on chip architecture and design methodology[END_REF][START_REF] Benini | Networks on chips: A new soc paradigm[END_REF]. A survey of research and practices of Network-on-Chip can be found in [START_REF] Bjerregaard | A survey of research and practices of networkon-chip[END_REF].

A component which can be seen as part of the interconnect is Direct Memory Access (DMA). It is a device that can control the memory system without using the CPU. On a specified stimulus, the module will move blocks of data from one memory location to another. DMA is essential for embedded systems since it allows large quantities of information to be transferred to or from memory, while the processor can be doing something else.

Design Flow

Systems-on-chip require the creation and use of radically new design methodologies because some of the key problems in SoC design lie at the boundary between hardware and software.

Classic SoC design flows imply a long design cycle because most of them rely on a sequential approach where complete hardware architecture should first be developed before software could be designed on top of it. This long design cycle is not acceptable because of time to market constraints.

Due to their complexity, the design of embedded systems requires modeling phases at different abstraction levels (Fig- 2.3). At each level, many different activities are required during the design flow: specification and functional modeling, performance modeling, design and synthesis, validation and verification. Because the real product is not available before the development task is completed, all activities operate on models. According to [START_REF] Jantsch | Modeling Embedded Systems and SoC's: Concurrency and Time in Models of Computation[END_REF]:

A model is a simplification of another entity, which can be a physical thing or another model. The model contains exactly those characteristics and properties of the modeled entity that are relevant for a given task. A model is minimal with respect to a task if it does not contain any other characteristics than those relevant for the task.

A model is therefore an abstraction of one entity and may be defined differently according to its use (functional validation, performance evaluation). There is an increasing use of early systemlevel modeling, even if it would not contain the entire hardware architecture, but only a subset of components which are sufficient to allow some level of software verification on the hardware before the full hardware is available, thus reducing the sequential nature of the design process. The use of high-level programming models to abstract hardware/software interfaces is the key enabler for concurrent hardware and software designs. This abstraction allows to separate lowlevel implementation issues from high-level application programming (Fig- 2.3). It also smoothens the design flow and eases the interaction between hardware and software designers. It acts as a contract between hardware and software teams that may work concurrently. Additionally, this scheme eases the integration phase since both hardware and software have been developed to comply with a well-defined interface.

Furthermore programming an application-specific heterogeneous multi-processor architectures becomes one of the key issues for MPSoC, because of two contradictory requirements:

• Reducing software development cost and overall design time: needs high level abstract models; • Improving performance: needs accurate and precise low level models. All models are simplification of reality, an exact copy of a real product can only be the real product itself. So there is always a trade-off as to what level of detail is included in the model, too little detail implies a risk of missing relevant informations and giving wrong predictions, too much detail makes models overly complicated and thus difficult to understand or analyze.

Low Level Modeling

Modeling the hardware is an important phase in the design of an embedded system. It is achieved by developing virtual prototypes that can be fully functional software models of the physical hardware, allowing accurate simulation, design verification and automatic layout generation. The advantage of virtual prototypes lies in their early availability in the development cycle. This way The Y-chart model distinguishes between 3 abstraction domains • Behavioral (functional): describes the temporal and functional behavior of a system without any reference to the particular way in which it is implemented.

• Structural: deals with how the system is composed of interconnected hierarchical subsystems.

• Physical/Geometrical: specifies how the system is laid out in terms of physical placement in space and physical characteristics without any elements of functionality.

Each of these domains can also be divided into levels of abstraction:

• Transistor level

• Logical level

• Register-transfer level (RTL)

• Algorithmic level Each level defines an abstract platform, called virtual prototype on which simulation can be done more or less accurately (cycle accurate, instruction accurate, transaction accurate . . . ). As depicted in Fig- 2.5, highest accuracy is obtained by lowest abstraction level but implies a higher modeling effort as the number of components is huge. Simulation or timing analysis on such models is also a major constraint. Typically a cycle-accurate processor model can be simulated at a rate of between 50 and 1000 instructions per second, while execution on the real hardware is on the order of millions of instructions per second.

• System level
Hardware Description Languages (HDL) are used to model systems at a low level of abstraction, typically at RTL, and are used to do simulation with high precision or to automatically generate the hardware layer. Tools like Verilog [START_REF] Thomas | The VERILOG Hardware Description Language[END_REF] or VHDL [START_REF]IEEE Standards Intepretations: IEEE Std 1076-1987, IEEE Standard VHDL Language Reference Manual[END_REF] are used to specify hardware in a textual format.

Applications

Software too can be described at different levels of abstraction. The lowest level is binary machineexecutable code which is typically generated from a program written in a higher level programming language such as C. An application is then evaluated on a real platform if such exists, or by using a virtual platform. C code is compiled and translated automatically to assembly language and machine code.

More generally, applications are written using a programming model. The programming model specifies how application components are running in parallel and how they communicate including synchronization operations that are available to coordinate their activities. The programming model is usually embodied in a parallel language or a programming environment [START_REF] Culler | Parallel Computer Architecture: A Hardware/-Software Approach[END_REF].

Examples of parallel programming models are as follows:

• Shared address space: communication is performed by posting data into shared memory locations, accessible by all the communicating processing elements; • Data-parallel programming: several processing elements perform the same operations simultaneously, but on separate parts of the same data set; • Message passing: when the communication is performed between a specific sender and a specific receiver.

Examples of such programming models are briefly described in the following:

• StreamIt is an example of programming model for streaming applications [START_REF] Thies | Streamit: A language for streaming applications[END_REF];

• MPI (message-passing interface) [START_REF]MPI: A Message-Passing Interface Standard[END_REF] is a message-passing library interface specification. It includes the specification of a set of primitives for point-to-point communication with message passing, collective communications, process creation and management, one-sided communications, and external interfaces;

• MCAPI (multi-core communications APIs) [START_REF]The multicore association communications api[END_REF] defines a set of communication APIs for multi-core communications, to support lightweight, high performance implementations typically required in embedded applications;

• YAPI (Y-chart application programmer's interface) is an interface to write signal and stream processing applications as process networks, developed by Philips Research [START_REF] De Kock | Yapi: application modeling for signal processing systems[END_REF]. TTL (task transaction level interface) proposed in [START_REF] Van Der Wolf | Design and programming of embedded multiprocessors: an interface-centric approach[END_REF] is derived from YAPI;

• OpenCL (Open computing language) is an open standard for writing applications that execute across heterogeneous platforms consisting of CPUs, GPUs, and other processors, introduced by Khronos working group [START_REF] Lee | An opencl framework for heterogeneous multicores with local memory[END_REF]. OpenCL provides parallel computing using task-based and data-based parallelism;

• OpenMP (open multi-processing) is an application programming interface (API) that supports multi-platform shared memory multiprocessing programming in C, C++, and Fortran on many architectures [START_REF] Chapman | Using OpenMP: Portable Shared Memory Parallel Programming (Scientific and Engineering Computation[END_REF].

Both hardware and software abstraction levels described previously are defined with too much detail for rapid evaluation at early stage of the design flow. It implies a high development effort before performances estimation can be done. The abstraction level close to our work is situated on top of what is generally defined as system-level design.

System-Level Design

In modern system-level design methodology, known as HW/SW co-design, the development of hardware platform and application software is done in parallel. Design space exploration needs separate application and architecture specifications. An explicit mapping step maps application components to architecture. HW/SW co-design includes various design problems including system specification, design space exploration, performance estimation, HW/SW co-verification, and system synthesis. This can be achieved at system level for early estimation and then models are refined at lower level for more accurate performance evaluation.

Modeling and simulation at high abstraction levels are used to increase and to simplify the development and validation of MPSoC at early design stage. For that we need abstract models of both software and hardware components. Defining such models, requires knowledge about hardware and software architecture details as well as execution environment constraints (timing, power consumption . . . ) at early design stages. This can be achieve by hardware-software codesigner based on profiling or past experiences.

Description languages have been developed as well at higher levels of abstraction. At system level, these language can describe abstractions of software and a high level component view of hardware. One can cite for example:

• SystemVerilog [START_REF] Sutherland | SystemVerilog for Design: A Guide to Using SystemVerilog for Hardware Design and Modeling[END_REF] is an extension of Verilog inheriting capabilities for synthesizable modules description (Verilog) and object oriented language abstraction, that allow the verification of complex systems;

• SpecC [START_REF] Fujita | The standard specc language[END_REF] is built on top of ANSI-C programming language and is intended for the specification and design of digital embedded systems, including hardware and software portions and supports concepts like behavioral and structural hierarchy, concurrency, communication, synchronization, state transitions, exception handling, and timing;

• SystemC transaction-level modeling (TLM) is another standardization work [START_REF] Ghenassia | Transaction-Level Modeling with SystemC: TLM Concepts and Applications for Embedded Systems[END_REF] which offers a set of standard APIs and a library, built on top of C++ programming language, that implements a foundation layer upon which interoperable transaction-level models can be built;

• AADL (Architecture Analysis and Design Language) [START_REF] Peter | The architecture analysis & design language (AADL): An introduction[END_REF] defines a language for describing both the software architecture and the execution platform architecture of performancecritical, embedded, real-time systems. It describes a system as a hierarchy of components with their interfaces and their interconnections, specifying both functional interfaces and aspects critical for performance;

• SysML [START_REF] Weilkiens | Systems Engineering with SysML/UML: Modeling, Analysis, Design[END_REF] is based on an extension of the Unified Modeling Language (UML) and has views that deal with multiple aspects of the system: functional and behavioral, structural, performance, and slew of other models like cost and safety.

Underlying the specification of embedded systems there is the notion of Model of computation and communication which defines more formally how concurrent components interact with each other. A multitude of modeling formalisms have been applied to embedded system design. Typically, these formalisms strive for a maximum of precision, as they rely on a mathematical (formal) model. We will presents next the main classes of models used in the design of MPSoC.

Models of Computation for Embedded Systems Design

Modeling formalisms for embedded system design have been widely studied, and several reviews and textbooks about models of computation (MoCs) can be found in the literature [START_REF] Lavagno | Models of computation for embedded system design[END_REF][START_REF] Sgroi | Formal models for embedded system design[END_REF][START_REF] Edwards | Design of embedded systems: Formal models, validation, and synthesis[END_REF][START_REF] Vahid | Embedded System Design: A Unified Hardware/Software Introduction[END_REF][START_REF] Gomes | Models of computation for embedded systems[END_REF]. Usage of formal models in embedded system design allows (at least) one of the following [START_REF] Sgroi | Formal models for embedded system design[END_REF]:

• Unambiguously capture functionality of the required system;

• Verification of functional specification correctness with respect to its desired properties;

• Support synthesis onto a specific architecture and communication resources;

• Use different tools based on the same model (supporting communication among teams involved in design, producing, and maintaining the system).

Two basic types of MoCs can be differentiated: process based and state based MoCs [START_REF] Daniel | Embedded System Design: Modeling, Synthesis and Verification[END_REF].

Process-based MoCs describe the system behavior as a set of concurrent processes communicating with each other through message passing channels or shared memory facilities such as:

• Kahn process networks [START_REF] Kahn | The Semantics of a Simple Language for Parallel Programming[END_REF]: process are independent of each other and execute in parallel.

Communication is done through uni-directional message passing channels incorporating buffers, which enable asynchrony;

• Dataflow model, processes are broken down into atomic blocks of execution, called actors, executing once all their inputs are available. On every execution, an actor consumes the required number of tokens on all of its inputs and produces resulting tokens on all of its outputs. In the same way as KPNs, actors are connected into a network using unbounded, uni-directional FIFOs with tokens of arbitrary type. More formally, a dataflow network is a directed graph where nodes are actors and edges are infinite queues. Dataflow networks are deterministic and have the same termination semantics as KPNs. It is a basis for many commercial tools such as LabView [START_REF] Bishop | LabVIEW 8 Student Edition[END_REF] and Simulink [START_REF]MATLAB Simulink Student Version[END_REF];

• Synchronous DataFlow (SDF) [START_REF] Lee | Synchronous data flow: Describing signal processing algorithm for parallel computation[END_REF] is a specialization of dataflow modeling, where production and consumption values on edges are not necessarily the same. Unlike dataflow, states do not influence the number of tokens that are produced and consumed in each firing cycle and these numbers can be specified a priori;

• Process Calculi :

-Communicating Sequential Processes (CSP) [START_REF] Hoare | Communicating sequential processes[END_REF][START_REF] Brookes | A theory of communicating sequential processes[END_REF] allows the description of systems in terms of component processes that operate independently, and interact with each other solely through message-passing communication. CSP uses explicit channels for message passing, whereas actor systems transmit messages to named destination actors;

-Calculus of Communicating Systems (CCS) [START_REF] Milner | A Calculus of Communicating Systems[END_REF]: the fundamental model of interaction is synchronous and symmetric, i.e. the partners act at the same time performing complementary actions;

-Algebra of Communicating Processes (ACP) [START_REF] Bergstra | Process algebra for synchronous communication[END_REF] focus on the algebra of processes, and sought to create an abstract, generalized axiomatic system for processes.

State based models are defined by a set of states and transitions, called state machines. States explicitly represents the memory state of a program and transitions which can be guarded over specific boolean conditions, represents the changes in the system behavior. Finite State Machines (FSM, automata) is one of the basic model for describing various type of application and is usually sequential, i.e it can only be in one state at a time. Two types of FSM exists: Moore type in which the outputs are determined solely by its current state [START_REF] Moore | Gedanken-experiments on sequential machines[END_REF] and Mealy type in which outputs are determined both by its current state and the current inputs.

Several extension of FSM have been proposed:

• Finite State Machine with DataPath (FSMD) introduces a set of variable in order to reduce the number of states;

• Hierarchical and concurrent finite states machines (HCFSM) incorporate notions of hiearchy and concurrency. Hierarchy is defined through the notion of superstates representing an enclosed state machine and communicating through shared variables, events or signals. Statecharts [START_REF] Harel | Statecharts: A visual formalism for complex systems[END_REF] are the most well known formalism;

• Co-Design Finite State Machines (CFSM) [START_REF] Chiodo | A formal specification model for hardware/software codesign[END_REF] connect individual sequentials elements in a global asynchronous network.

Combinations of different models have also been developed such as Program State Machine (PSM) [START_REF] Gajski | Specification and design of embedded systems[END_REF] which can be seen as a combination of KPN and HCFSM. Petri nets [START_REF] Petri | Kommunikation mit Automaten[END_REF] are directed graphs, similar to dataflows, with two types of nodes: places and transitions. Places correspond to the states of the program and transitions are the computational entities. A firing of the transition implies the consumption of tokens in the input places and output tokens in the output places.

The notion of time is extremely important in many of the modeling formalisms for embedded systems. Untimed MoC, like Petri nets, is based on data dependency only and neither a transition or the transfer of a token from one place to another takes a particular amount of time. Using a timed MoC reflects the intention of capturing the timing behavior of a component which could also influence its functional behavior. We can distinguish between continuous-time and discretetime system according to the type of the time variables.

In discrete event MoC, events are sorted by a time stamp stating when they occur and are treated in chronological order. Transaction Level Modeling (TLM) is a discrete-event MoC built on top of SystemC, where modules interchange events with time stamps.

Synchronous models of computation divide the time axis into totally ordered slots and everything inside a slot occurs at the same time. This type of MoC is more suited for programming control and real-time systems. Esterel [START_REF] Berry | The esterel synchronous programming language: Design, semantics, implementation[END_REF], Lustre [START_REF] Halbwachs | The synchronous dataflow programming language lustre[END_REF] and Signal [START_REF] Benveniste | Hybrid Dynamical Systems Theory and the SIGNAL Language[END_REF] are some existing synchronous languages.

Many of the untimed MoC presented previously have also been extended with timing information. One can cite for example, Timed automata [START_REF] Alur | A theory of timed automata[END_REF] , that extend finite automata with clock variables which give timing constraints on the behavior of the system, or Timed Petri Nets [START_REF] Berthomieu | Modeling and verification of time dependent systems using time petri nets[END_REF] where a timed interval is associated with each transition.

Modeling implies also the notion of determinism. Deterministic systems produce one unambiguous output for a given input, but a system may not always react with the same outputs when confronted with the same inputs or inputs may not be precisely defined. For example communication times in distributed systems are hard to predict and may vary due to physical effects or interferences. This leads to non-deterministic models where systems may produce different behaviors. Quantitative properties concerning the different outputs are sometimes captured with stochastic systems. We will discuss non determinism and uncertainty in more detail in the next chapters.

Performance Evaluation

Performance analysis aims to assess and understand some quantitative properties at an early stage of the product development and is as important as functionality. In [START_REF] Marwedel | Embedded system design[END_REF] Marwedel indicates five metrics for the evaluation of the efficiency of an embedded system:

• Power consumption • Code size • Run time efficiency • Weight • Cost
All these metrics can be subject to design requirements of the system, that is appropriate predictions of these characteristics are necessary in early design stage and can be considered objectives of early performance analysis. According to [START_REF] Mohanty | Rapid design space exploration of heterogeneous embedded systems using symbolic search and multi-granular simulation[END_REF], design space exploration is the process of analyzing several implementation alternatives to identify an optimal solution. For efficient system-level design space exploration of complex embedded systems the separation-of-concerns concept has been introduced by [START_REF] Keutzer | System Level Design: Orthogonolization of Concerns and Platform-Based Design[END_REF]. Therefore, Y-chart design methodology [START_REF] Balarin | Hardware-Software Co-Design of Embedded Systems: The Polis Approach[END_REF][START_REF] Kienhuis | A methodology to design programmable embedded systems -the y-chart approach[END_REF], depicted on Fig- 2.6, became a popular basis for early design space exploration.

To perform quantitative performance analysis, application models are mapped onto the architecture model under consideration, whereafter performance of each application-architecture combination can be evaluated. Subsequently, the resulting performance numbers may inspire the designer to improve the architecture, adapt the application or modify its mapping.

Performance is often focus on the analysis of timing aspects e.g. how fast a system can react to events. However power consumption is, in some situation, as important as execution time, and we will focus in this thesis on performance analysis on these two metrics. Very often, the timing behavior of an embedded system can be described by the time interval between a specified pair of events. Depending on the application domain timing properties can be more or less critical. Many embedded systems must meet real time constraints, that is, they must react to events within a specific time interval, called deadline. A real time constraint is called hard if its violation is considered a system failure, and it is called soft otherwise. First of all it is necessary to distinguish between the following terms (taken from [START_REF] Thiele | Performance analysis of distributed embedded systems[END_REF]):

• Worst case and best case. The worst case and the best case are the maximal and minimal time interval between the arrival and termination events under all admissible system and environment states. The execution time may vary largely, owing to different input data and interference between concurrent system activities.

• Upper and lower bounds. Upper and lower bounds are quantities that bound the worst-and best-case behavior. These quantities are usually computed offline, that is, not during the runtime of the system.

• Statistical measures. Instead of computing bounds on the worst-and best-case behavior, one may also determine a statistical characterization of the runtime behavior of the system, for example, distributions, expected values, variances, and quantiles.

In hard real time systems, performance is hardwired into correctness, for example requiring that some deadline is never violated. For such systems we are more interested in upper bounds and worst case behavior whereas in soft real time system lower and upper-bounds represent very extreme cases and a more quantitative estimation will be more useful.

Performance evaluation is a key challenge in the analysis of MPSoC and can be broadly divided in two main approaches: formal methods and simulation-based approaches. Formal verification is the process of checking whether some properties are satisfied by using mathematical proofs. There are different type of formal verification:

• Model checking [START_REF] Clarke | Model Checking[END_REF]: given an abstract model and a property to verify, typically expressed as a temporal logic formula, a model checker performs exhaustive exploration of the set of all possible states.

• Theorem proving: the system is modeled as a set of mathematical definitions in some formal mathematical logic. Properties of the system are derived as theorems that follow from these definitions by using standard results in mathematical logic [START_REF] Paulson | The foundation of a generic theorem prover[END_REF].

• Equivalence checking: formulas for both the specification and the implementation are reduced to some canonical form (if one exists) by applying mathematical transformations. If their canonical forms are identical, then the specification and the implementation are said to be equivalent.

Simulation consists in exploring a model interactively or randomly, possibly using heuristics for choosing the visiting states. It is a technique of partial validation, i.e if no error is detected, this method increase the confidence in program correctness but can never ensure that all properties are satisfied. Discrete event simulation [START_REF] Cassandras | Introduction to Discrete Event Systems[END_REF][START_REF] Leupers | Processor and System-on-Chip Simulation[END_REF] is widely used for evaluating performance of MPSoCs.

Timing Analysis

Timing requirements have been widely studied in the real time community where schedulability analysis techniques have been developed such as Rate Monotonic Analysis [START_REF] Liu | Scheduling algorithms for multiprogramming in a hard-realtime environment[END_REF]. Most of these techniques are devoted to single-processor systems but have been extended to distributed systems [START_REF] Tindell | Holistic schedulability analysis for distributed hard real-time systems[END_REF] and more recently for fixed priority multiprocessors scheduling [START_REF] Guan | Fixed-priority multiprocessor scheduling with liu and layland's utilization bound[END_REF].

In the domain of communication networks, abstractions have been developed to model flow of data through a network. In particular Network Calculus [START_REF] Boudec | Network calculus: a theory of deterministic queuing systems for the internet[END_REF] provides the means to deterministically reason about timing properties of data flows in queuing networks, and can be viewed as a deterministic queuing theory. Modular performance analysis [START_REF] Wandeler | System architecture evaluation using modular performance analysis: a case study[END_REF] and Real-Time Calculus [START_REF] Thiele | Real-time calculus for scheduling hard real-time systems[END_REF] extends the concepts of Network Calculus to the domain of real-time embedded systems. Some other model-based solutions for timing design, performance optimization and timing verification are symbolic timing analysis for systems (SymTA/S) [START_REF] Henia | System level performance analysis -the symta/s approach[END_REF] or schedulability analysis provided by the tool TIMES [START_REF] Amnell | Times: A tool for schedulability analysis and code generation of real-time systems[END_REF], which is based on timed automata, a model we will discuss later in detail as it underlies our models.

Power Consumption Evaluation

Accurate power consumption estimation can be done at transistor or gate level, but due to the complexity of working at this level of abstraction, this is very costly. Thus, to accelerate power estimation analysis, many abstract models have been proposed including TLM approaches [START_REF] Rabie Ben Atitallah | An mpsoc performance estimation framework using transaction level modeling[END_REF][START_REF] Seung | A high level power model for network-on-chip (noc) router[END_REF][START_REF] Beltrame | Multi-accuracy power and performance transactionlevel modeling[END_REF][START_REF] Xi | A transaction-level noc simulation platform with architecturelevel dynamic and leakage energy models[END_REF] or algorithmic descriptions [START_REF] César | Exploring noc mapping strategies: An energy and timing aware technique[END_REF][START_REF] Eisley | High-level power analysis for multi-core chips[END_REF][START_REF] Elmiligi | Power optimization for application-specific networks-on-chips: A topology-based approach[END_REF][START_REF] Hu | Energy-aware mapping for tile-based noc architectures under performance constraints[END_REF][START_REF] Koohi | High-level modeling approach for analyzing the effects of traffic models on power and throughput in mesh-based nocs[END_REF] .

Generally, high-level models use a reference design model to retrieve more accurate power estimation with RTL power estimation tools. Nevertheless, simulation time and memory requirement of these tools are considerable, making their use impracticable when exploring large design spaces.

Our Modeling Framework

The models presented in this thesis are much more abstract than those used in the development of the software and hardware in the sense that they do not represent the actual computations but attempt to capture the essential features which are relevant for predicting performance. For the application models we abstract away from the actual lines of code and view an application as a task graph, a collection of high-level procedures, each characterized by its execution cost (number of processor cycles), its precedences (to which tasks it needs to wait and which tasks wait for it to terminate) and the amount of data it sends/receives to/from other tasks.

The modeling of the processing elements is even more abstract compared to their real complexity. The state of a processor at a given instant is characterized by its speed (assuming processors that can switch between voltage/frequency levels), whether it is turned on, and which task is executing on it. The speed of the processor is used to translate the quantity of work of a task into a duration. In addition we use rough model of static and dynamic power consumption for the processors indicating the power per time unit in either of its speeds, in execution and idling. The same high-level modeling style is applied to other architectural components such as interconnect and memory

In this modeling framework, a task is viewed as a simple timed automaton which leaves its active state some time after entering it. The advantages of such abstract models in terms of how hard it is to simulate or analyze them are evident: to advance a clock in a discrete event simulation is orders of magnitude faster than a cycle-accurate simulation of the underlying software/herdware system, and even much faster than simulation at the operational semantics level of C programs. And of course, such models need not wait for the complete hardware and software to be realized. However the question about the relation between such models and any reality should not be ignored, and we phrase it explicitly: Where do the numbers that decorate the model come from?

The answer may vary depending on how developed the system in question is at the time of analysis. If the code is fully written and the architecture fully developed, one may profile the tasks and measure the execution times. In fact, if the systems is fully operational, testing it on the real hardware can be more efficient than any simulation. If a new application is to be deployed on a variant of an existing architecture, numbers can be derived based on a combination of profiling and designers know-how from similar applications. These numbers can be very imprecise and there may also be a large real-life variability among execution times of instances of the same task. To compensate for the imprecision we invoke a very attractive feature of our models, inherited from the tradition of formal verification: unlike "executable" models needed for simulation and for implementation, we use models that are not necessarily deterministic: they may exhibit nondeterminism (or under-determination in the sense of [START_REF] Maler | On under-determined dynamical systems[END_REF]) in power consumption, in size of data items and in task durations as well as in their arrival patterns. The methods applied to handle this non determinism vary from Monte-Carlo simulation where the uncertainty space is randomly sampled to generate statistics, via verification methods that attempt to prove that something such as deadline miss never happens under all possible choices in the uncertainty space, to more sophisticated methods that compute the expected performance of a system.

To recapitulate our approach: we replace overly detailed models at a very low-level of abstraction (some of which might be inexistent at the time of the analysis) by very coarse grained models that compensate for their imprecision by taking the under-determination more seriously and explicitly in the analysis method. It seems that software and especially hardware developers bring to performance analysis too many low-level details (which are indispensable for implementation and functional correctness, though) while investing less effort in modeling the external environment of the system, such as the arrival model of tasks, which can have more effect on the performance than the low-level implementation details. This is understood because the external environment is not part of the system that they are responsible for developing and whose detailed implementation model cannot be avoided.

Since our approach originates historically from the tradition of formal verification it is worth making the premises of verification explicit in order to assess both its potential contribution and its current inadequacy for performance evaluation. Algorithmic formal verification is concerned with proving functional correctness of systems such as communication protocols and digital hardware. This is often done on models that abstract away from data and focus on control (synchronization).

However, functional correctness in the strict sense often used in verification is not a necessary nor sufficient condition for the usefulness of a system. A correct system with an extremely slow response is not likely be ever used, while systems that work well most of the time are all around us. To apply the insights of formal verification to system design beyond the very narrow context in which it is currently used, one should rethink some the following premises of the field:

1. System models, at least traditionally, are qualitative/logical without quantitative information;

2. The questions posed to the verification tool are of a qualitative yes/no nature: is the system correct or not;

3. There is an implicit universal quantification over the possible behaviors of the system: a system is correct if all its behaviors do not violate the specifications.

The first premise is relaxed by models of automata augmented with numerical variables are used extensively in software verification as well as in hybrid systems. Timed automata [START_REF] Alur | A theory of timed automata[END_REF], the model most relevant to the present thesis, have been invented to model delays and execution times in a quantitative way. Relaxing the second premise has been promoted as quantitative analysis/synthesis [START_REF] Cerný | From boolean to quantitative synthesis[END_REF][START_REF] Bloem | Better quality in synthesis through quantitative objectives[END_REF] and it consists of decorating states and transitions with numerical costs and tracking their evolution along system behaviors. Such costs typically admit a simpler dynamics than more general numerical variables in programs or hybrid systems. For example, the model of linearlypriced timed automata [START_REF] Bouyer | Quantitative analysis of real-time systems using priced timed automata[END_REF][START_REF] Kim Guldstrand Larsen | As cheap as possible: Efficient cost-optimal reachability for priced timed automata[END_REF], which are timed automata augmented with costs that can grow at different rates at different states, is simpler to analyze than other hybrid systems with constant slopes [START_REF] Kesten | Integration graphs: A class of decidable hybrid systems[END_REF][START_REF] Kempf | Performance evaluation of schedulers in a probabilistic setting[END_REF][START_REF] Asarin | Reachability analysis of dynamical systems having piecewise-constant derivatives[END_REF] because the cost variables are passive observers of the dynamics. The relaxation of universal quantification is what underlies statistical model checking [START_REF] Håkan | Probabilistic verification of discrete event systems using acceptance sampling[END_REF] [62] [START_REF] David | Statistical model checking for networks of priced timed automata[END_REF] and can be viewed as a compromise between the rigor of formal verification and the scalability constraints for real systems. We demonstrate in this thesis that a combination of all these relaxations has a great potential in solving a central problem related to the multi-core revolution: how to evaluate and optimize the performance of application programs on such execution platforms. Functional correctness and good performance are complementary and sometimes conflicting evaluation criteria. In hard real-time systems, performance is hardwired into correctness: a feedback function of a controller should be computed between every two consecutive sensor readings which puts a deadline constraint on its computation time. Using a timed model of the software/hardware architecture, which represents the execution times of the tasks as well as the scheduling policy, one can verify that such a deadline is never missed. In certain simple situations studied extensively by the real-time community [START_REF] Buttazzo | Hard Real-time Computing Systems: Predictable Scheduling Algorithms And Applications[END_REF]142,[START_REF] Kopetz | Real-Time Systems: Design Principles for Distributed Embedded Applications[END_REF] one can do the calculation [START_REF] Liu | Scheduling algorithms for multiprogramming in a hard-realtime environment[END_REF] without invoking an explicit dynamic "executable" model at all. For embedded systems where the real-time constraints are softer the system is expected to give a best effort performance depending on the system load and resource availability. A typical example would be video streaming where a good trade-off between response time and image quality is sought. For such systems, the actual response time is a performance measure of the system, together with additional criteria such as system price or power consumption. Unlike what is common in verification, the quantitative measures are not Booleanized via predicates/constraints into a yes/no answer but remain quantitative and can be used to compare the relative performance of different designs.

Unlike safety-critical verification, soft systems are not evaluated according to their worst-case behavior but in a more probabilistic fashion. The traditional verification approach to the problem of performance evaluation based on "classical" timed automata technology [START_REF] Yovine | Kronos: A verification tool for real-time systems[END_REF][START_REF] Edwards | The semantics and execution of a synchronous block-diagram language[END_REF][START_REF] Bozga | If-2.0: A validation environment for component-based real-time systems[END_REF][START_REF] Kim Guldstrand Larsen | Uppaal in a nutshell[END_REF][START_REF] Wang | Efficient verification of timed automata with BDD-like data structures[END_REF][START_REF] Beyer | Rabbit: A tool for BDD-based verification of real-time systems[END_REF][START_REF] Amnell | Times: A tool for schedulability analysis and code generation of real-time systems[END_REF] is exhaustive: it can compute performance measures such as termination time and other costs for all possible values of the uncertainty space, thus compute lower-and upper-bounds on termination time. For soft real-time systems this is, at the same time, too much and too little. The lower and upper-bounds represent very extreme cases which are realized only when all the tasks take their extremal duration values.

Under very reasonable assumptions these extreme values are less likely than termination times that admit many realizations (as 7 is more likely than 12 in dice). In contrast with the exhaustive approach, in Monte-Carlo simulation the uncertainty space is finitely sampled according to some distribution and each sampling point induces a single deterministic behavior whose performance is evaluated by (cheap) simulation. Such an approach is weaker than formal verification because it does not cover all behaviors: it can, at most, put bounds on the probability of error or a deadline miss. On the other hand it is stronger as it can give an estimation of the distribution and expected value of the termination times, which can be much more useful for this type of applications than the very conservative bounds computed by the exhaustive approach.

Related tools

Timed automata are a common and theoretically well-founded formalism for real-time systems. Reachability analysis of timed automata has been implemented in several tools, including KRONOS [START_REF] Daws | The tool KRONOS[END_REF], UPPAAL [START_REF] Kim Guldstrand Larsen | Uppaal in a nutshell[END_REF], IF [START_REF] Bozga | If-2.0: A validation environment for component-based real-time systems[END_REF] or RABBIT [START_REF] Beyer | Rabbit: A tool for BDD-based verification of real-time systems[END_REF]. Literature relates many tools for design-space exploration, based on timed automata or other formalisms. We present in the sequel some of them, close to our work. TIMES [START_REF] Amnell | Times: A tool for schedulability analysis and code generation of real-time systems[END_REF] It is a tool suite designed mainly for symbolic schedulability analysis and synthesis of executable code with predictable behaviours for real-time systems. Given a system design model consisting of a set of application tasks whose executions may be required to meet mixed timing, precedence, and resource constraints, a network of timed automata describing the task arrival patterns and a preemptive or non-preemptive scheduling policy, Times will generate a scheduler, and calculate the worst case response times for the tasks. The design model may be further validated using the UPPAAL timed model checker.

PTOLEMY [START_REF] Buck | Ptolemy: A framework for simulating and prototyping heterogenous systems[END_REF] The Ptolemy project studies heterogeneous modeling, simulation and design of concurrent systems with a focus on systems that mix computationnal domains [START_REF] Eker | Taming heterogeneity -the ptolemy approach[END_REF] It uses tokens as the underlaying communication mechanism and controllers regulate how actors fire and how tokens are sent between each actors. Actors are software components that execute concurrently and communicate through messages sent via interconnected ports. A model is a hierarchical interconnection of actors. The semantics of a model is not determined by the framework, but rather by a software component in the model called a director, which implements a model of computation including process networks, discrete-events, dataflow, synchronous/reactive, rendezvous-based models, 3-D visualization, and continuous-time models. Each level of the hierarchy in a model can have its own director, and distinct directors can be composed hierarchically. A major emphasis of the project has been on understanding the heterogeneous combinations of models of computation realized by these directors. Directors can be combined hierarchically with state machines to make modal models [START_REF] Lee | Finite state machines and modal models in ptolemy ii[END_REF]. For example, a hierarchical combination of continuous-time models with state machines yields hybrid systems [START_REF] Lee | Operational semantics of hybrid systems[END_REF].

OCTOPUS [START_REF] Basten | Model-driven designspace exploration for embedded systems: the octopus toolset[END_REF] The octopus toolset supports model-driven design-space exploration based on high level modeling with a clear separation of application, platform and mapping. It provides formal analysis of func-tional correctness and performance and semi-automatic exploration of alternatives and synthesis of optimized designs. Analysis process works with different type of models:

• Timed automata model checking using UPPAAL [START_REF] Kim Guldstrand Larsen | Uppaal in a nutshell[END_REF] • Petri nets simulation using CPNTools [START_REF] Vinter Ratzer | Cpn tools for editing, simulating, and analysing coloured petri nets[END_REF] • Synchronous dataflow for trade-off analysis using SDF3 [START_REF] Stuijk | SDF 3 : SDF for free[END_REF] HOPES [START_REF] Ha | Model-based programming environment of embedded software for mpsoc[END_REF] It is a model based framework for MPSoC software development. The application model is based on actor-orientation and is described in UML using PeaCE model [START_REF] Ha | Peace: A hardware-software codesign environment for multimedia embedded systems[END_REF]:

• Process network: specify execution condition of each task and define interaction between them.

• Synchronous piggybacked dataflow [START_REF] Ha | Hardware-software codesign of multimedia embedded systems: the peace[END_REF]: specify signal processing

• Flexible FSM [START_REF] Kim | Static analysis and automatic code synthesis of flexible fsm model[END_REF]: specify control tasks.

The hardware platform is separately specified in a block diagram with a set of architectures and constraints parameters described in an xml-style. Application is manually partitioned into the abstract PEs that compose the hardware platform.

SESAME (Simulation of Embedded System Architectures for Multilevel Exploration ) [START_REF] Pimentel | A systematic approach to exploring embedded system architectures at multiple abstraction levels[END_REF] It is a modeling and simulation environment for system-level design based on the Y-chart design approach [START_REF] Kienhuis | A methodology to design programmable embedded systems -the y-chart approach[END_REF] which allows application and architecture to be modeled separately. The application model can be mapped onto the platform model and both are co-simulated via trace-driven simulation [START_REF] Pimentel | Calibration of abstract performance models for system-level design space exploration[END_REF].

BIP (Behavior, Interaction, Priority ) [START_REF] Basu | Modeling heterogeneous real-time components in bip[END_REF] It is a component framework intended for rigorous system design. BIP allows the construction of composite hierarchically structured systems from atomic components characterized by their behavior and their interface. Components are composed by layered application of interactions and of priorities. Interactions express synchronization constraints between actions of the composed components while priorities are used to filter amongst possible interactions and to steer system evolution so as to meet performance requirements e.g. to express scheduling policies. Interactions are described in BIP as the combination of two types of protocols: rendez-vous, to express strong symmetric synchronization and broadcast, to express triggered asymmetric synchronization. BIP has a rigorous operational semantics which has been implemented by specific execution engines for centralized, distributed and real-time execution. BIP is used as a unifying semantic model in a rigorous system design flow [START_REF] Basu | Rigorous component-based system design using the BIP framework[END_REF]. Rigor is ensured by two kinds of tools: verification tools such as D-Finder [START_REF] Bensalem | D-finder: A tool for compositional deadlock detection and verification[END_REF] for checking safety properties (and deadlock-freedom in particular) and source-to-source transformers [START_REF] Bozga | Source-to-source architecture transformation for performance optimization in BIP[END_REF], [START_REF] Bonakdarpour | A framework for automated distributed implementation of component-based models[END_REF] that allow progressive refinement of (purely functional) application software towards platform-dependent implementations.

Chapter 3

Timed automata

In order to talk about systems behavior in a formal manner, it is necessary to represent them as some kind of mathematical structure. The simplest way to represent behavior is by means of automata or labelled transition system. These are simply graphs containing nodes and directed, labelled edges. Nodes represent the possible states of the system and edges (or transitions) represent activities as moves between two nodes.

In [START_REF] D'argenio | Modest -a modelling and description language for stochastic timed systems[END_REF] authors have identified a handful of semantic concepts which are well-established in the context of computer-aided verification and modelling formalisms for discrete event systems:

• Action nondeterminism: From a given state several transitions may exist.

• Probabilistic branching: From a given state several transitions may exists and the choice is based on some probability distribution.

• Clocks: A way to represent real time constraints and to specify the dynamics of a model in relation to a physical, quantitive notion of time.

• Delay nondeterminism: allows one to leave the precise timing of events under specified.

• Random variables: give quantitative information about the likelihood of a certain event to happen within a given time frame.

Working with high level models, implies taking into account uncertainty in order to compensate for the lack of precision. Non-determinism can be modeled in many ways and labeled transition systems possess only action non-determinism. Other formalisms associate some kind of quantitative informations with action non-determinism.

Probabilistic automata have been used [START_REF] Segala | Modeling and verification of randomized distributed real-time systems[END_REF][START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF][START_REF] Segala | A compositional trace-based semantics for probabilistic automata[END_REF] for the purpose of modeling and analyzing asynchronous, concurrent systems with discrete probabilistic choice in a formal and precise way. Basically, a probabilistic automaton is a labeled transition system where the target of a transition is a probabilistic choice over several next states. Stochastic processes [START_REF] Doob | Stochastic Processes[END_REF] is another formalism which is often used to represent the evolution of some random value, or system, over time. This formalism will be introduced in the next chapters.

In the present chapter we are interested in timing uncertainty. Timed automata [START_REF] Alur | A theory of timed automata[END_REF] provide a theory for modeling and verification of real time systems. They provide the ability to constraint the execution of a transition to occur anywhere within a time interval. Timed automata introduce a dense non-determinism which is a very useful modeling feature when we have uncertain information about process durations. Other formalisms with the same purpose include timed Petri Nets [START_REF] Berthomieu | Modeling and verification of time dependent systems using time petri nets[END_REF], timed process algebra [START_REF] Reed | A timed model for communicating sequential processes[END_REF][START_REF] Yi | Ccs + time = an interleaving model for real time systems[END_REF][START_REF] Nicollin | The algebra of timed processes, atp: Theory and application[END_REF] and real time logics [START_REF] Alur | A really temporal logic[END_REF][START_REF] Zhou Chaochen | Duration calculus, a logical approach to real-time systems[END_REF].

We will present next, the timed automaton formalism, which will be used as a basis for our modeling framework presented in chapter 6.

Clocks, time constraints, zones

We use Z and R to denote, respectively the integer and real numbers, while N and R+ will stand for their respective non-negative restrictions. We will use R+ as the time domain on which clock variables range. We use R ⊥ to denote R+∪ ⊥ were ⊥ is a special symbol meaning inactive or irrelevant. We extend the addition operation to R ⊥ by letting ⊥ +d =⊥.

Clocks and Valuations

Let C = {c 1 , ..., c n } be a finite set of variables called clocks, each ranging over R ⊥ . A clock valuation is a function v : C → R ⊥ assigning to each clock c ∈ C its value v(c). The set of possible valuations of C is then R n ⊥ . A clock c is said to be active in valuation v iff v(c) =⊥, otherwise it is inactive. In timed automata, clock valuations change due to two types of activities: time progress which happens inside a discrete state and clock assignment which take place during discrete transitions:

Time progress

Let d be a non-negative real. We say that clock valuation v is the result of applying d-timeprogress to clock valuation v, denoted by v = v + d, if for every clock c, v (c) = v(c) + d. Note that by the definition of addition on R ⊥ , all the clocks inactive in v do not change their value while all the other clocks advance uniformly.

Clocks assignment

A clock assignment is a function γ : R ⊥ → R ⊥ indicating a transformation of clock values which occurs during a transition. v = γ(v) denotes the fact that v is the result of applying assignment γ to clock valuation v. The type of assignments that we allow in the definition of timed automata is restricted to compositions of one or more of the following basic assignments:

• Resetting to zero: c i = 0 • Deactivation of a clock: c i =⊥ • Clock copying: c i = c j

Clock constraints

Clock constraints are used to express the influence of clock values on the discrete dynamics (invariants and transition guards). We restrict ourselves to a family of constraints that we denote by Ψ C , defined by the following grammar:

ψ ::= true | c i ≺ k | c i -c j ≺ k | ψ ∧ ψ
where c i , c j ∈ C, k ∈ N and ≺∈ {<, ≤, =, ≥, >}.

Timed zones

Clock constraints define naturally the set of clock valuations that satisfy them. These are subsets of R n + . Every constraint ψ ∈ Ψ C is a conjunction of atomic constraints. Knowing that the set of valuations satisfying an atomic constraint defines a half-space, every constraint ψ ∈ Ψ C will define a convex polyhedron which is the intersection of those half-spaces. Z ψ denote this polyhedron and it is called the timed zone associated with ψ. The set of all the zones defined on C will be denoted Z C . Since the half-spaces are either orthogonal (c i ≺ k) or diagonal (c i -c j ≺ k) with k ∈ N, the vertices of these polyhedra are integer points and there is a finite number of zones in any bounded subset of R n . The most important property of zones is that they can be canonically represented as matrices i.e. DBMs (Difference Bound Matrices) [START_REF] Dill | Timing assumptions and verification of finite-state concurrent systems[END_REF].

In the following we will define some useful operations on zones that will be used throughout this chapter. Let C ⊆ C be a set of clocks, and let Z 1 , Z 2 ∈ Z C be two timed zones defined on C, then:

Z 1 ∩ Z 2 is the intersection of two zones Z 1 and Z 2 , which is a zone (fig3.1-(b)) Z 1 Z 2 is the convex hull of two zones Z 1 and Z 2 defined as Z 1 Z 2 = min{Z ∈ Z C | (Z 1 ⊆ Z) ∧ (Z 2 ⊆ Z)}
Z = {v ∈ V C | ∃d ≥ 0, v -d ∈ Z} Z /C
is the projection of a zone Z on a clock subset C ⊆ C: All these operations can be computed efficiently on a DBM representation of timed zones. More details can be found, for example, in [START_REF] Yovine | Methodes et outils pour la verification symbolique de systemes temporises[END_REF].

Z /C = {v /C | v ∈ Z}

Timed Automata: Syntax and Semantics

Timed automata have been introduced in [START_REF] Alur | Automata for modeling real-time systems[END_REF][START_REF] Alur | A theory of timed automata[END_REF] as finite state Büchi automata (a variation of finite automaton that runs on infinite, rather than finite, inputs) extended with a set of real valued variables modeling clocks. Constraints on the clock variables are used to restrict the behavior of an automaton and Büchi accepting conditions are used to enforce progress properties. A simplified version, namely Timed Safety Automata, has been later introduced in [START_REF] Henzinger | Symbolic model checking for real-time systems[END_REF] to specify progress properties using local invariant conditions. A timed automaton is presented as a discrete structure which is essentially a finite automaton (i.e a graph containing a finite set of nodes or locations and a finite set of labeled edges) extended with clock variables. Locations are supposed to capture all information about the current status of the system, except for timing information. Edges represents events or transitions which change the discrete state of the system. Time progress takes place inside the discrete states and is not expressed explicitly in this structure. Actually, time passage is recorded using clocks. All clocks of the system increase synchronously at the same rate. These clocks can be set to zero, or deactivated when a transition is taken.

Clocks constraints are used to restrict the behavior of the automaton by forcing it to leave a state or forbidding it from taking a certain transition. In [START_REF] Sifakis | Compositional specification of timed systems (extended abstract)[END_REF][START_REF] Bornot | Modeling urgency in timed systems[END_REF] these constraints are associated with the transitions, while in [START_REF] Henzinger | Symbolic model checking for real-time systems[END_REF] they are divided between states and transition. Constraints on states denote staying conditions (called invariant). The automaton may stay in a state (while the active clocks are progressing ) as long as the staying condition holds, otherwise it has to leave the state via one of the enabled transitions. Constraints on transitions are called guards, and a transition can be taken only if its guard constraints are satisfied. Definition 3.2.1. (Timed automaton) A timed automaton is a tuple A = (Q, q 0 , C, Σ, I, ∆) where Q is a finite set of discrete states, q 0 ∈ Q is the initial state, C is a finite set of clocks and Σ is a finite set of labels. I ∈ Q → Ψ C is a function associating a staying condition (invariant) with every state q. The automaton is permitted to stay at q only as long as the clock constraint I q is satisfied.

∆ ⊆ Q × Ψ C × Σ × Γ C × Q is the
transition consisting of elements of the form e = (q, g, a, γ, q ) where: q, q ∈ Q are, respectively, the source and the target of the transition g ∈ Ψ C is an enabling condition called the transition guard.It restricts the execution of the transition to clock valuations that satisfy it. a ∈ Σ is the transition label, γ ∈ Γ C is a clock assignment function which takes place during a transition.

We assume, without loss of generality, that from every state q there is at most one transition labeled by a for every a ∈ Σ.

Parallel Composition of Timed Automata

A timed automaton is often considered to be an element in a network of components running in parallel and communicating with each other. The global behavior of such a network is captured by the global timed automaton, called the product. There are many variations of composition depending mainly on the interaction mechanisms through which the automata influence each other. At this point we use a definition based on a distributed alphabet [START_REF] Volker | The Book of Traces[END_REF] where each component A i has its alphabet Σ i . The alphabets of the components may have non-empty intersections and any global transition labeled by a must involve a local a-transition in every automaton A i such that a ∈ Σ i . Independent local transitions (transitions with different labels) enabled at the same global state can be executed in any order (interleaving). Definition 3.2.2. (Parallel composition of timed automata)

Let N = {A i = (Q i , q i 0 , C i , Σ i , I i , ∆ i ) | i ∈ {1, .
., n}} be a network of timed automata. We assume the sets of clocks of each pair of automata to be disjoint and denote by J(a) the indices i such that a ∈ Σ i . The composition of these automata, denoted by A 1 . . . A n is a timed automaton A = (Q, q 0 , C, Σ, I, ∆) where Q = Q 1 × . . . × Q n is the set of global discrete states of the form q = (q 1 , . . . , q n ), q 0 = (q 1 0 , . . . , q n 0 ) is the initial state, C = n i=1 C i is the global set of clocks, Σ = n i=1 Σ i is the global alphabet and I is the global invariant I(q) = i∈{1,...,n} I i (q i ). The global transition relation ∆ consists of tuples of the form ((q 1 , . . . , q n ), g, a, γ, (q 1 , . . . , q n )) such that:

• ∀i / ∈ J(a), q i = q i • ∀i ∈ J(a), (q i , g i , a, γ i , q i ) ∈ ∆ i • g = i∈J(a) g i • γ = • i∈J(a) γ i
Steps Timed automata define infinite transition systems whose states are configurations of the form (q, v) consisting of a discrete state q and a clock valuation v. The initial configuration is s 0 = (q 0 , ⊥) with all clocks inactive and the transitions are either discrete transitions of the automaton or timepassage transitions. This is formalized by the notion of a step.

Definition 3.2.3. (Steps) A step of a timed automaton A is one of the following :

• A discrete step: (q, v) -→ a (q , v ), for some transition (q, g, a, γ, q ) ∈ ∆ such that v |= g and v = γ(v)

• A time step:(q, v) -→ d (q , v + d) for some d ∈ R + such that v + d satisfies I(q)
Note that the concatenation of two time steps is a time step:

(q, v) -→ d 1 (q, v + d 1 ) -→ d 2 (q, v + d 1 + d 2 ) ≡ (q, v) -→ d 1 +d 2 (q, v + d 1 + d 2 )
Conversely, due to the dense nature of the real numbers, a time step can be split into any number of smaller time steps. A compound step is a discrete step followed by a time step (possibly of zero duration):

(q, v) -→ a,d (q , v + d) ≡ (q, v) -→ a (q , v ) -→ d (q , v + d)
A run of the automaton A starting from a configuration (q, v) is a finite sequence of compound steps (possibly starting by a pure time step). These definitions apply to products as well. Note that a global time step in a global state q = (q 1 , . . . , q n ) is just a local (and uniform) time step for each component A i . The global invariant requires that all local invariants hold at v + d. On the other hand a global discrete step labeled by a is a local discrete step for all components A i such that a ∈ Σ i .

Reachability Analysis

Given timed automata models we would like to verify them, that is, to see what the possible runs of a given automaton are, and whether they satisfy a given property. The enumeration of possible runs is done in a set-based fashion, computing in one step all the successors of a set of configurations by an arbitrary passage of time and by transitions. Verification based on timed automaton can be done in different manners:

• Reachability analysis: does there exists a run of A which ends in some specific state?

• Verification of temporal timed logic: does the timed automaton A satisfies a temporal logic property ϕ ?

• Language inclusion, simulation: can A 1 produce all behaviors that A 2 does?

• Equivalence checking, timed bisimulation of timed automata: are two automaton A 1 , A 2 equivalent or bisimilar?

In the context of this thesis, timed automata are used as the basis modeling formalism and we use only reachability analysis to check whether some error state is reachable or not. All the property that we use are bounded-horizon timed properties that can be reduced to safety reachability on the composition of the system and the property monitor. We will recall next how reachability analysis works.

The original decidability proof for verification of timed automata [START_REF] Alur | Automata for modeling real-time systems[END_REF] was based on partitioning the state space into a finite number of equivalence classes called regions. Regions are the "atomic" zones from which all other zones can be constructed. Two configurations (q, v) and (q, v ) are region-equivalent if for every transition guard g, v |= g iff v |= g, and if by letting time pass they reach the same region. Hence for every sequence of regions visited by a run from (q, v) there is a run from (q, v ) visiting the same sequence. The timed automaton can thus be reduced to a finite automaton whose states are regions with discrete transitions and special transitions that correspond to the passage of time. Region equivalence is guaranteed to capture all the qualitative behaviors of any automaton, but its force is also its weakness because the large number of regions renders this approach impractical.

The most popular approach is on-the-fly forward search based on zones. This approach has the following advantages:

• It does not explore the parts of the state space which are not reachable from the initial state;

• It does not refine zones beyond what is necessary and will typically result in a number of generated zones much smaller than the number of regions;

• It uses an efficient data structure, the DBM, to store and manipulate zones.

The principle of symbolic reachability computation for discrete systems is to take a representation of a set P of states reachable after k steps, and compute from it the set succ(P ) of its successors by all transitions, that is, the set

succ(P ) = q∈P a∈Σ {succ a (q)}
The basic element in this computation is an object consisting of one discrete state and a set of clock valuations. Successors by different transitions are treated separately and enumeratively, while the symbolic treatement is reserved for time passage and clocks valuations.

Definition 3.3.1. A symbolic state of a timed automaton A = (Q, q 0 , C, Σ, I, ∆) is a pair (q, Z)
with q ∈ Q a discrete state and Z a zone.

Symbolic states are closed under the following operations:

• The time successor of a symbolic state (q, Z) is the symbolic state (q, Z ) where Z is the set of clock valuations reachable from Z by letting time progress without violating the staying condition I(q):

post t (q, Z) = {(q, v + d)|(v ∈ Z) ∧ (d ≥ 0) ∧ ((v + d) |= I(q))} = (q, (Z ∩ I(q)))
We say that (q, Z) is time-closed if (q, Z) = post t (q, Z).

• Let (q, g, a, γ, q ) ∈ ∆ be a transition. The a-transition successor of a symbolic state (q, Z) is the set of configurations reached by taking this transition. Only clock valuations of Z that satisfy the guard g are concerned with this transition. These clock valuations will be transformed according to the assignment function σ while taking this transition:

post a (q, Z) = {(q , v )|∃v ∈ Z, v |= g ∧ v = γ(v)} = (q , (γ(Z ∧ g)))
• The a-successor of a symbolic state (q, Z) is the set of configurations reached from (q, Z) by an a-transition followed by passage of time:

succ a (q, Z) = post t (post a (q, Z)) = (q , (γ(Z ∧ g)) ∩ I(q ))
Proposition 3.3.1. Let (q , Z ) = succ a (q, Z) for a transition (q, g, a, γ, q ). A configuration (q , v ) belongs to (q , Z ) if and only if it is the endpoint of a compound step

(q, v) -→ a,d (q , v )
for some (q, v) ∈ (q, Z) and some d ≥ 0

Equipped with these operators under which the set of symbolic states is closed, we can now introduce the forward reachability algorithm for timed automata which computes this way all the runs of A. Algorithm-1 presents a breadth-first version of reachability computation but other exploration orders are possible. The algorithm terminates because there are finitely many zones in any bounded subset of R n ⊥ .

Algorithm 1 Forward reachability algorithm (breadth first).

Explored ← ∅ New ← ∅ Waiting ← {(q 0 , ⊥)} while Waiting = ∅ do for all (q, Z) ∈ Waiting do for all (q, g, a, γ, q ) ∈ ∆ do New ← New ∪succ a (q, Z) end for Explored ← Explored ∪(q, Z) end for Waiting ← New \ Explored New ← ∅ end while return Explored

Authors in [START_REF] Daws | Reducing the number of clock variables of timed automata[END_REF] introduce the notion of clock activity in order to reduce the number of clocks and the complexity of timed verification. A clock is said to be active at some discrete state when its value is relevant for the future evolution of the system, for example, when the clock appears in the state invariant or in a guard of a transition outgoing from the state. The work of [START_REF] Daws | Reducing the number of clock variables of timed automata[END_REF] had two major parts. The first was the (approximate) detection of such clock inactivity by performing a syntactic data-flow analysis of the automaton. Then this information was used to reduce the dimensionality of the clock space, by manipulating in each state polyhedra whose dimension is equal to the number of clocks active in this state. In our modeling framework we express clock deactivation explicitly by assigning a clock value to ⊥ and, in the class of automata that we use for modeling, clock activity tracking is self-evident and we can benefit from the dimensionality reduction without performing the analysis.

Implementation

In the context of this thesis, timed automata models presented thereafter are defined using the IF language [START_REF] Bozga | If-2.0: A validation environment for component-based real-time systems[END_REF]. We give in this section, an overview of this formalism as described in [START_REF] Bozga | The if toolset[END_REF].

IF is a notation for systems of components (called processes), running in parallel and interacting either through shared variables or asynchronous signals. Processes describe sequential behaviors including data transformations, communications and process creation. Furthermore, the behavior of a process may be subject to timing constraints. The number of processes may change over time: they may be created and deleted dynamically. The semantics of a system is the labelled transition system (LTS) obtained by interleaving the behavior of its processes. To enforce scheduling policies, the set of runs of the LTS can be further restricted using dynamic priorities. This representation is expressive enough to describe the basic concepts of modeling and programming languages for distributed real time systems.

Processes

The behavior of a process is described as a timed automaton, extended with data. A process has a unique process identifier (pid) and local memory consisting of variables (including clocks), control states and a queue of pending messages (received and not yet consumed).

A process can move from one control state to another by executing some transition. As for StateCharts [START_REF] Harel | Statecharts: A visual formalism for complex systems[END_REF][START_REF] Harel | Modeling Reactive Systems with Statecharts: The STATEMATE Approach[END_REF], control states can be hierarchically structured to factorize common behaviors. A sequence of transitions between two stable states defines a step. The execution of a step is atomic, meaning that it corresponds to a single transition in the LTS representing the semantics. Notice that several transitions may be enabled at the same time, in which case the choice is made non-deterministically.

Transitions can be either triggered by signals in the input queue or be spontaneous. Transitions can also be guarded by predicates on variables, where a guard is the conjunction of a data guard and a time guard. A transition is enabled in a state if its trigger signal is present and its guard evaluates to true. Signals in the input queue are a priori consumed in a FIFO fashion, but one can specify in transitions which signals should be "saved" in the queue for later use.

Transition bodies are sequential programs consisting of elementary actions (variable or clock assignments, message sending, process creation/destruction, resource requirement/release, etc) and structured using elementary control-flow statements (like if-then-else, while-do, etc). In addition, transition bodies can use external functions/procedures, written in an external programming language (C/C++).

Signals

Signals are typed and can have data parameters. Signals can be addressed directly to a process (using its pid) and/or to a signal route which will deliver it to one or more processes. The destination process stores received signals in a FIFO buffer.

Data

The IF notation provides the predefined basic types bool, integer, real, pid and clock, where clock is used for variables measuring time progress. Structured data types are built using the type constructors enumeration, range, array, record and abstract. Abstract data types can be used for manipulating external types and code.

Composition

The semantics associates with a system a global LTS. At any point of time, its state is defined as the tuple of the states of its living components: the states of a process are the possible evaluations of its attributes (control state, variables and signal queue content). The transitions of the global LTS representing a system are steps of processes and signal deliveries to queues where in any global state there is an outgoing transition for all enabled transitions of all components (interleaving semantics). The formal definition of the semantics can be found in [START_REF] Bozga | IF-2.0: Common Language Operational Semantics[END_REF].

System models may be highly nondeterministic, due to the non-determinism of the environment which is considered as open and to the concurrency between their processes. For the validation of functional properties, leaving this second type of non-determinism non resolved is important in order to verify correctness independently of any particular execution order. Nevertheless, going towards an implementation means resolving a part of this non determinism and choosing an execution order satisfying time related and other nonfunctional constraints.

In IF, such additional restrictions can be enforced by dynamic priorities defined by rules specifying that whenever for two process instances some condition (state predicate) holds, then one has less priority than the other.

Time

The time model of IF is that of timed automata with urgency [START_REF] Bornot | Modeling urgency in timed systems[END_REF]. The execution of a transition is an event defining an instant of state change, whereas time is progressing in states. The progress of time is controlled by urgencies of the enabled transitions. Transitions are annotated with urgency types that are eager, lazy and delayable. Eager transitions prevent time progress. Lazy transition have no impact on the time progress. Delayable transitions are considered lazy unless their guard is disabled by the progress of time, and then they are considered eager.

Example

As an example, consider a multi-threaded server which can handle at most N simultaneous requests. Thus, if possible, for a request message (received from the environment) a thread is created. The server keeps in the thc variable the number of running threads. Threads processes are quite simple: once created, they work during a time interval [l, u], and when finished they send a done message back to the server. A graphical description is shown in Fig- 3

Observers

Observers express in an operational way safety properties of a system by characterizing its acceptable execution sequences. They also provide a simple and flexible mechanism for controlling model generation. They can be used to select parts of the model to explore and to cut off execution paths that are irrelevant with respect to given criteria.

Observers are described as IF processes i.e., as extended timed automata. They differ from IF processes in that they can react synchronously to events and conditions occurring in the observed system. Observers are classified into:

• Pure observers -which express requirements to be checked on the system.

• Cut observers -which in addition to monitoring, guide simulation by selecting execution paths. For example, they are used to restrict the behavior of the environment

• Intrusive observers -which may also alter the system's behavior by sending signals and changing variables.

For monitoring the system state, observers can use primitives for retrieving values of variables, the current state of the processes, the contents of queues, etc. For monitoring actions performed by a system, observers use constructs for retrieving events together with data associated with them. Events are generated whenever the system executes one of the following actions: signal output, signal delivery, signal input, process creation and destruction and informal statements. Observers can also monitor time progress, by using their own clocks or by monitoring the clocks of the system.

In order to express properties, observer states can be marked as ordinary, error or success. Error and success are both terminating states. Reaching a success state (an error state) means satisfaction (violation). Cut observers use a cut action which stops exploration.

Model exploration

IF toolset includes an exploration platform that is a component which has an API providing access to the LTS corresponding to IF description. The interface offers primitives for representing and accessing states and labels as well as basic primitives for traversing LTS enabling implementation of any on-the-fly forward enumerative exploration or validation algorithm. The exploration platform composes all active processes and computes global states and the corresponding system behavior.

Simulation time is handled by a specialized process managing allocation and deallocation of clocks, computing time progress conditions and firing timed transitions. There are two implementations available, one for discrete time and one for dense time. For discrete time, clock values are explicitly represented by integers. Time progress is computed with respect to the next enabled deadline. For dense time, clock valuations are represented using variable-size Difference Bound Matrices (DBMs) as in tools dedicated to timed automata such as KRONOS [START_REF] Yovine | Kronos: A verification tool for real-time systems[END_REF] and UPPAAL [START_REF] Kim Guldstrand Larsen | Uppaal in a nutshell[END_REF].

Chapter 4 Duration Probabilistic Automata: Analysis

The next two chapters constitute the major theoretical contribution of the thesis. They are concerned with a class of stochastic processes, Duration Probabilistic Automata (DPA) [START_REF] Maler | On zone-based analysis of duration probabilistic automata[END_REF], that can model scheduling problems such as job-shop, where task durations are uncertain and distributed uniformly over a bounded interval. DPAs can also be viewed as timed automata where the intervals of temporal uncertainty are interpreted probabilistically, an assumption which is implicit in the Monte-Carlo simulation provided by the tool. In this chapter we develop a piecewise-analytic approach to compute performance measures for such systems, while in the next chapter we study the synthesis of schedulers which are expected-time optimal. Naturally, these new results and computational techniques are first developed on clean abstract models, less loaded with real-life details than the models used in the more applied parts of the thesis.

Scheduling under Stochastic Uncertainty

Scheduling, the allocation of limited reusable resources over time to competing tasks, is a universal activity. It is performed routinely in domains of very different scales in terms of time, space and energy. These include the allocation of airways and runways to flights, allocating machines to different product lines in a factory, and the efficient allocation of computation and communication resources to information-processing tasks. This latter activity is becoming of prime importance in many scales, ranging from world-wide cloud computing, via the realization of multiple distributed control loops, down to mapping and scheduling tasks on multi-core computers. In all such situations one wants to synthesize schedulers which are optimal or good in some sense, or at least to be able to compare the performance of proposed schedulers and choose the better ones. Performance and optimality of such schedulers are typically based on the quantity of work performed over time, which in the case of a finite amount of work can be expressed as termination time. Good schedules are typically associated with intensive, almost idle-free, utilization of critical bottleneck resources.

In a deterministic setting one assumes that everything is known in advance about the demand for work, including the tasks to be executed, their arrival times and the durations for which they occupy resources. In other words, once the scheduling policy itself is determined, the system admits a unique execution scenario (run, realization). Evaluating a scheduler based on this unique run is straightforward -just simulate it -while finding an optimal scheduler for any non-trivial scheduling problem (such as job-shop) is NP-hard or worse. However, determinism is rarely the case in real life and exact duration of tasks, their arrival times and many other features may vary to large extents. Each instance in this uncontrollable space yields a different schedule and the overall evaluation of a scheduler or a scheduling policy, which can be viewed as a strategy in a two-person timed game [START_REF] Bloem | Better quality in synthesis through quantitative objectives[END_REF] with uncertainty viewed as an adversary, should be based on some quantification over all possible behaviors it induces [START_REF] Maler | On optimal and reasonable control in the presence of adversaries[END_REF].

This adversarial time-optimality problem has been tackled in [START_REF] Asarin | As soon as possible: Time optimal control for timed automata[END_REF][START_REF] Abdeddaïm | Scheduling with timed automata[END_REF] using a worst-case approach on models of different types of uncertainty. In [START_REF] Asarin | As soon as possible: Time optimal control for timed automata[END_REF], using, the general model of timed game automaton [START_REF] Asarin | Controller synthesis for timed automata[END_REF] where the adversary is discrete, the following problem was proved to be decidable: synthesize a controller which is worst-case time-optimal in the sense that the maximal (over all possible runs induced by the adversary) time to reach a goal state is minimal. In [START_REF] Abdeddaïm | Scheduling with timed automata[END_REF] the case of job-shop scheduling with uncertain task durations each ranging over a bounded interval was treated. For this problem, worst-case optimality is defined trivially by the optimal solution to a deterministic scheduling problem associated with the worst case where all tasks take their respective maximal duration. One has to define a new notion of optimality (d-future optimal strategies) to make the optimal synthesis problem meaningful, resulting in a synthesis algorithm based on value iteration over sets of clock valuations (zones) which can be seen as an offline version of some kind of model-predictive control.

The use of worst-case reasoning is to some extent a residue of the safety-critical banner under which formal verification has been argued for, but in many (if not most) real-life situations, temporal uncertainty is modeled probabilistically as a distribution over the durations of each task and scheduler quality is measured accordingly, for example by the expected completion time or by its maximum over all but a small fraction of the runs. In this chapter we develop and implement a computational framework in order to evaluate and optimize the performance of such schedulers, modeled by automata similar in structure to those used in [START_REF] Abdeddaïm | Scheduling with timed automata[END_REF] but whose durations are probabilistic. Such automata are sufficiently rich to express stochastic variants of well-known scheduling problems such as job-shop or task-graph.

The study of continuous-time stochastic processes has been going on for many years in other branches of mathematics where simple computational questions like those we pose are not typically asked, as well as in closer domains such as probabilistic verification and performance evaluation [START_REF] Brinksma | Lectures on Formal Methods and Performance Analysis[END_REF][START_REF] Bouyer | From Qualitative to Quantitative Analysis of Timed Systems[END_REF]. A well-studied class of such processes are continuous-time Markov chains (CTMC) where durations are distributed exponentially. Such distributions are memoryless in the sense that time spent waiting for a task to terminate does not influence the distribution on the remaining time. As a result they are easy to compute with and problems such as model-checking against qualitative [5] and quantitative [START_REF] Baier | Model-checking algorithms for continuous-time markov chains[END_REF] temporal properties or optimal controller synthesis for finite-horizon problems [START_REF] Abdeddaïm | Scheduling with timed automata[END_REF] are well understood. This forgetfulness assumption may be realistic and useful for modeling request arrivals in queuing models, but seems inappropriate for modeling the durations of several instances of the same computational task.

In this work we assume task durations to be uniform over a bounded interval, which is a natural "stochastization" of the set-theoretic temporal uncertainty of timed automata. Handling such systems we find ourselves in the realm of the so-called generalized semi-Markov processes (GSMP), a class of continuous-time stochastic processes [START_REF] German | Non-markovian analysis[END_REF][START_REF] Glynn | A GSMP formalism for discrete event systems[END_REF][START_REF] Cassandras | Introduction to Discrete Event Systems[END_REF][START_REF] Kartson | Modelling with Generalized Stochastic Petri Nets[END_REF]. Similar computational studies of GSMPs include [START_REF] Alur | Bounded model checking for GSMP models of stochastic real-time systems[END_REF][START_REF] Bernadsky | Symbolic analysis for GSMP models with one stateful clock[END_REF], [START_REF] Vicario | Using stochastic state classes in quantitative evaluation of dense-time reactive systems[END_REF][START_REF] Carnevali | State-density functions over DBM domains in the analysis of non-Markovian models[END_REF] and [START_REF] Maler | On zone-based analysis of duration probabilistic automata[END_REF]. The former are concerned with verifying temporal properties for some classes of GSMPs and develop techniques to determine whether the probability of a property-violating behavior is zero. The work of [START_REF] Vicario | Using stochastic state classes in quantitative evaluation of dense-time reactive systems[END_REF][START_REF] Carnevali | State-density functions over DBM domains in the analysis of non-Markovian models[END_REF] is concerned with stochastic Petri nets for which a computational framework is developed for propagating densities in the marking graph. This work, as well as [START_REF] Maler | On zone-based analysis of duration probabilistic automata[END_REF] on duration probabilistic automata, use densities on clocks which are auxiliary state variables. At each reachable state and zone in the clock space, the distribution over clock values is maintained and used to compute the distribution after the next transition. In contrast, the approach presented in the this chapter works directly on the space of the duration random variables and does not use clocks explicitly. Similar ideas were developed in [START_REF] Jurdzinski | Calculating probabilities of real-time test cases[END_REF] to compute the probability of test cases in timed systems.

The rest of the chapter is organized as follows. Section 4.2 defines single and parallel processes, their behaviors (timed and qualitative) and presents a useful coordinate transformation between durations and time stamps. Section 4.3 shows how to derive the timing constraints associated with a qualitative behavior when processes execute independently without resource conflicts, and how to compute the volumes of the polytopes they define. Section 4.4 extends the framework to the more interesting case of resource conflicts which are resolved by dynamic scheduling strategies. Finally we present very preliminary experimental results and discuss future directions.

Preliminaries

We consider a composition S = P 1 || • • • ||P n of n sequential stochastic processes, each consisting of a sequence of steps. Each step has a probabilistic duration and cannot start before its predecessor terminates. We consider two execution frameworks:

1. Independent execution: all processes start simultaneously and each process starts a step as soon as its preceding step has terminated, regardless of the state of other processes;

2. Coordinated execution: the initiation of a step is controlled by a scheduler which may hold a step of one process in a waiting state until the termination of a step of another process that uses the same resource.

The second framework will allow us to compare schedulers but we start with the first because it is simpler and does not require knowledge of timed automata. On this simpler model we will develop the basic computational machinery that will allow us to compute the probabilities of different qualitative behaviors, each corresponding to an equivalence class of timed behaviors associated with a particular order in which steps of different processes terminate.

F (y) = y 0 ψ(τ )dτ =    0 if y < a (y -a)/(b -a) if a ≤ y ≤ b 1 if b ≤ y Definition 4.2.

(Process).

A sequential stochastic process is a pair P = (I, Ψ) where I = {I j } j∈K is a sequence of duration intervals and Ψ = {ψ j } j∈K is a matching sequence of densities with ψ j being the uniform density over

I j = [a j , b j ],
indicating the duration of step j.

We consider finite processes with K = {1, . . . , k}. Probabilistically speaking, step durations can be viewed as a finite sequence of independent uniform random variables {y j } j∈K that we denote as vectors y = (y 1 , . . . , y k ) ranging over a duration space

D = I 1 × • • • × I k ⊆ R k with density ψ(y 1 , . . . , y k ) = ψ 1 (y 1 ) • • • ψ k (y k ).
Each point y in the duration space induces a unique behavior of the system written as a time-event sequence of the form

ξ y = y 1 e 1 y 2 e 2 • • • y k e k . ( 4.1)
Time event sequences are alternations between time elapses represented by real numbers and discrete events that take no time. In the case of a single process y j ∈ I j is the duration of step j and e j is the event of terminating that step. The timed language1 associated with the process consists of all the timed behaviors it may generate, namely L = {ξ y : y ∈ D}. The untimed language associated with the process is L, obtained by projecting away durations and retaining events and their order. In the case of a single process L is simply the singleton language {w} where w = e 1 e 2 • • • e k .

q 1 q 2 e k q k e 1 e 2 • • •
Mechanically speaking the process behaviors can be viewed as generated by the automaton of Fig. 4.1 in which being at state q j corresponds to executing step j. Each run of the automaton is associated with a point y in the duration space. Upon entering q j an auxiliary clock variable x is reset to zero and the termination transition labeled by e j is taken exactly when x = y j .

Suppose we want to characterize the probability of a certain subset of L. For example those behaviors in which for every j the actual duration of step j is in some sub-interval I j = [a j , b j ] ⊆ I j . The total probability of these behaviors is simply the volume of the rectangle I 1 × • • • × I k divided by the volume of the whole rectangle D. Probabilities of other subsets of the language can be more interesting but harder to compute. For example, the probability that the whole process terminates before some deadline r is simply the volume of the subset of D satisfying y 1 +• • •+y k < r divided by the volume of D. Our technique is based on computing such volumes for a system of several parallel processes as described in the sequel.

It turns out to be easier to compute volumes after a coordinate transformation from the space of durations to the space of time stamps consisting of vectors t = (t 1 , . . . , t k ) where t j is the absolute occurrence time of event e j , defined as t j = y 1 + y 2 + • • • + y j . A behavior ξ y can thus be written also as a sequence of time-stamped events2 ξ t = (e 1 , t 1 ), (e 2 , t 2 ), . . . , (e k , t k ).

Assuming that all durations admit a positive lower bound a j > 0, all time stamps satisfy precedence constraints of the form t j < t j+1 .

Converting y to t and vice versa is done by the linear transformations t = T y and y = T t where T and T are matrices of the form

T =     1 0 0 0 1 1 0 0 1 1 1 0 1 1 1 1     T =     1 0 0 0 -1 1 0 0 0 -1 1 0 0 0 -1 1    
These matrices are lower triangular (the value of t j cannot depend on a duration y j with j > j) and their diagonal entries are equal to 1. The determinant of a triangular matrix is equal to the product of the diagonal entries which is 1 and hence the transformations are volume preserving. This means that the volume of the duration space D is equal to the volume of the time-stamp space C defined by the constraints

ϕ C : j∈K a j ≤ t j -t j-1 ≤ b j
and computing the volume of any subset C ⊆ C amounts to computing the volume of its T image D ⊆ D. Let us remark that the density of t j is the convolution of the densities ψ 1 , . . . , ψ j and its support is the Minkowski sum of I 1 , . . . , I j . The time-stamp space C and its subsets that we will encounter are defined as conjunctions of inequalities of the form x ≺ c or x -x ≺ c where ≺∈ {<, ≤, =, ≥, >} and c is an integer constant. They define polytopes which are called zones (or timed polyhedra). Zones are used extensively in the analysis of timed automata [START_REF] Henzinger | Symbolic model checking for real-time systems[END_REF][START_REF] Daws | The tool KRONOS[END_REF][START_REF] Kim Guldstrand Larsen | Uppaal in a nutshell[END_REF]. They admit an efficient representation by difference-bound matrices (DBM) [START_REF] Dill | Timing assumptions and verification of finite-state concurrent systems[END_REF] and efficient algorithms based on shortest-path to remove redundant constraints [START_REF] Cormen | Introduction to algorithms[END_REF]. Definition 4.2.3 (Process System). A process system consists of n processes

S = P 1 || • • • ||P n = {(I i , Ψ i )} n i=1
We use notations P i j to refer to step j of process i and

I i j = [a i j , b i j ]
and ψ i j for the respective intervals and densities. To ease notation we assume all processes to have the same number k of steps. The event alphabet of the system is

Σ = {e 1 1 , e 1 2 , . . . , e n k-1 , e n k }
consisting of all the termination events of the steps of the various processes.

A behavior of the system is induced by a point in the global duration space

y = (y 1 1 , y 1 2 , . . . , y n k-1 , y n k ) ∈ D = n i=1 k j=1 I i j ⊂ R nk ,
which can be transformed into a point t in the time-stamp space

t = (t 1 1 , t 1 2 , . . . , t n k-1 , t n k ) ∈ C = T D
where T is the appropriate block diagonal matrix. When all processes start simultaneously, the time stamps are taken from the same global time reference and one can view a global run as merging local runs and sorting the events according to their time stamps, as illustrated in Fig. 4.2. The set of all such global behaviors is denoted by

L = L 1 || • • • ||L n .
All timed behaviors that admit the same order of events are said to exhibit the same qualitative behavior. This can be formalized as an operation among the untimed local languages. Let

L i = {e i 1 e i 2 • • • e i k }
be the untimed language associated with process P i : it consists of the unique qualitative behavior which satisfies the precedence constraints of P i . The potential qualitative behaviors of S constitute the language

L = L 1 || • • • ||L n
which is the shuffle of these languages, that is, the set of sequences consisting of one occurrence of each event in Σ and respecting the local precedence constraints for each process. Mathematically speaking, a qualitative behavior corresponds to a linear order 3 which is consistent with the partial order defined by the union of the precedence relations of all the tasks. Such an order is also known as interleaving in the theory of concurrency (readers can refer to [START_REF] Volker | The Book of Traces[END_REF] or [START_REF] Esparza | Unfoldings -A Partial-Order Approach to Model Checking[END_REF]). 3 and e 2 2 in state (q 1 3 , q 2 2 ) is indicated by the dashed arrows.

We use the term qualitative behavior also for any prefix of a sequence in L. Such a prefix corresponds naturally to an incomplete run where not all processes have finished all their steps. From the standpoint of automata, qualitative behaviors correspond to paths in the transition graph of the global automaton associated with the system which is the (Cartesian) product A = A 1 || • • • ||A n of the automata associated with the individual processes as illustrated in Fig. 4.3. Unfortunately, these extremely important objects are not easy to draw for non-trivial dimensions. Incomplete behaviors correspond to paths not reaching the final state.

In a global state of the form (q 1 j 1 , . . . , q n jn ) each process i is busy executing its step j i and there is a race between the termination transitions. The transition e i j i that will win will be the first to satisfy the condition x i = y i j i . Since x i has been reset to zero at t i j i -1 this condition will be fulfilled at time t i j i -1 + y i j i = t i j i . The outcomes of all these races are completely determined by the value of y, and this determines the qualitative behavior which is exhibited. Had there been no timing constraints on task durations, that is, I i j = [0, ∞), the system would be completely asynchronous and all interleavings would, in principle, be possible. When durations are bounded, some qualitative behaviors may become strictly impossible due to the arithmetics of timing constraints while others will occur at low probability. In the sequel we develop methods for computing these probabilities.

Computing Volumes

The computation of the probability of a qualitative behavior w is performed in two steps. First we associate with it a zone Z w ⊆ C consisting of all instances of t that yield this behavior. Then we integrate over this zone to find its volume.

Let ϕ C be the constraint describing the whole time-stamp space:

ϕ C : i∈N j∈K a i j ≤ t i j -t i j-1 ≤ b i j
with t i 0 = 0 for every i. The zone Z w for the qualitative behavior of Fig. 4.2 can be characterized by adding constraints that specify the particular order of events in w:

ϕ w : ϕ C ∧ t 1 1 < t 2 1 < t 2 2 < t 3 1 < t 2 3 < t 1 2 < t 1 3 < t 3 2 < t 3 3 .
Some of these constraints appear already in ϕ C and some are implied via transitivity by other constraints. After eliminating these redundant constraints one obtains the following description:

ϕ w : ϕ C ∧ (t 1 1 < t 2 1 ) ∧ (t 2 2 < t 3 1 ) ∧ (t 3 2 < t 1 2 ) ∧ (t 1 3 < t 2 3 ) ∧ (t 2 3 < t 3 3 ).
As illustrated in Fig. 4.2, the constraints that remain in ϕ w are the inter-process constraints that are sufficient to characterize w. These constraints can be computed incrementally as we move along the prefix of a qualitative behavior. Let us follow the first two steps. Initially we have the empty word whose associated zone is C and hence its probability is 1. After the occurrence of the first event e 1 1 we know that P 1 1 terminated before P 2 1 and P 3 1 . This leads to the constraints:

ϕ e 1 1 : ϕ C ∧ (t 1 1 < t 2 1 ) ∧ (t 1 1 < t 3 1 ) (4.2)
After this first event we have a competition between e 2 1 , e 3 1 and e 1 2 . The winner of the race is the next event of w, e 2 1 and hence we add the constrains t 2 1 < t 3 1 and t 2 1 < t 1 2 and remove the constraint t 1 1 < t 3 1 which becomes redundant, yielding:

ϕ e 1 1 e 2 1 : ϕ C ∧ (t 1 1 < t 2 1 ) ∧ (t 2 1 < t 3 1 ) ∧ (t 2 1 < t 1 2 ).
In general whenever event e i j occurs, we add a constraint stating that t i j is smaller than the time stamps associated with all the pending events in the other processes. The incremental process is illustrated in Fig. 4.4.

This procedure is probabilistically correct in the following sense. For every w ∈ L the probability of all behaviors having w as a prefix is the relative volume of the corresponding zone Z w , namely, p(w) = |Z w |/|C|. This holds trivially for the empty behavior when there are no constraints. For the inductive step observe that any qualitative behavior of the form w e which extends w has to satisfy ϕ w due to causality as well as additional constraints that guarantee that e is indeed the next event to win the race. The constraints associated with all the extension of w form a partition of Z w and all the probabilistic mass p(w) is split among them, satisfying e p(w e) = p(w). 1 and then for e 1 1 e 2 1 . The constraint t 1 1 < t 3 1 becomes redundant after the second event.

COMPUTING VOLUMES

In [START_REF] Maler | On zone-based analysis of duration probabilistic automata[END_REF] a similar incremental approach that goes from a path/prefix to its successors has been developed using the clock auxiliary variables. The use of clocks required the concept of density transformers to account for the distribution of clock values before and after transitions (see also [START_REF] Bernadsky | Symbolic analysis for GSMP models with one stateful clock[END_REF][START_REF] Alur | Bounded model checking for GSMP models of stochastic real-time systems[END_REF][START_REF] Vicario | Using stochastic state classes in quantitative evaluation of dense-time reactive systems[END_REF][START_REF] Carnevali | State-density functions over DBM domains in the analysis of non-Markovian models[END_REF]). These are not needed in the clock-free approach presented here. Those acquainted with the verification of timed automata using a forward computation of the simulation/reachability graph [START_REF] Daws | The tool KRONOS[END_REF][START_REF] Kim Guldstrand Larsen | Uppaal in a nutshell[END_REF] may notice that for every w the zone Z w in the time-stamp space is empty exactly when its associated clock space zone in the reachability graph becomes empty. This suggests an alternative clock-free analysis algorithm for timed automata which is immediately applicable to acyclic systems but will require more work to be adapted to the cyclic case.

Having labeled qualitative behaviors by constraints we need to compute the volume of the zones. We illustrate this procedure on a concrete example with n = 3 and k = 1, hence [START_REF] Ackland | A single-chip 1.6 billion 16-b mac/s multiprocessor dsp[END_REF][START_REF] Akyildiz | Next generation/dynamic spectrum access/cognitive radio wireless networks: A survey[END_REF], and [a 3 1 , b 3 1 ] = [START_REF] Akyildiz | Next generation/dynamic spectrum access/cognitive radio wireless networks: A survey[END_REF][START_REF] Alur | Bounded model checking for GSMP models of stochastic real-time systems[END_REF]. The constraints associated with all qualitative behaviors where process P 1 wins the first race are

D = C = I 1 1 × I 2 1 × I 3 1 , with concrete values [a 1 1 , b 1 1 ] = [2, 5], [a 2 1 , b 2 1 ] =
ϕ e 1 1 : (2 ≤ t 1 1 ≤ 5) ∧ (3 ≤ t 2 1 ≤ 4) ∧ (4 ≤ t 3 1 ≤ 7) ∧ (t 1 1 < t 2 1 ) ∧ (t 1 1 < t 3 1 ).
We pick an integration order t 3

1 ≺ t 2 1 ≺ t 1 1
, that is, the inside-out order of variable elimination, and rewrite ϕ e 1 1 as

ϕ e 1 1 : (2 ≤ t 1 1 ≤ 5) ∧ (max(3, t 1 1 ) ≤ t 2 1 ≤ 4) ∧ (max(4, t 1 1 ) ≤ t 3 1 ≤ 7)
Then we split I 1 1 into maximal segments where both max(3, t 1 1 ) and max(4, t 1 1 ) are uniform. In our example [START_REF] Abdeddaïm | Scheduling with timed automata[END_REF][START_REF] Alur | Model-checking for probabilistic real-time systems[END_REF] splits into [START_REF] Abdeddaïm | Scheduling with timed automata[END_REF][START_REF] Ackland | A single-chip 1.6 billion 16-b mac/s multiprocessor dsp[END_REF], [START_REF] Ackland | A single-chip 1.6 billion 16-b mac/s multiprocessor dsp[END_REF][START_REF] Akyildiz | Next generation/dynamic spectrum access/cognitive radio wireless networks: A survey[END_REF] and [START_REF] Akyildiz | Next generation/dynamic spectrum access/cognitive radio wireless networks: A survey[END_REF][START_REF] Alur | Model-checking for probabilistic real-time systems[END_REF] and the volume of the set can be written as

+ 5 4 4 t 1 1 7 t 1 1 dt 3 1 dt 2 1 dt 1 1 = 3 + 3 2 + 0 = 9 2
which after dividing by |C| = 9 gives a probability of 1/2 for e 1 1 winning the first race. Figure 4.5 illustrates two possible splits of a 2-dimensional zone into integration domains. The number of case splits and the forms of the integration domains may vary a lot depending on the chosen order. Theorem 1 (Probability of Qualitative Behaviors). Given a system of stochastic sequential processes as in Def. 5.3.1 the probability of any of its qualitative behaviors is computable.

2 x 1 b 2 b 1 a 2 a 1 A C x 2 x 1 b 2 b 1 a 2 a 1 D B E 1 ≺ 2 2 ≺ 1
The global termination time (makespan) of a behavior is Θ = max{t 1 k , . . . , t n k }. For all behaviors that are qualitatively equivalent the maximum is attained by the same variable, namely t i k for any behavior whose last event is e i k . To compute the expected termination time we integrate t i k over Z w and sum up over all w:

E(Θ) = 1 |C| n i=1 w=w e i k Zw t i k .
Before moving to the coordinated execution framework let us mention some useful observations. So far we have treated qualitative behaviors in their finest granularity, taking note of the ordering between any pair of events. In many situations we are interested in sets of qualitative behaviors and their probability can often be computed more efficiently than summing up the probabilities of individual qualitative behaviors.

Suppose we want to characterize the set of all qualitative behaviors that pass through a global state q = (q 1 j 1 , . . . , q n jn ). Let L i j = {e i 1 • • • e i j-1 } be the qualitative behavior of P i that leads to q i j . Then the set of qualitative behaviors that lead to q is

L(q) = L 1 j 1 || • • • ||L n jn .
The constraints that characterize L(q) may forget the specific interleaving, that is, the specific order in which past events have occurred. The only constraints that are relevant are those that guarantee that the entrance of each process into its respective local state preceded the exit of all other processes from their respective states, that is,

ϕ q : ϕ C ∧ n i=1 i =i t i j i -1 < t i j i .
Thus, to compute the expected termination time it suffices to partition the set of qualitative behaviors into n classes according to the identity of the last transition, letting Z i be the zone defined by

ϕ i : ϕ C ∧ i =i t i k < t i k .
Then the expected termination time is

E(Θ) = 1 |C| n i=1 Z i t i k . (4.3)
A similar observation, made in the context of zone-based verification of timed automata, underlies the fact that the union of zones reached by interleavings of the same set of events is convex [START_REF] Zhao | Partial order path technique for checking parallel timed automata[END_REF][START_REF] Lugiez | A partial order semantics approach to the clock explosion problem of timed automata[END_REF][START_REF] Ben-Salah | On interleaving in timed automata[END_REF].

Conflicts and Schedulers

Now we adapt the framework to the case where steps of different processes may be at conflict due to requiring the same resource and hence cannot be executed simultaneously. Naturally, this situation is more intuitively expressed using automata, states and runs. We explain the automatonbased modeling very informally and delegate the formal definitions of DPA to Chapter 5 where they are used for deriving a state-based optimal scheduler. As a running example consider a system of two processes with three steps each, admitting a resource conflict between their respective second steps P 1 2 and P 2 2 . Conflicts are modeled in automata using forbidden states in the global automaton, state (q 1 2 , q 2 2 ) in our example. To be able to prevent the automaton from entering this state 4 we refine the process model so that the initiation of step P i j does not occur automatically upon the termination of step P i j-1 . We thus modify the process automaton shown in Fig. 4.3 by inserting a waiting state qi j between q i j-1 and q i j . The automaton can leave this state only when it receives a start command s i j from a scheduler as illustrated in Fig. 4.6-(a).

As long as the scheduler is not completely specified the system is open or using another terminology, admits both probabilistic and set-theoretic non-determinism. For example in state (q 1 2 , q 2 1 ) process P 1 may either start its second step (q 1 2 , q 2 1 ) → (q 1 2 , q 2 1 ) or wait until step P 2 1 terminates and let P 2 take the resource first (q

1 2 , q 2 1 ) → (q 1 2 , q2 2 ) → (q 1 2 , q 2
2 ). A scheduler resolves this type of non-determinism by telling each process in a waiting state whether to take the resource and proceed to execution or wait until the resource is taken and released by another process. 5Once such a scheduler is defined, the set-theoretic non-determinism is eliminated and the only non-determinism that remains is the one associated with task durations and thus it becomes possible to compute probabilities. To be more precise, probabilities can be computed also for nondeterministic schedulers that make a probabilistic choice, but we do not consider them here.

A scheduler is thus a mechanism which may observe the state of the system and decide whether to grant a resource to a process, possibly based on the level of progress of other processes. The most passive scheduler grants the resource to the first process whose corresponding step becomes enabled. Under such a FIFO scheduling policy it is the result of the race between e 1

1 and e 2 1 which determines the resource granting decision. The automaton obtained by composing the system with such a scheduler is shown in Figure 4.6-(b) where we have chosen to ignore the zero-measure situation when both processes terminate exactly at the same time (alternatively this situation can be handled by assigning an arbitrary priority when this is the case).

More active schedulers interfere with the execution order by imposing additional conditions upon the start transitions. Suppose that the duration of step P 1 3 is much longer than that of P 2 3 hence it would be reasonable to give P 1 2 a priority over P 2 2 even if the latter becomes enabled earlier. This priority can have different degrees of rigidity. A strict priority scheduler allows s 2 2 only in global states where P 1 2 has terminated, a condition that we write as A 1 > q 1 2 . The automaton obtained by composing the system with such a scheduler is shown in Fig. 4.7. Note that strict priority schedulers make the automaton always "bypass" a conflict state from the same side.

q 2 1 q 1 1 q1 2 q 1 2 q 1 3 q 1 f q2 2 q 2 2 q 2 3 q 2 f q 1 2 q 2 2 x 1 := 0 e 2 2 e 2 1 e 2 1 x 2 1 := 0 s 2 2 s 2 2 s 1 2 s 1 2 (a) e s e 1 2 e q 2 1 q 1 1 q1 2 q 1 2 q 1 3 q 1 f q2 2 q 2 2 q 2 3 q 2 f q 1 2 q 2 2 Z 12 Z 12 Z 21 Z 21 e 2
q 2 1 q 1 1 q1 2 q 1 2 q 1 3 q 1 f q2 2 q 2 2 q 2 3 q 2 f q 1 2 q 2 2 e 2 2 A 1 > q 1 2 Figure 4
.7: (a) A scheduler that gives strict priority to P 1 . This is realized by the condition A 1 > q 1 2 which allows P 2 2 to start only after P 1 2 terminates.

Strict priority schedulers can be unnecessarily rigid for tasks with a significant variability in durations as they do not adapt to the actual evolution of the schedule. As an example for such adaptability consider the case where P 2 1 terminates very early so that we can start P 2 2 so that it will surely terminate before P 1 2 becomes enabled and hence will not block it. Even if this is not guaranteed with certainty, a scheduler might want to start P 2 2 if the expected delay incurred to P 1 is small. Technically, the knowledge of the relative timing of e 2 1 at decision time is encoded by the value of clock x 1 reset upon starting P 1 1 . The larger is the value of x 1 , the more we are likely to block P 1 and for a longer period. Hence the condition for issuing s 2 2 by such a state-dependent scheduler will be of the form (A 1 > q 1 2 ) ∨ (A 1 < q1 2 ∧ x 1 < d) for some constant d. The labeling of states and qualitative behaviors with constraints in order to compute volumes, probabilities and expected termination times can be extended to handle all these types of schedulers. As an illustration consider the FIFO scheduler of Fig. 4.6-(b) which admits 4 classes of qualitative behaviors (scenarios) that correspond to the outcomes of the conflict between P 1 and P 2 on the shared resource. These scenarios are characterized by the identity of the winner (for this scheduler it depends on the relation between t 1 1 and t 2 1 ) and by whether the loser termination time is delayed (depending on whether the winner releases the resource before the loser becomes enabled). These cases are summarized in Table 4.1 and depicted in Fig. 4.6-(b).

The transformation T from the duration space to the time-stamp space is different from the independent execution framework. It can nevertheless be shown to be volume preserving along the following lines. First, one can show that after adding inter-process precedence constraints causality is preserved and there is always a rearrangement of the indices such that the transformation matrix remains lower triangular. Secondly the notion of volume preservation can be easily generalized from linear to piecewise-linear transformations.

The above analysis can be generalized to m distinct resources and to multi-party conflicts on each of them. For each resource l one can compute the set U l of all the utilization scenarios for this resource and their respective zones. A scenario corresponds to a particular order of resource winner loser delayed loser not delayed utilization by conflicting steps and to the waiting delays incurred to these steps. Then the classes of potential qualitative behaviors of interest are the combinations of those, that is,

P 1 Z 12 t 1 1 < t 2 1 t 1 1 + a 1 2 < t 1 2 < t 1 1 + b 1 2 t 2 1 < t 1 2 t 1 2 + a 2 2 < t 2 2 < t 1 2 + b 2 2 Z 12 t 1 1 < t 2 1 t 1 1 + a 1 2 < t 1 2 < t 1 1 + b 1 2 t 1 2 < t 2 1 t 2 1 + a 2 2 < t 2 2 < t 2 1 + b 2 2 P 2 Z 21 t 2 1 < t 1 2 t 2 1 + a 2 2 < t 2 2 < t 2 1 + b 2 2 t 2 2 < t 1 1 t 2 1 + a 2 2 < t 2 2 < t 2 1 + b 2 2 Z 21 t 2 1 < t 1 2 t 2 1 + a 2 2 < t 2 2 < t 2 1 + b 2 2 t 1 1 < t 2 2 t 2 1 + a 2 2 < t 2 2 < t 2 1 + b 2 2
U = U 1 ו • •×U m
with zones defined by intersection. While this sounds like a recipe for a severe combinatorial explosion, note that many scenarios will lead to empty zones, either for logical reasons (interprocess ordering of conflicting steps is incompatible with local precedence constraints) or due to the arithmetics of timing constraints (two conflicting tasks, one at the beginning and one at the end of their respective processes, are likely to be executed in one order). Naturally, for priority schedulers there will be fewer scenarios to analyze.

Implementation and Experimental Results

We have implemented a prototype tool which computes expected termination times as described in this chapter. As input it takes a system description consisting of processes, steps, duration intervals and conflicts as well as a definition of a scheduling policy. Then for every utilization scenario it derives the corresponding zone, using the DBM library of IF [START_REF] Bozga | The if toolset[END_REF] to normalize constraints and detect empty zones. Then it performs integration over the non-empty zones to compute probability and expected termination time. The integration uses the GNU Multiple Precision Arithmetic Library (GMP) to avoid rounding errors. Below we give more technical details.

System Description

The prototype tool takes as input a textual description of the system, specified by the following grammar:

system-decl ::= { process-decl } * { conflict-decl } * process-decl ::= process-id { step-decl } step-decl ::= [ l , u ] conflict-decl ::= shared := type { step-id , { step-id } * } type ::= STRICT | FIFO step-id ::= process-id.step-num
Conflicts are defined through shared variables by specifying all steps P i j that use the same resource. An example of such description is depicted in Listing-4.1 where processes P 1 and P 2 execute their respective second step on the same resource.

Constraints Generation

Constraints are generated in two steps. First we generate those implied by independent steps, those where starting and ending do not influence steps from other processes. Constraints for conflicting steps are handled in a separated step and imply cases splitting. Depending on scheduling policy, the termination of steps before the conflict influences execution order on the shared resource and also the start time of successors steps.

As an example consider 2 process P 1 and P 2 having 3 steps and executing their respective second step P 1 2 and P 2 2 on the same resource. For a FIFO policy there are 4 cases as shown in Table-4.1 and for a strict policy with P 1 > P 2 there are 2 cases:

• t 1 2 < t 2 1 implies P 2 2 starts after P 1 2 (real conflict) • t 1 2 > t 2 1 implies P 2 2 starts after P 2 1 (false conflict)
Depending on the number of conflicts several cases needs to be computed. The number of cases for a single FIFO scheduler implying s steps is bounded by (2 (s-1) • s!) . This bound for a STRICT scheduler implying s steps is 2 s . The total number of cases for n processes with i resources sharing s i steps in FIFO and j resources sharing s j steps in strict policy is then bounded by:

n • i (2 (s i -1) • s i !) • j 2 (s j )
Note that during generation, constraints are also encoded as zones, enabling elimination of unfeasible cases, by emptiness check.

Finally for computing expected time we need to know the variable corresponding to the last step responsible for the global execution time. This splits all previous cases according to the identity of the last process, by adding constraints ∀i, t i n < t last n . Expected time is then computed according to variable t last n in each case. For the example depicted in Listing-4.1, the constraints are split into 4 cases corresponding to the several possible orders of execution, shown in Listing 4.2, 4.3, 4.4, 4.5. Note that, here, each step of the processes are associated with a variable t i defined in a lexicographic order i.e process P 1 {t 1 , t 2 , t 3 } and process P 2 {t 4 , t 5 , t 6 }. Variable Dt i defines the domain of each steps and variable expT correspond to the last step leading to the global execution time, so expected time will be computed according to variable expT .

Dt1 : = [ 2 , 8 ] 2<t 1 <8 2<t 1 <8 2<t 1 <8 2<t 1 <8 Dt4 : = [ 4 , 1 0 ] Dt4 : = [ 4 , 1 0 ] Dt4 : = [ 4 , 1 0 ] Dt4 : = [ 4 , 1 0 ] 4<t 4 <10 4<t 4 <10 4<t 4 <10 4<t 4 <10 Dt2 : = [ 3 , 7 ] Dt2 : = [ 3 , 7 ] Dt2 : = [ 3 , 7 ] Dt2 : = [ 3 , 7 ] 3<t 2-t 1 <7 3<t 2-t 1 <7 3<t 2-t 1 <7 3<t 2-t 1 <7 t 1<t 2 t 1<t 2 t 1<t 2 t 1<t 2 / / F a l s e c o n f l i c t / / F a l s e c o n f l i c t / / R e a l c o n f l i c t / / R e a l c o n f l i c t Dt5 : = [ 4 , 1 2 ] Dt5 : = [ 4 , 1 2 ] Dt5 : = [ 4 , 1 2 ] Dt5 : = [ 4 , 1 2 ] 4<t 5-t 4 <12 4<t 5-t 4 <12 4<t

Computation

For each case, resulting from constraint generation we compute the volume of the corresponding polyhedron defined as a zone. This volume is divided by the domain of each variable to get the probability of each case. The associated expected time value is computed according to the variable which defines the execution of the last step in the global behavior. Results for the example of Listing-4.1 is shown in Table - At implementation, the symbolic volume SV is represented as a list of pairs Z i , E i where Z i is a zone and E i is a polynomial on t variables. Recall ϕ C is the constraint describing the whole time-stamp space, Z i ⊆ C i with ϕ C i is the constraint of each case.

Initially SV = Z i , 1 and then, iteratively, we eliminate all variables t , that is we compute the integral of E i with respect to t. At each iteration, SV grows depending on the number of splits implied by the integration calculation. We explain in the following how this computation works.

Variable Elimination

The variable elimination computation is shown in Algorithm-2. The function isDegenerate() checks if the zone is not empty and if all bounds l ≤ x i -x j ≤ u are thick that is l = u. The function compact() merges nodes with the same zone to avoid splitting explosion.

In general integration takes place in R nk and its complexity depends on the following factors. First, the number of scenarios (orders of resource utilizations and their combinations) determines the number of zones whose volume we might need to compute, in case they are not detected beforehand to be empty. Then the order of variables elimination influences the number of splits during integration as shown in Fig- 4.5. The naive order is to eliminate variable in a lexicographic order (Order 1) from t 1 to t n but this gives bad results. To counter that, different heuristics have been implemented. One of them consists in computing the minimal constraints system [START_REF] Kim Guldstrand Larsen | Efficient verification of real-time systems: compact data structure and state-space reduction[END_REF] for each zone and then the least constrained variable is eliminated (Order 2). Topological ordering is another one and consists in eliminating variables according to the reverse order implied by the global execution. For the case depicted in Listing-4.2 the order of elimination using this heuristic is:

t 6 ≺ t 3 ≺ t 5 ≺ t 2 ≺ t 4 ≺ t 1
In a similar heuristic, for each zone and each variable t we compute I t , the projection of the zone on t. Then we define a partial order relation between these intervals such that I t < I t if the upper Algorithm 2 Variable elimination function ELIMINATE(X,L) //L is a list of nodes, X is a the variable to eliminate //Here, elimination means computation of the integral with respect to X Res ← ∅ The resulting node list for all N = Z, E ∈ L do Z and E are zone and polynomial of node N

for i = 0 → N Z do N Z is the dimension of Z if i = x then for j = 0 → N Z do Z c ← new ZONE Z c
encode bounds constraints // Split and enforce these bounds as maximal, resp minimal

for k = 0 → N Z do if k = x ∧ k = i then Z c ∧ {X k -X i ≤ Z[k][x] -Z[i][x]} end if end for for k = 0 → N Z do if k = x ∧ k = j then Z c ∧ {X j -X k ≤ Z[x][k] -Z[x][j]} end if end for // Intersect bounds constraints with current zone Z split ← Z ∧ Z c if ¬ isDegenerate(Z split ) then check if current zone is not degenerated // Create a new node with Z split and integrate current polynomial E Res ← Res ∪ Z split , X j -Z[x][j] X i -Z[i][
x] E dX end if end for end if end for end for compact(Res) end function bound of I t is smaller than the lower bound of I t . Then we construct a compatible linear order and integrate backwards (Order 3).

The chosen order determines the number of case splits but also the form of the integration domains and the polynomials obtained during integration. We experienced orders of integration that generate more splits but take less overall computation time. However, experimental result show that lexicographic order behaves the worst. None of the other heuristics is universally better than the other. For the moment we have no systematic explanation for these variations.

We show in Tables 4.3 and 4.4 the difference on the number of splits during integration according to the chosen elimination ordering. Order 1,2 and 3 stand for the ordering heuristics presented above. Each row corresponds to a non-empty case. Column Splits indicates the number of splits that occurred during integration (i.e the maximum size of the list SV ) and column Int indicates the number of integrations that have been performed (at least as many as the number of variables incremented by the number of splits). Column Proba and ExpectedTime give the probability and expected time for each case. The row Time shows the execution time for computing all cases. We see that the number of splits is extremely sensitive to the elimination order.

Experiments

We started conducting some more systematic experiments to assess the feasibility bounds of this approach. For each value of n from 1 to 5 and for each value of k from 1 to 40, we choose a number of conflicts (between 0 and 3) and a number of participants in each conflict (2 or 3). Each choice in this space defines a problem type for which we draw 10 concrete problems by randomly choosing the identity of the conflicting steps as well as step duration intervals of the form [c -d, c + d] with c drawn uniformly in [START_REF] Bjerregaard | A survey of research and practices of networkon-chip[END_REF][START_REF] Bozga | Source-to-source architecture transformation for performance optimization in BIP[END_REF] and d in [0, c/20]. Then we try to compute expected termination times for a FIFO scheduler with a timeout of 3 minutes per problem on a computer with a Pentium processor at 2.0GHz and 2 GB of memory.

The experiments with n = 1 compute the volume of one zone, the time-stamp space. Applying the reverse order integration we can compute up to dimension 63 in 0.4 seconds (currently this is a limitation of our DBM library). This performance is due to the fact that the elimination ordering is optimal in the sense that no split is created during computation and, in that case, the number of integration steps is minimal and equals the number of variables.

As already mentioned we tested several orders of integration that generate more or less splits. Since there is a lot of exploration and fine tuning ahead, this is definitely not the last word on the topic. To give an idea, we mention some problem types for which we managed to compute for all the test cases. These include (n, k) = (2, 12) with 2 conflicts, [START_REF] Ackland | A single-chip 1.6 billion 16-b mac/s multiprocessor dsp[END_REF][START_REF] Alur | A theory of timed automata[END_REF] and (4, 6) with 3 binary conflicts or 2 ternary conflicts and (5, 4) with 2 binary conflicts. The results are listed in Table -4

Conclusions

We have presented a computational technique to evaluate schedulers in a non-Markovian setting. To the best of our knowledge no similar computational results have been reported. The analysis was based on splitting the space of valuations of the random variables and computing volumes. This technique relies heavily on computing volumes and integrals over zones. Finding good heuristics for this activity is a challenging research problem. We mention some future work for a longer term:

1. To analyze larger systems one needs to develop algorithms that do not explore all classes of qualitative behaviors but restrict the exploration to a high-volume small subset of those, whenever such exists.

2. Another major challenge is to extend this framework to cyclic systems, define the appropriate performance measures and study their steady-state behavior.

3. Finally, it would be interesting to compare the analytic method developed here with statistical approaches based on random simulation. It is intriguing to see how many simulation runs are needed to approximate our results with a good confidence.

Duration Probabilistic Automata: Synthesis

We now move to the synthesis of optimal schedulers that minimize the expected termination time.

We develop techniques for value/policy iteration (dynamic programming) that compute a value function and optimal action for any point in the extended state space (including clock values).

To this end we define a stochastic time-to-go function which assigns to any state of the schedule (global state of the automaton and the values of active clocks) the density of the time to total termination starting from this state under the optimal strategy. These functions are piecewisecontinuous and we show how they can be computed backwards from the final state. This will require several definitions. We will use non-standard notation for distributions:

Preliminary Definitions

ψ[≤ t] = t 0 ψ[t ]dt ψ[> t] = 1 -ψ[≤ t]
with ψ[≤ t] indicating the probability of a duration which is at most t. We use c to denote the "deterministic" density which gives the constant c with probability 1, which would be written in density terms as

ψ[t] = ∞ if t = c 0 otherwise
The expected value of a time density

ψ is E(ψ) = ψ[t] • tdt.
We will use such densities to specify durations of tasks (process steps) as well as the remaining time to termination given some state of the system. To this end we need the following operators on densities:

1. Convolution, to characterize the duration of two or more tasks composed sequentially; • The convolution ψ 1 * ψ 2 is a density ψ supported by

I = I 1 ⊕ I 2 = [a 1 + a 2 , b 1 + b 2 ] defined as ψ [t] = t 0 ψ 1 [t ]ψ 2 [t -t ]dt • The residual density (shift) of ψ relative to a real number 0 ≤ x < b is ψ = ψ /x such that ψ [t] = ψ[x + t] • γ a,b (x)
where

γ a,b (x) = 1 if 0 < x < a b-a b-x if a < x < b
Note that when x < a, ψ /x is a simple shift of ψ. When x > a we already know that the actual duration is at least x (restricted to the sub-interval [x, b]) and hence we need to normalize, as illustrated in Figure 5.1. 1 Note also that (ψ * c)[t] = (c * ψ)[t] = ψ[t -c] and that 0 is the identity element for convolution. We can write ψ = ψ /x more explicitly as

ψ [t] =        0 when x + t < a 1 b-a when x < a, a < x + t < b 1 b-x when a < x, x + t < b 0 when b < x + t (5.1)
One can verify that the shift satisfies:

1. ψ /x [t -x] = γ a,b (x) • ψ[t].
2. (ψ /x ) /y = ψ /(x+y) .

A subset of a hyper-rectangle is called a zone if it can be expressed as a conjunction of orthogonal and difference constraints, namely constraints of the form x i ≤ c, x i -x i ≤ c, etc. 1 The definition can be extended to any bounded-support density with the normalization factor being

1 := 0 s 1 q 1 q 1 e 1 • • • x k := 0 s k q k q k q k+1 e k x 1 = y 1 x k = y k y 1 := ψ 1 () • • • y k := ψ k ()

Processes in Isolation

The processes in our model are inspired by the jobs in the job-shop problem. Each process consists of an ordered sequence of steps such that a step can start executing only after its predecessor has terminated. 2 For simplicity of notation we assume all processes to have the same number k of steps and let K = {1, . . . , k}. Definition 5.2.1 (Process). A sequential stochastic process is a pair P = (I, Ψ) where I = {I j } j∈K is a sequence of duration intervals and Ψ = {ψ j } j∈K is a matching sequence of densities with ψ j being the uniform density over I j = [a j , b j ], indicating the duration of step j.

Probabilistically speaking, step durations can be viewed as a finite sequence of independent uniform random variables {y j } j∈K that we denote as points y = (y 1 , . . . , y k ) ranging over a duration space

D = I 1 × • • • × I k ⊆ R k with density ψ(y 1 , . . . , y k ) = ψ 1 (y 1 ) • • • ψ k (y k ).
A state-based representation of a process is given by simple DPA. Definition 5.2.2 (SDPA). A simple duration probabilistic automaton (SDPA) of k steps is a tuple A = (Σ, Q, {x}, Y, ∆) where Σ = Σ s Σ e is the alphabet of start and end actions with Σ s = {s 1 , . . . , s k } and Σ e = {e 1 , . . . , e k }. The state space is an ordered set Q = {q 1 , q 1 , q 2 , . . . , q k , q k+1 } with q j states considered idle and q j states are active, x is a clock variable and Y = {y 1 , . . . , y k } is a set of auxiliary random variables. The transition relation ∆ consists of tuples of the form (q, g, r, q ) with q and q being the source and target of the transition, g is a guard, a precondition (external or internal) for the transition and r is an action (internal or external) accompanying the transition. The transitions are of two types:

1. Start transitions: for every idle state q j , j < k + 1 there is one transition of the form (q j , s j , {x}, q j ). The transition, triggered by a scheduler command s j , activates clock x is resets it to zero; 2. End transitions: for every active state q j , there is a transition, conditioned by the clock value, of the form (q j , x = y j , e j , q j+1 ). This transition renders clock x inactive and outputs an e j event.

The operational interpretation is the following (see Fig. 5.2). First, for each step j we draw a duration y j according to ψ j . Upon a scheduler command s j the automaton moves from a waiting state q j to active state q j in which clock x advances with derivative 1. The end transition is taken when x = y j , that is, y j time after the corresponding start transition. An extended state (configuration) of the automaton a pair (q, x) consisting of a discrete state and a clock value 3 which represents the time elapsed since the last start transition. The generalized state-space of the SPDA is thus

S = {(q j , ⊥) : j ≤ k + 1} ∪ {(q j , x) : j ≤ k ∧ x ≤ b j }
where ⊥ indicates the inactivity of the clock in waiting/idle states.

2 See [START_REF] Abdeddaïm | Scheduling with timed automata[END_REF] for a straightforward generalization to partial-order precedence constraints. 3 To avoid additional notations we use x both for the clock variable and its value.

Note the difference between transition labels s j and e j : the start transitions are controllable and are issued by the scheduler that we want to optimally synthesize while the end transitions represent the uncontrolled external (to the scheduler) environment which is assumed to be uniformly distributed. Without a scheduler, the SDPA is under-determined and can issue a start transition any time. The derivation of an optimal scheduler is done via the computation of a time-to-go function that we first illustrate on the degenerate case of one process in isolation, where each state has only one successor and any waiting between steps unnecessarily increases the time to termination. Definition 5.2.3 (Local Stochastic Time to Go). The local stochastic time-to-go function associates with every state (q, x) a time density µ(q, x) with µ(q, x)[t] indicating the probability to terminate within t time given that we start from (q, x) and apply the optimal strategy. This function admits the following inductive definition:

µ(q k+1 , ⊥) = 0 (5.2) µ(q j , ⊥) = µ(q j , 0) (5.3) µ(q j , x)[t] = t 0 ψ j [x + t ] • γ a,b (x) • µ(q j+1 , 0)[t -t ]dt (5.4)
Line (5.2) indicates the final state while (5.3) comes from the fact that in the absence of conflicts the optimal scheduler need not wait and should start each step immediately when enabled. Equation (5.4) computes the probability for termination at t based on the probabilities of terminating the current step in some t and of the remaining time-to-go being t -t . It can be be summarized in a functional language as µ(q j , x) = ψ j /x * µ(q j+1 , ⊥) = ψ j /x * µ(q j+1 , 0) (5.5)

The successive application of (5.5) yields, not surprisingly, µ(q

1 , 0) = ψ 1 * • • • * ψ k .
Definition 5.2.4 (Local Expected Time to Go). The expected time-to-go function is

V : Q × X → R + defined as V (q, x) = µ(q, x)[t] • tdt = E(µ(q, x)).
This measure satisfies V (q j , x) = E(ψ j /x ) + V (q j+1 , 0) where the first term is the expected termination time of step j starting from x. For the initial state this yields

V (q 1 , 0) = E(ψ 1 * • • • * ψ k ) = E(ψ 1 ) + • • • + E(ψ k ) = k j=1 (a j + b j )/2.

Conflicts and Schedulers

We now extend the model to express n processes, indexed by N = {1..n}, that may run in parallel except for steps which are mutually conflicting due to the use of the same resource. Definition 5.3.1 (Process System). A process system is a triple (P, M, h) where

P = P 1 || • • • ||P n = {(I i , Ψ i )} i∈N
is a set of processes, M is a set of resources, and h : N × K → M is a function which assigns to each step the resource it uses.

We use notations P i j to refer to step j of process i and ψ i j and I i j = [a i j , b i j ] for the respective densities and their support intervals. Likewise we denote the corresponding controllable and uncontrollable actions by s i j and e i j , respectively. Without loss of generality we assume there is one instance of each resource type, hence two steps P i j and P i j such that h(i, j) = h(i , j ) are in conflict and cannot execute simultaneously. Each process is modeled as an SPDA A i = (Σ i , Q i , {x i }, Y i , ∆ i ) and the global system is obtained as a product of those restricted to conflictfree states. We write global states as q = (q 1 , . . . , q n ) and exclude states where for some i and i , q i = q i j , q i = q i j and steps P i j and P i j are conflicting. We say that action s i j (respectively, e i j ) is enabled in q if q i = q i j (resp. q i = q i j ). Since only one transition per process is possible in a global state, we will sometime drop the j-index and refer to those as s i and e i .

Definition 5.3.2 (Duration Probabilistic Automata). A duration probabilistic automaton (DPA) is a composition

A = A 1 • • • • • A n = (Σ, Q, X, Y, ∆) of n SDPA with the action alphabet being Σ = i Σ i . The discrete state space is Q ⊆ Q 1 × • • • Q n (
with forbidden states excluded). The set of clocks is X = {x 1 , . . . , x n }, the extended state-space is S ⊆ S 1 × • • • S n and the auxiliary variables are Y = i Y i ranging over the joint duration space D = D 1 ו • •×D n . The transition relation ∆ is built using interleaving, that is, a transition (q, g, r, q ) from q = (q 1 , . . . , q i , . . . , q n ) to q = (q 1 , . . . , q i , . . . , q n ) exist in ∆ if a transition from (q i , g, r, , q i ) exists in ∆ i , provided that q is not forbidden.

The DPA thus defined (Fig. 4.6-a) is not probabilistically correct as it admits non-determinism of a non probabilistic nature: in a given state the automaton may choose between several start transitions or decide to wait for an end transition (the termination of an active step). A scheduler selects one action in any state and then the only non-determinism that remains is due to the probabilistic task durations. A discussion on different types of schedulers can be found in [START_REF] Kempf | Performance evaluation of schedulers in a probabilistic setting[END_REF].

Definition 5.3.3 (Scheduler).

A scheduler for a DPA A is a function Ω : S → Σ s ∪ {w} such that for every s ∈ Σ s , Ω(q, x) = s only if s is enabled in q and Ω(q, x) = w (wait) only if q admits at least one active component.

Composing the scheduler with the DPA (see Fig. • Start steps: (q, x) s i j -→ (q , x ) iff q i = q i j and Ω(q, x) = s i j ;

• End steps: (q, x) e i j -→ (q , x ) iff q i = q i j and x i = y i j ;

• Time steps: (q, x)

t -→ (q, x + t) iff ∀i (q i = q i j ⇒ x i + t < y i j ).
The run associated with y is a sequence of steps starting at (q 1 1 , . . . , q n 1 ) and ending in (q 1 k+1 , . . . , q n k+1 ).

The duration of a run is the sum of the time steps and it coincides with the termination time of the last process, known as the makespan in the OR jargon. In a state q where P i is active, its t-i-successor, denoted by σ i (t, q, x), is the state (q , x ) reached after a time step of duration t followed by an e i transition.

Expected Time Optimal Schedulers

In [START_REF] Kempf | Performance evaluation of schedulers in a probabilistic setting[END_REF] we developed a method to compute the expected termination time under a given scheduler by computing volumes in the duration space. We now show how to optimally synthesize such schedulers from an uncontrolled DPA description. To this end we will have to extend the formulation of stochastic time-to-go from a single process (5.4) to multiple processes (5.8).

We define a partial order relation on global states based on the order on the local states with q q if for every i, q i q i . We lift this relation to extended states letting (q, x) (q , x ) if q q or q = q ∧ x ≤ x . The forward cone of a state q is the set of all states q such that q ≺ q . The immediate successors of a state q are the states reachable from it by one transition. A partial scheduler is a scheduler defined only on a subset of Q. To optimize the action of the scheduler in a state we need compare the effect of the action on the time-to-go. Definition 5.4.1 (Local Stochastic Time-to-Go). Let A be a DPA with a partial strategy whose domain includes the forward cone of a state q. With every i, x and every s ∈ Σ s ∪ {w} enabled in q, the time density µ i (q, x, s) : R + → [0, 1] characterizes the stochastic time-to-go for process P i if the controller issues action s at state (q, x) and continues from there according to the partial strategy.

Note that for any successor q of q the optimal action has already been chosen and we denote its associated time-to-go by µ(q, x). Once µ i (q, x, s) has been computed for every i, the following measures, all associated with action s, can be derived from it. Definition 5.4.2 (Global Stochastic Time-to-Go). With every state (q, x) and action s enabled in it, we define

• The stochastic time-to-go for total termination (makespan): µ(q, x, s) = max{µ 1 (q, x, s), . . . , µ n (q, x, s)} • The expected total termination time:

V (q, x, s) = t • µ(q, x, s)[t]dt
The computation of µ for a state q, based on the stochastic time-to-go of its successors, is the major contribution of this chapter. The hard part is the computation of the time-to-go associated with waiting in a state where several processes are active. In this situation (known as a race) the automaton may leave q via different transitions and µ should be computed based on the probabilities of these transitions (and their timing) and the cost-to-go from the respective successor states.

With each state (q, x) we associate a family {ρ i (q, x)} i∈N of partial time densities with the intended meaning that ρ i (q, x)[t] is (the density of) the probability that the first process to terminate its current step is P i and that this occurs within t time. This definition is relative, of course, to the fact that the time elapsed since the initiation of each and every active step is captured by the respective clock value in x. 5If we look at the algorithm more carefully we see that it splits into three parts, the third being merely book-keeping. In the first we essentially compute the outcome of waiting by race analysis and of starting. As we shall see, starting from a specific class of time densities, this part can be done in a symbolic/analytic way, resulting in closed-form expressions over x and t for the values of µ i , µ and V associated with each action. The second part involved optimization: to characterize the extended states according to the action that optimizes V in them. For this part we have not characterized the class of partitions of the clock space obtained but proved a monotonicity property (non-lazy schedulers) that will facilitate the task of tracing the boundary. Since this work is not fully completed, it is delegated to Appendix A.

Computational Aspects

We now turn to the properties of the previously defined functions and the way to compute them. For every q, µ i (q, x) is in fact an infinite family of functions parameterized by the clock valuations inside the rectangle Z q of clock valuations which are possible as state q. Definition 5.5.1 (Zone-Polynomial Time Densities). A function µ : Z → (R + → [0, 1]), where Z is a rectangular clock space, is zone polynomial if it can be written as

µ(x 1 , . . . , x n )[t] =        f 1 (x 1 , . . . , x n )[t]) if Z 1 (x 1 , . . . , x n ) and l 1 ≤ t ≤ u 1 f 2 (x 1 , . . . , x n )[t]) if Z 2 (x 1 , . . . , x n ) and l 2 ≤ t ≤ u 2 . . . f L (x 1 , . . . , x n )[t]) if Z L (x 1 , . . . , x n ) and l N ≤ t ≤ u L where • For every r, Z r (x 1 , ..., x n ) is a zone included in the rectangle Z, which moreover satisfies either Z r ⊆ [x i ≤ a i ] or Z r ⊆ [a i ≤ x i ],
for every i = 1..n.

• For every r, the bounds l r , u r of the t interval are either nonnegative integers c or terms of the form c -x i , with i = 1, n, c ∈ Z + . Moreover, the interval [l r , u r ] must be consistent with the underlying zone, that is, Z r ⊆ [l r , u r ].

• For every r, f r (x 1 , ..., x n )[t] = k P k (x 1 ,...,x n ) Qr(x 1 ,...,x n ) t k where P k are arbitrary polynomials and Q r is a characteristic polynomial associated with zone Z r defined as i (b i -max{x i , a i }).

Note that for each zone, the max is attained uniformly as either a i or x i .

Theorem 2 (Closure of Zone-Polynomial Densities). Zone-polynomial time densities are closed under 5.7 and 5.8).

Sketch of Proof Operation 5.7 is a simple substitution. Closure under summation is also evident -you just need to refine the partitions associated with the summed functions and make them compatible and then apply the operation in each partition block. The only intricate part concerns the quasi-convolution part of (5.8). The function µ i (σ i (t , q, x))[t -t ] is not a zone polynomial time density. Due to the time progress by t enforced by the substitution σ i it might happen that polynomials of the form (b i -(x i -t )) appear in the denominators. But, in all feasible cases, they will be simplified through multiplication by ρ i (q, x)[t ] which contains the same polynomials as factors (within ψ i /x i [≥ t ], see Def. 5.4.3). Hence, integration of t is always trivially completed as t occurs only on numerator polynomials and/or powers of the form t k and (t -t ) k . Moreover, after integration, the remaining constraints on t and x can also be rewritten to match the required form of the zone-polynomial time densities.

We realized a prototype implementation of operator (5.8) that we detail in the next section and apply to a simple example.

Implementation

In the following we denote by F a zone polynomial function µ(x 1 , . . . , x n )[t] (Definition 5.5.1). We provide a library for the manipulation of such function. At implementation F is represented as a list of nodes {N 1 , . . . , N k } and F = i N i (5.9)

A node N i = Z i , L i is defined by:

• Z i a zone • L i a list of pairs C i j , F i j where: -C i j is a constraints on variable t -E i j is an expression defined as a polynomial fraction f r (x 1 , ..., x n )[t] as in Definition 5.5.1

F =                          Z C E l 1 1 < t < u 1 1 E 1 1 Z 1 . . . . . . l 1 k 1 < t < u 1 k 1 E 1 k 1 . . . . . . . . . l n 1 < t < u n 1 E 1 1 Z n . . . . . . l n k n < t < u n k n E n k n
(5.10)

As an example ψ /x [t] defined by (5.1) is encoded as:

ψ /x [t] =                    Z C E 0 < t < a -x 0 0 < x < a a -x < t < b -x 1 b-a b -x < t 0 a < x < b 0 < t < b -x 1 b-x b -x < t 0 (5.11)
Manipulation of zones are performed using the DBM library of IF [START_REF] Bozga | The if toolset[END_REF]. We extend the polynomial library developed for volume computation in the previous chapter for the manipulation of polynomial fractions. To compute µ(q, x, s) several operations on nodes are necessary. We present in the sequel how they have been implemented. Note that, by construction we ensure that

F is in a disjoint form. That is, ∀N i , N j ∈ F, Z i ∩ Z j = ∅ ∧ ∀C i j , C i k ∈ L i , C i j ∩ C i k = ∅

Disjoint nodes

Let us first explain how nodes are kept disjoint during all computations. It is a necessary operation for further computations, especially to facilitate integration of zone polynomial function according to the t variables. This operation is performed by: ∀i = j, if Z i ∧ Z j = ∅ remove N i , N j and add new nodes:

• {Z i ∧ Z j , L i + L j } • {Z i -Z j , L i } • {Z j -Z i , L j }
The subtraction of two zones leads to several zones implying creation of new nodes. It is computed as follows:

Z 1 -Z 2 = i,j (Z 1 ∩ ¬Z 2 [i][j])
The number of resulting nodes is bounded by n 2 where n is the dimension of the zone. More efficient algorithm based on minimal constraint graph can be used to minimize the number of splits, readers can refer to [START_REF] David | Minimal dbm substraction[END_REF] for more details.

The operation L i + L j is done by adding each pair C, E from the two lists together. This addition results in 3 new pairs defines as follows:

C 1 , E 1 + C 2 , E 2 =    C 1 ∩ C 2 , E 1 + E 2 C 1 ∩ ¬C 2 , E 1 ¬C 1 ∩ C 2 , E 2 (5.12)
Inside the operation (5.12), constraints on t are defined as conjunction of bounds, i.e with C i = l i < t < u i and C i = l j < t < u j :

C i ∩ C j = max(l i , l j ) < t < min(u i , u j )
Note that the list L i associated with each disjoint zone must also be disjoint, that is:

∀ C k i , E k i , C k j , E k j ∈ L k , C i ∩ C j = ∅
For that we need to compute unique bounds l and u on variable t. This is done by creating a new case for each possible pair of bounds as shown in Algorithm-4.

Algorithm 4 CANONIZE ( C, E )

Res = ∅ The resulting node list for all l i ∈ C do for all u j ∈ C do //set l i and u j as lower and upper bound

C tmp ← {l i < t < u j } Z tmp ← new ZONE for all l k = l i do // l i > l k ⇒ x i -a i > x k -a k ⇒ x k -x i < a k -a i Z tmp ← Z tmp ∩ {l i > l k } end for for all u k = u j do // u j < u k ⇒ x i -a i < x k -a k ⇒ x i -x k < a i -a k Z tmp ← Z tmp ∩ {u j < u k } end for Z tmp ← Z tmp ∩ {l i < u j } check if new bounds are correct if ¬ isDegenerate(Z tmp ) then Res ← Res ∪ Z tmp , { C tmp , E } end if end for end for return Res

Product

The multiplication of two zone polynomial functions F 1 and F 2 is done by multiplying all their nodes in pairs. The result of N i • N j is a node N k = Z i ∩ Z j , L i • L j and the computation is shown in Algorithm-5.

Algorithm 5 MULTIPLY (N 1 , N 2 ) N r = Z r , L r
The resulting node

Z r = Z 1 ∩ Z 2 L r = ∅ if ¬ isDegenerate(Z r ) then for all E i , C i ∈ L 1 do for all E j , C j ∈ L 2 do if C i ∩ C j = ∅ then L r ← L r ∪ E i • E j , C i ∩ C j end if end for end for end if return N r

Addition

The addition of two two zone polynomial functions F 1 and F 2 is performed in the same way as for multiplication, i.e by adding all their nodes in pairs as shown in Algorithm 6. The results of the addition of two nodes is:

N i + N j =    Z i ∩ Z j L i + L j Z i ∩ ¬Z j L i ¬Z i ∩ Z j L j
Note that the zone subtraction did not appear in the multiplication operation because the resulting nodes are empty like Z i ∩ ¬Z j , L i • 0 = 0 .

Integration

Integration is performed on zone polynomial functions that are in disjoint form as explained previously. Constraints on variable t are disjoint and are sorted in increasing order. Note that they are defined continuously between lowest and uppermost bounds i.e u i = l i-1 . For all nodes integration is performed on each E according to bounds on t. In the following F [e] denotes substitution of variable t by expression e. Consider one node Z, L of a probability density function. We compute its distribution t <t ψ /x [t ]dt by computing iteratively integrals from 0 to t according to the bounds in the ordered list

L = { a 1 < t < a 2 , E 1 , . . . , a n-1 < t < a n , E n } which gives a node Z, L where L = a 1 < t < a 2 , E 1 = t a 1 E 1 [t ]dt , . . . , a n-1 < t < a n , E n-1 + t a n-1 E n [t ]dt 5.6. IMPLEMENTATION Algorithm 6 ADD (N 1 , N 2 ) Res ← ∅ The resulting node list if Z 1 ∩ Z 2 = ∅ then N tmp ← new Z 1 ∩ Z 2 , L tmp L tmp list of resulting pairs C, E for all E i , C i ∈ L 1 do for all E j , C j ∈ L 2 do L tmp ← L tmp ∪ C i ∩ C j , E 1 + E 2 L tmp ← L tmp ∪ C i ∩ ¬C j , E 1 L tmp ← L tmp ∪ ¬C i ∩ C j , E 2 end for end for Res ← Res ∪N tmp end if for all Z ∈ Z 1 -Z 2 do Res ← Res ∪ Z, L 1 end for for all Z ∈ Z 2 -Z 1 do
Res ← Res ∪ Z, L 2 end for return Res

As an example recall (5.11) for which we can get the probability distribution (5.14). In the same way we can compute t<t ψ /x [t ]dt as shown in (5.15).

ψ /x [t]dt =    Z C E 0 < x < a ∅ 1 a < x < b ∅ 1 (5.13) t 0 ψ /x [t ]dt =                    Z C E 0 < t < a -x 0 0 < x < a a -x < t < b -x t-a+x b-a b -x < t 1 a < x < b 0 < t < b -x t b-x b -x < t 1 (5.14) ∞ t ψ /x [t ]dt =                    Z C E 0 < t < a -x 1 0 < x < a a -x < t < b -x b-x-t b-a b -x < t 0 a < x < b 0 < t < b -x b-x-t b-x b -x < t 0
(5.15)

An Example

We illustrate the above computation on a simple example consisting of two one-step processes P 1 and P 2 with respective duration intervals I 1 1 = [START_REF] Basten | Model-driven designspace exploration for embedded systems: the octopus toolset[END_REF][START_REF] Cherepacha | Dp-fpga: An fpga architecture optimized for datapaths[END_REF] and I 2 1 = [START_REF] Benveniste | Hybrid Dynamical Systems Theory and the SIGNAL Language[END_REF][START_REF] Bozga | Source-to-source architecture transformation for performance optimization in BIP[END_REF]. We start the backward value iteration from the final state V (q 1 2 , q 2 2 , ⊥, ⊥) = 0. In each of the two predecessor states (q 1 1 , q 2 2 ) and (q 1 2 , q 2 1 ) only one clock is active. The output of our tool and the plots of the value function are depicted in Figure 5

V (q 1 2 , q 2 1 , ⊥, x 2 )
The more involved and interesting case is in state (q 1 1 , q 2 1 ) where we have a race and a lot of case splitting according to the relation between clocks. Listing 5.1 shows the output of our tool which yields (5.16) as plotted in Fig 5 .5.

We can compute the expected time-to-go from the initial state

V (q 1 1 , q 2 1 , 0, 0) =
V (q 1 1 , q 2 1 , x 1 , x 2 )

Concluding Remarks

We have built a framework to define and synthesize optimal schedulers in a non-Markovian setting.

To the best of our knowledge no similar computational results have been reported. The synthesis algorithm is based on backward value iteration that computes the stochastic time-to-go function over the extended state space.

                                                                                                                                                                                 365 8 -7 16 x 1 -3 80 x 1 x 2 + 1 1600 x 1 x 2 2 + 3 160 x 2 1 -1 1600 x 2 1 x 2 + 1 4800 x 3 1 -9 16 x 2 + 3 160 x 2 2 -1 4800 x 3 2 if 10 ≤ x 1 ≤ 20 20 ≤ x 2 ≤ 30 10 ≤ x 2 -x 1 ≤ 20 365 8 -7 16 x 1 -3 80 x 1 x 2 + 1 1600 x 1 x 2 2 + 3 160 x 2 1 -1 1600 x 2 1 x 2 + 1 4800 x 3 1 -9 16 x 2 + 3 160 x 2 2 -1 4800 x 3 2 if 0 ≤ x 1 ≤ 10 10 ≤ x 2 ≤ 30 10 ≤ x 2 -x 1 ≤ 30 365 8 -9 16 x 1 -3 80 x 1 x 2 -1 1600 x 1 x 2 2 + 3 160 x 2 1 + 1 1600 x 2 1 x 2 -1 4800 x 3 1 -7 16 x 2 + 3 160 x 2 2 + 1 4800 x 3 2 if 10 ≤ x 1 ≤ 20 0 ≤ x 2 ≤ 10 -20 ≤ x 2 -x 1 ≤ -10 545 12 -1 2 x 1 -1 40 x 1 x 2 + 80 x 2 1 -1 2 x 2 + 1 80 x 2 2 if 0 ≤ x 1 ≤ 10 0 ≤ x 2 ≤ 10 -10 ≤ x 2 -x 1 ≤ 10 545 12 -1 2 x 1 -1 40 x 1 x 2 + 80 x 2 1 -1 2 x 2 + 1 80 x 2 2 if 10 ≤ x 1 ≤ 20 0 ≤ x 2 ≤ 10 -10 ≤ x 2 -x 1 ≤ 0 545 12 -1 2 x 1 -1 40 x 1 x 2 + 80 x 2 1 -1 2 x 2 + 1 80 x 2 2 if 10 ≤ x 1 ≤ 20 10 ≤ x 2 ≤ 30 -10 ≤ x 2 -x 1 ≤ 10 545 12 -1 2 x 1 -1 40 x 1 x 2 + 80 x 2 1 -1 2 x 2 + 1 80 x 2 2 if 0 ≤ x 1 ≤ 10 10 ≤ x 2 ≤ 20 0 ≤ x 2 -x 1 ≤ 10 2000+x 1 x 2 -50x 1 -40x 2 50-x 2 if 10 ≤ x 1 ≤ 20 40 ≤ x 2 ≤ 50 30 ≤ x 2 -x 1 ≤ 40 2000+x 1 x 2 -50x 1 -40x 2 50-x 2 if 0 ≤ x 1 ≤ 10 40 ≤ x 2 ≤ 50 30 ≤ x 2 -x 1 ≤ 50 2000+x 1 x 2 -50x 1 -40x 2 50-x 2 if 0 ≤ x 1 ≤ 10 30 ≤ x 2 ≤ 40 30 ≤ x 2 -x 1 ≤ 40 4225 2 -155 4 x 1 + 1 4 x 1 x 2 + 1 80 x 1 x 2 2 + 3 8 x 2 1 -1 80 x 2 1 x 2 + 1 240 x 3 1 -205 4 x 2 + 3 8 x 2 2 -1 240 x 3 2 50-x 2 if 10 ≤ x 1 ≤ 20 30 ≤ x 2 ≤ 40 10 ≤ x 2 -x 1 ≤ 30 4225 2 -155 4 x 1 + 1 4 x 1 x 2 + 1 80 x 1 x 2 2 + 3 8 x 2 1 -1 80 x 2 1 x 2 + 1 240 x 3 1 -205 4 x 2 + 3 8 x 2 2 -1 240 x 3 2 50-x 2 if 10 ≤ x 1 ≤ 20 40 ≤ x 2 ≤ 50 20 ≤ x 2 -x 1 ≤ 30 4225 2 -155 4 x 1 + 1 4 x 1 x 2 + 1 80 x 1 x 2 2 + 3 8 x 2 1 -1 80 x 2 1 x 2 + 1 240 x 3 1 -205 4 x 2 + 3 8 x 2 2 -1 240 x 3 2 50-x 2 if 0 ≤ x 1 ≤ 10 30 ≤ x 2 ≤ 40 20 ≤ x 2 -x 1 ≤ 30 2625-125 2 x 1 -1 2 x 1 x 2 -1 40 x x 2 2 + 3 4 x 2 1 + 1 40 x 2 1 x 2 -1 120 x 3 1 -75 2 x 2 + 3 4 x 2 2 + 1 120 x 3 2 60-x 1 if 20 ≤ x 1 ≤ 30 0 ≤ x 2 ≤ 20 -30 ≤ x 2 -x 1 ≤ -10 2625-125 2 x 1 -1 2 x 1 x 2 -1 40 x x 2 2 + 3 4 x 2 1 + 1 40 x 2 1 x 2 -1 120 x 3 1 -75 2 x 2 + 3 4 x 2 2 + 1 120 x 3 2 60-x 1 if 30 ≤ x 1 ≤ 60 0 ≤ x 2 ≤ 30 -30 ≤ x 2 -x 1 ≤ -10 7850 3 -60x 1 + 1 2 x 2 1 -40x 2 + x 2 2 60-x 1 if 20 ≤ x 1 ≤ 30 20 ≤ x 2 ≤ 30 -10 ≤ x 2 -x 1 ≤ 10 7850 3 -60x 1 + 1 2 x 2 1 -40x 2 + x 2 2 60-x 1 if 30 ≤ x 1 ≤ 40 20 ≤ x 2 ≤ 30 -10 ≤ x 2 -x 1 ≤ 0 7850 3 -60x 1 + 1 2 x 2 1 -40x 2 + x 2 2 60-x 1 if 20 ≤ x 1 ≤ 30 10 ≤ x 2 ≤ 20 -10 ≤ x 2 -x 1 ≤ 0 2400-40x 1 +x 1 x 2 -60x 2 60-x 1 if 40 ≤ x 1 ≤ 60 0 ≤ x 2 ≤ 30 -60 ≤ x 2 -x 1 ≤ -30 2400-40x 1 +x 1 x 2 -60x 2 60-x 1 if 30 ≤ x 1 ≤ 40 0 ≤ x 2 ≤ 10 -40 ≤ x 2 -x 1 ≤ -30 111000-3050x 1 +50x 1 x 2 - x 1 x 2 2 +30x 2 1 -1 6 x 3 1 -3000x 2 +30x 2 2 3000-50x 1 +x 1 x 2 -60x 2 if 40 ≤ x 1 ≤ 60 30 ≤ x 2 ≤ 50 -30 ≤ x 2 -x 1 ≤ -10 332500 3 +60x 1 x 2 -3000x 1 - x 2 1 x 2 +25x 2 1 -3050x 2 +25x 2 2 -1 6 x 3 2 3000-50x 1 +x 1 x 2 -60x 2 if 30 ≤ x 1 ≤ 40 30 ≤ x 2 ≤ 50 -10 ≤ x 2 -x 1 ≤ 20 332500 3 +60x 1 x 2 -3000x 1 - x 2 1 x 2 +25x 2 1 -3050x 2 +25x 2 2 -1 6 x 3 2 3000-50x 1 +x 1 x 2 -60x 2 if 20 ≤ x 1 ≤ 30 30 ≤ x 2 ≤ 50 0 ≤ x 2 -x 1 ≤ 30 332500 3 +60x 1 x 2 -3000x 1 - x 2 1 x 2 +25x 2 1 -3050x 2 +25x 2 2 -1 6 x 3 2 3000-50x 1 +x 1 x 2 -60x 2 if 40 ≤ x 1 ≤ 60 30 ≤ x 2 ≤ 50 -10 ≤ x 2 -x 1 ≤ 10
(5.16) (5.16) The value function V (q 1 1 , q 2 1 , x 1 , x 2 ). Since we have polynomials in x we use the x i rather than the x i notation for clocks. 1 , q 2 1 , x 1 , x 2 ) as produced by our tool Chapter 6

Modeling embedded systems with timed automata

Preliminaries

Our guiding modeling principle is to abstract away as much as possible from low-level details such as the application code itself or hardware protocols and compensate for the lack of precise information by increasing the uncertainty margins and taking this uncertainty seriously in the analysis. There will be several types of under-determination in the durations of tasks and data transfers or their arrival rates. These can be due to various origins: tentative ignorance in early development stages, true data-dependent variability in the algorithms or unmodeled variability in the architecture workload and physical conditions. Our goal is to provide HW/SW designers with a tool for rapid design space exploration, that is, given an application and architecture description with a specific deployment scheme, provide performance evaluation at early stage in the design flow. For this we provide a high level language for model description, on the top of timed automata models, which is the input for simulation and formal verification (Fig- 6.1).

Timed automata [START_REF] Alur | A theory of timed automata[END_REF] have been invented to model delays and execution times in quantitative way. We choose this formalism as a basis of our modeling framework. More precisely we use IF toolset [START_REF] Bozga | If-2.0: A validation environment for component-based real-time systems[END_REF] where the timed model is that of timed automata with urgency [START_REF] Bornot | Modeling urgency in timed systems[END_REF]. In this chapter, we present our modeling framework, while the syntax of our description language as well as the techniques used for performance evaluation will be discussed in Chapter 7.

Evaluation can be done on different metrics such as platform cost or application latency in order to compare several deployment strategies. Such criteria can be conflicting in the sense that improving one of them implies worsening the other. Initially, designers have several alternatives both in application implementation and in the choice of the target platform. Providing a way for rapid evaluation of different options at early design stages, can help them to identify weakness sooner. That's why we believe that a clear distinction has to be made between applications and target platforms, enabling a quick comparison between various combinations of implementations to evaluate trade-offs. • Applications are modeled at the task level, i.e a piece of code is modeled as a timed process. The basic unit is a job decomposed into tasks. A task is characterized by quantitative estimations of its duration and the amount of data it exchanges with other tasks. Such a description is compatible in spirit with numerous data-flow and component-based framework [START_REF] Benveniste | Data-flow synchronous languages[END_REF][START_REF] Edwards | The semantics and execution of a synchronous block-diagram language[END_REF][START_REF] Stuijk | SDF 3 : SDF for free[END_REF][START_REF] Thies | Streamit: A language for streaming applications[END_REF][START_REF] Basu | Modeling heterogeneous real-time components in bip[END_REF] advocated for writing such applications.

• Environment models the dynamics of task arrival according to some logical and timing constraints.

• Architecture is an abstraction of MPSoC including high-level performance related features such as processor speeds, bandwidth and latency of communication mechanisms, static and dynamic power consumption of architecture elements, etc.

• System specifies the deployment policy for the application on the platform, namely mapping, scheduling and buffer sizing.

Application Model

Application reflects software components and their logical interactions without considering target platforms. They are described by task-data graphs (Fig- 6.2) which are a simple generalization of the common task-graph model [START_REF] Coffman | Computer and Job-shop Scheduling Theory[END_REF]. The basis component is a task that is an atomic computational entity. Application behavior is determined by the relationship between these tasks, defining control and data flows. Control flow is represented by precedence links meaning that a task cannot start before some other tasks terminate. On the other hand, data flow specifies that data has to be communicated to a computational entity. It can be defined in two ways. In the first, a task produces an amount of data which is consumed by another task. This is achieved by adding on precedence link a quantity of data that has to be transferred between a task and its successors. However, communications are not always the results of an explicit producer/consumer scheme. A computation may need a chunk of some specific data structure for executing, like for example in image processing where images are encoded by some object and several operations work on pieces of it. The initial object is placed in some memory component, depending of the target architecture, not necessarily known when the application is modeled. For this reason, we introduce the concept of abstract data and communication task to model the fact that some task needs a quantity of data to execute, meaning that data will be transferred between the memory component on which data is initially placed and the local memory of the processing element on which the task has been mapped. Depending on the mapping of the tasks onto the architecture and the data transfer mechanism used, e.g. DMA (direct memory access) or inter-process communication, these transfers are

Task Model

A task is an atomic computational entity, similar to actors in SDF [START_REF] Lee | Synchronous data flow: Describing signal processing algorithm for parallel computation[END_REF], processing kernels or filters in streaming models of computation [START_REF] Thies | Streamit: A language for streaming applications[END_REF]. We distinguish computational tasks, reflecting the execution of some piece of code, and transfer tasks, expressing data communications. Task models are defined independently from target platform, that is, explicit deployment is specified by the system component, and implies resource immobilization and a translation of tasks attributes into duration.

A computational task is characterized by an amount of work measured by instructions or cycles. Once a task is scheduled to execute on a processor with a given frequency, its amount of work is translated into duration. At this level of abstraction it may be difficult to estimate precisely this amount. To compensate for this, we define it with bounded uncertainty. The termination of a task may be a pre-condition to the initiation of other tasks, that is, a task cannot start before some other tasks terminate and this is modeled by precedence links. Precedence is viewed as a control dependency but is also a common way to model data dependency between computational entities and can be decorated with some amount of data when tasks need to communicated a non-negligible quantity of data. Definition 6.2.1. (Task) A Task τ is defined by an amount of work w τ = [l τ , u τ ] with l τ ≤ u τ measured by instructions or cycles. When a task τ is executed on a processing element working at frequency f , its execution time is in the interval

[ lτ f , uτ f ]
A generic timed automaton for a task is shown in Fig- 6.3. Symbols ? and ! denote respectively input and output signals. For every task, its automaton stays in state Wait Pred until all its predecessors terminate (incoming signal pred). Termination of predecessors includes control Figure 6.3: Timed automaton for a task dependency of other tasks and data dependency involving communication latency. Once all precedence constraints are satisfied, the task requests a PE for an interval of workload (signal askP(l,u)). When the system component maps it to a PE (signal Start Computation) it moves to the execute state. Termination time (signal End Computation ) depends on the task workload and the PE characteristics. Notice that execution are non-preemptive, that is, once a task is mapped on a processing element, the processor is released only after the entire task terminates. Signal pred is a way to inform all successors of task termination.

Data Model

As explained in [START_REF] Jantsch | Modeling Embedded Systems and SoC's: Concurrency and Time in Models of Computation[END_REF] data is an important aspect of all models, and going from one representation of data to another representation often marks a distinctive step in the design flow. Idealized data types, such as real or integer numbers, or tokens, are useful for investigating the principal properties of an algorithm or a functionality not blurred by the maneuvers necessary to deal with concrete, implementation-oriented data types. Symbols are used to further abstract from the detailed properties of data which in reality may contain hundreds of thousands of bits arranged according to some specific structure.

We abstract data as simple data blocks which can be accessed by read/write operations when tasks are transferring some amount of data. We do not focus on any structural aspect of these data blocks. Here the use of abstract data is a way to deal with data placement, that is on which memory component data resides and to which memory component it has to be transferred. This mapping will be defined in the system component and defining abstract data is done on the application side independently from a specific architecture.

Data transfer is modeled by communication tasks which simply specify that some amount of data has to be communicated between two application components. Concrete communication realization depends on the mapping and the platform communication model e.g. DMA (direct memory access) or inter-process communication. Because some treatments, like image processing, can produce a variable amount of data, we allow bounded uncertainty on the data quantity to be communicated. Another characteristic for communication tasks is precedence as for other tasks, it models the fact that data are produced or consumed by some computational entity. The timed automaton for a communication task (Fig- 6.4) stays in state Wait Pred until all its predecessors have finished. The triggering of a signal transfer to the system initiate the transfer of an amount of data ([l, u]) from src to dst. Depending on the mapping to the target platform, this will imply more or less latency and immobilization of different components: memory, buses, DMA.

Once data has been written on target memory, the system component reports this fact by sending a signal dataAvailable which denotes the end of the transfer and signal dataAvailable is used to inform all successors.

The reason for using communication tasks is to make the model more general than the classical task graph model where data transfer are specified on precedence links. With this model, data can be communicated, not only between two computational entities, but from or to some abstract data whose placement is defined afterwards depending on target architectures.

To illustrate this consider the simple example shown in Fig- (6.5). Given this simple algorithm we would like to evaluate different implementation alternatives. At the application level, objects manipulation are abstracted using abstract data components, omitting data placement on target platform. The performance of the application on specific hardware architecture will then depend on data mapping, i.e placement of A and B on memory more or less distant from the processing element on which computation is done will give more or less communication latency. Evaluating different mapping strategies can then be done easily without changing neither application nor architecture models.

As we said previously, communication tasks are used to model communications between software components, involving data transfer between two processing entities. We can distinguish different cases: • transfer(τ 1 , τ 2 , δ ) for transferring δ bytes produced by task τ 1 to task τ 2 i.e from local memory of processor on which τ 1 has been mapped to local memory of processor on which τ 2 has been mapped.

• transfer(d, τ, l, u ) for reading pieces of an abstract data d, used by τ . Transfer is done from memory component where d has been mapped to local memory of processor on which τ has been mapped.

• transfer(τ, d, l, u ) for writing pieces of an abstract data d produced by τ . Transfer is done from local memory of processor on which τ has been mapped to memory component where d has been mapped.

The use of this kind of communication model is useful for describing dataflow concepts such as pipelining or data prefetching. This will be discussed when we present DMA communication in the architectural side.

Job Model

Components defined above are structured in a particular object named Job which is the basic unit of work whose instances arrive to be executed. Definition 6.2.3. (Job) A Job is directed acyclic graph J = (T, C, E) where

• T = {τ 1 , ...τ n } is a set of computation tasks • C = {τ c 1 , ...τ c m } is a set of communication tasks
• E is a set of ordered pairs of tasks (precedence link), defining a strict partial order precedence relation on T ∪ C Jobs instantiation depends on environment components called generators that define their arrival scheme. A job and its underlying elements are created dynamically according to generators triggering.

Jobs have been extended to allow loops modeling, that is, jobs that execute a finite number of iterations sequentially. In this case, instantiation of a new iteration is done by the job itself at the end of its own execution.

Environment Model

One aspect of scheduling which is treated differently along communities is the dynamic aspect: in classical real-time scheduling new task instances arrive periodically or quasi-periodically but these are traditionally simple tasks without precedence constraints. In contrast, job-shop and task-graph problems typically do not handle the dynamic "reactive" aspect, that is, a stream of job instances that arrive one after the other, for example, a sequence of encoded image frames or web queries. This aspect is extremely important, first because it represents the real nature of these applications and, secondly, it favors solutions based on pipelining which is the concurrent execution of tasks that belong to different job instances (see some definitions and theoretical investigations in [START_REF] Degorre | On scheduling policies for streams of structured jobs[END_REF]). One approach to treat this recurrence aspect is to use cyclic task-graphs admitting a loop from the last to the first task. While this might be suitable for modeling loops in programs where the termination of one instance enables the execution of the next one, it is not at all natural for jobs arriving from the outside, often independently of their processing by the system. To this end we use the concept of an input generator, a process that generates a timed sequence of job instances subject to some logical and timing constraints. The simplest generator is the deterministic periodic generator which produces an instance of a job repeatedly in regular time intervals. Strictly periodic generators are sometimes idealization of more time-noisy processes and we allow additional types of non-deterministic generators listed below. The environment model is not restricted to a single generator, but one can define several different generators. In all following definitions, O denotes an offset i.e the time at which the first event is generated.

Single Shot Generator

This is the simplest generator which generates only one job instance after some non-deterministic offset O, defined as a time interval. The automaton for this generator is depicted on Fig- 6.7. A job instance is created in the time interval [l, u].

Periodic Generator

A periodic generator generates an event e every P units of time. The sequence {t k } k=1...n of time stamps for the events satisfies ∀k ∈ N,

t k = O + k • P

Periodic Generator with Uncertainty

For this generator the time between two events ranges in the interval [P, P + J], that is, the time stamps t k satisfy ∀k ∈ N, t k + P ≤ t k+1 ≤ t k + P + J where t 0 = O. This type of generator ensures that two events are separated by at least P and by at most P + J time units. The time stamps of the events produces by this generator satisfy, ∀k ∈ N,

O + k • P ≤ t k ≤ O + k • P + J
Notice that we allow jitter to be greater than period in order to model bursts, a finite number of events generated, practically, at the same time. The timed automaton for this generator (Fig- 6.14) uses a counter N to enable jitter J to be greater than the period P . Each time, clock C reaches the time period, N is incremented and the next event must be generated in the interval [0, J -P • N ]. If J ≤ P then events are generated in [0, J] as shown in Fig- 6.12. Otherwise, if J > P many events could be generated in a short period. In Fig- 6.13 we can see an example where J = 2.5 × P , the shaded area shows a time frame, intersection of 3 "triggering intervals", where 3 events can be generated simultaneously. The associated timed automaton (Fig- 6.16) uses a vector of clocks of size M AX. Variable M AX denotes the maximum number of events that can be generated in any interval of length ∆. Variable first (resp. last) is used to memorize the index of the first (resp. last) clock measuring time since the generation of the oldest event in the time frame of length ∆. Variable N counts the number of events in the current time frame. Each time the first clock reaches ∆, N is decremented and the index first is incremented to the next clock. An event can be generated at any time when N < M and the time at which it has been generated is tracked by a new clock indexed by variable last. When the number of events is equal to M we wait until first time frame ended before enabling new event to be generated.

Bi-Bounded Variability Generator

For every interval of length ∆ the number of events e is at least m and at most n, ∀t, m ≤ N [t,t+∆] ≤ n. Fig- 6.17 shows an example of timeline for a bi-bounded variability generator which generate at least 2 and at most 3 events in any time interval of length ∆ (shown as blue rectangles).

Generators Characteristics

We summarize here some metrics about the different generators previously presented. Symbol ∆ represents a reference interval length and is associated with the period P in case of periodic-kind generators. M in(a)/∆ (resp. M ax(a)/∆) shows the minimal (resp. maximal) number of events that can be generated in any interval of length ∆. Finally inter-arrival Min (resp. Max) indicates the minimal (resp. maximal) inter-arrival duration between two consecutive events. Notice that we assume that interval defined by ∆ is left-closed and right-open. For example for periodic generator, considering a closed-interval, M ax(e)/∆ will be 2 instead of 1. P max(0, P -J) P + J Periodic uncertainty 0 1

P P P + J Bounded variability 0 n ∆ 0 (∆ if n = 1) ∞ Bi-bounded variability m n ∆ 0 ∆

Architecture Model

The architecture model defines the platform topology that is processing elements and memory connected through some communication infrastructure. Modeling these components is generally done with low level specification using HDL (VHDL, Verilog) or combined with software specification at system level (e.g SystemC). For rapid evaluation of different platforms or applications we argue that it is necessary to keep applications and platforms as independent as possible. We will present now, how we specify MPSoC architecture at a high level using timed automata models. Examples of different complete platforms will be shown in chapter 8, while here we focus on models for each of the components.

Processing Elements

Processors can be of any kind (general purpose, controller, DSP, ASIC . . . ) and are differentiated by their specific properties. The simplest model for a processor is defined with a frequency/speed which sets the number of cycles/instructions per time unit. The timed automaton (Fig- 6. [START_REF] Balarin | Hardware-Software Co-Design of Embedded Systems: The Polis Approach[END_REF]) for a simple processor model consists of two states, it stays in state idle until it receive compute(l,u) from a task component through the system component then it goes to state busy for a duration depending on the required amount of work ([l, u] defined as cycle or instruction number) and its frequency f (i.e [ l f , u f ]).

Power consumption is, in some situations, no less important than execution time. We distinguish energy and power as power is energy consumption per time unit. The high level power consumption characteristics of processing elements and other components can be identified [START_REF] Wolf | Computers as Components, Second Edition: Principles of Embedded Computing System Design[END_REF][START_REF] Benini | A survey of design techniques for system-level dynamic power management[END_REF] by:

• Voltage drops: The dynamic power consumption is proportional to the square of the power supply voltage (V 2 ). Therefore, by reducing the power supply voltage to the lowest level that provides the required performance, we can significantly reduce power consumption

• Toggling: A circuit uses most of its power when it is changing its output value. By reducing the speed at which the circuit operates, we can reduce its power consumption (although not the total energy required for the operation, since the result is available later).

• Leakage: Even when a circuit is not active, some charge leaks out of the circuit nodes.

Completely disconnecting the power supply eliminates power consumption, but it takes a significant amount of time to reconnect it.

As an example Fig- 6.20 shows the power state machine [START_REF] Benini | A survey of design techniques for system-level dynamic power management[END_REF] of StrongARM SA-1100 [START_REF]Intel strongarm sa-1100 microprocessor technical reference manual[END_REF] which provides three power modes, run mode is normal operation and has highest power consumption, idle mode saves power by stopping the processor clock and sleep mode shuts off most of the activity. Note that adding power consumption to the model we move beyond timed automata to the model of linearly-priced timed automata [START_REF] Behrmann | Minimum-cost reachability for priced timed automata[END_REF][START_REF] Kim Guldstrand Larsen | As cheap as possible: Efficient cost-optimal reachability for priced timed automata[END_REF] but since we are applying discrete event simulation we do not have to worry about it. In fact, discrete event simulation can be applied also to richer models of hybrid automata whose reachability problem is undecidable. Power consumption estimation will be explained in Chapter-7.

In the same spirit we define a model for handling Dynamic Frequency Scaling (DFS). This is a widely used technique aimed at adjusting computational power to application needs. It is often associated with Dynamic Voltage Scaling (DVS) enabling significant power reductions when computing demand is low. We define the model of this kind of processor with a fixed number of frequency level. For each of them one has to define corresponding power consumption information and latency for switching between different modes.

Memory

Memory can be of different types, here we restrict ourself to non banked memory (i.e reading and writing are blocking operation). Writing and Reading are separated to allow different parameters definition depending on each operation, for example, consumption can be different for reading or writing on a memory or it could be faster to read than write or conversely.

Communication

Communication is modeled through message passing. Each architectural component is modeled with some kind of network controller containing static routing table. Communication messages are injected in the architecture model by the system component, according to some application transfer task, on a specific architectural component. For example the routing table of a processing element contains informations about the path to its local memory or to a bus. All routing tables are computed statically from the whole architecture model which is simply a graph.

Bus-based Communication

The base component for modeling communication is the bus. It consists of a component which links many other components together (memory, processors). It has a finite number of communication channels allowing multiple communications do be done simultaneously.

The bus model stores communication messages in a FIFO queue and dispatches them on link of the target component through communication channels. Transferring a message has some latency depending on the message size.

NOC Communication

The topology of a network on chip specifies the structure in which routers connect IPs together. There are many different structures adopted for the NOC domains such as tree [START_REF] Guerrier | A generic architecture for on-chip packet-switched interconnections[END_REF] butterfly-tree mesh [START_REF] Pratim Pande | Design of a switch for network on chip applications[END_REF] torus [START_REF] Kumar | A network on chip architecture and design methodology[END_REF] folded torus [START_REF] Dally | The torus routing chip[END_REF] variations of the ring in octagon [START_REF] Karim | An interconnect architecture for networking systems on chips[END_REF] and spidergon [START_REF] Coppola | Spidergon: a novel on-chip communication network[END_REF] We focus here on spidergon scheme of the XSTREAM architecture [START_REF] Berenguer | xstream : Architecture multi-coeur sur puce pour des applications multimédia[END_REF]. In the spidergon topology nodes are connected by unidirectional links. Let the number of nodes be an even number Figure 6.23: Bus model N = 2 × n. Each node, i.e processing element, in the network pe i for 0 ≤ i ≤ N is directly connected to node pe j for j = (i + 1) mod N , j = (i -1) mod N and j = (i + N

2 ) mod N . An example with 8 processing elements is shown in Fig- 6.24 Figure 6.24: Spidergon topology with 8 processing elements A Spidergon topology of N nodes has 3 2 × N link and a diameter of N 4 hops. Each node has its own routing table defined statically and defines the shortest path to a target node. When a communication message arrives in a node, the router has to choose between 3 possible outcomes: the clockwise right link l r , the clockwise left link l l and the across link l a . As an example the routing table for processing element pe 0 from Fig- 6.24 can be defined as shown in Table -

Link

Target PEs l r {pe 1 , pe 2 } l l {pe 7 , pe 6 } l a {pe 3 , pe 4 , pe 5 } Communication latency is modeled with link bandwidth parameter and can be of different speeds. The energy consumption model is defined by associating a static power value to state idle (there is no communication) and a dynamic power value to state busy when the link is communicating. Communication among links is blocking, that is, when a transmission starts on a link, the next communication has to wait until the link is released for starting, and communication messages are scheduled in FIFO order on the same link in a non-preemptive manner. DMA is defined with an initialization latency each time a new transmission request is done and some dynamic latency depending on the size of the data to be transmitted. Energy consumption is defined as for other components with static and dynamic power value.

On Different Abstraction Levels

The granularity at which models are defined plays an important role in the simulation and verification steps. Given the opportunity to use different levels of abstraction even at high level of specification can be very useful. One way to use architecture model at highest level of abstraction Figure 6.27: Architecture with separate DMA for each PE Figure 6.28: DMA architecture with a shared memory for all PEs could be to entirely abstract communication architecture and is commonly the case in analysis framework ( [START_REF] Peter Vink | Performance analysis of soc architectures based on latency-rate servers[END_REF][START_REF] Ümit | An analytical approach for networkon-chip performance analysis[END_REF][START_REF] Wang | A Novel Analytical Model for Network-on-Chip using Semi-Markov Process[END_REF][START_REF] Saidi | Optimizing explicit data transfers for data parallel applications on the cell architecture[END_REF]) or in scheduling problems [START_REF] Coffman | Computer and Job-shop Scheduling Theory[END_REF][START_REF] Sinnen | Task Scheduling for Parallel Systems (Wiley Series on Parallel and Distributed Computing[END_REF][START_REF] Legriel | Meeting deadlines cheaply[END_REF] If the interface (i.e signal transmission) remains the same, then it would be simple to replace a certain bus or NoC model by another by merely replacing the corresponding timed automata. Because each component is defined by its own automaton communicating through signals interface, it would not affect the behavior for other hardware components at all. This allows easy investigation of the impact of any different network scheme that can be modeled as a timed automaton.

The simplest model could consist of modeling only processing elements and a bus component which defines the entire communication scheme. A communication task can be scheduled on this bus according to some policy and latency is proportional to the amount of data. With this abstraction, memory components are ignored and R/W operations are included in the latency model of the bus. In the same spirit, abstracting network while modeling the use of a DMA can be achieved by defining the transfer time with a more detailed function as

T (d) = I + α(p) × d (6.1)
which is inspired from [START_REF] Saidi | Optimizing explicit data transfers for data parallel applications on the cell architecture[END_REF] where T (d) represents the time needed for transferring d amount of data through the network (including memory reading and writing, DMA cost), I is some initialization latency (which can correspond to DMA or Bus initialization), α(p) is some transferring cost parametrized by the number of processors sharing the interconnect. When transfer time for a specific clock elapses the system component is informed by sending the signal dataAvailable.

In the same way we can provide more detailed models, especially for data transmission among bus components. Bus accesses are non-preemptive and multiple requests are treated sequentially, while in reality it is done in a round-robin manner, that smoothens the latency of pending transfers. This can be achieved by cutting data transfers into multiple smaller ones, and scheduling them on buses according to a round-robin scheme.

One advantage of our modeling framework is that defining different platform models can be done easily by defining a new timed automaton simulating the desired behavior according to signal arrival. We will discuss how one can extend already existing models in Chapter 7.

System Model

The aim of the system component is to characterize the deployment of an application on an architecture. This deployment is specified through mapping and scheduling definitions. We do not attempt here to find an optimal one but to provide a way to evaluate different models easily, that is comparing different scheduling strategies, evaluating an application on different architectures or several applications on a given architecture. For this reason, application and architecture are modeled independently and the link between them is done through this system component.

Scheduling consists in assigning a starting time for each task on a specific architectural component. Optimal schedulers can be sometimes computed, on simplified models, under deterministic behaviors. One might be interested in evaluating them while admitting uncertainty. A schedule can be computed according to different criteria such the overall termination time, the overall energy consumption, the overall communication time, architecture cost, etc. Considering opposing criteria there is no unique optimal solutions but rather a set of incomparable trade-offs.

One has to define several system components depending both on application and architecture (Fig- 6.30). Abstract data need to be mapped initially on concrete memory components, computation tasks need to be scheduled with some scheme on processing elements and transfer tasks have to be scheduled on the network (maybe initialized by some component like processor or memory). Task scheduling can be done according to different schemes which can be local to one processing element or global to all of them. We will present in the following those that we have implemented. Adding new scheduling policies can be done easily by writing the scheduler as a timed automaton. Notice that for all following schedulers we assume that the latency of the scheduling operation itself is negligible.

FIFO Scheduling

Tasks are pushed into processing elements according to their arrival order. One can choose a global scheduling with one global FIFO queue, where tasks are mapped to the first available processor (Fig- 6.31). In that case, task deployment is done dynamically during execution and task instances could execute on different processing elements. Another way to use FIFO scheduling is to define a fixed mapping, i.e each task is assigned a specific processing element and each instance will execute on it. For that we define one FIFO queue for each processing element and tasks are pushed in queues according to a mapping table (Fig- 6.32).

Fixed Priority Scheduling

Fixed priority scheduling is an extension of the FIFO policy. Each computation task is associated with one PE and a fixed priority, several tasks can have the same priority so that they will be executed according to FIFO scheduling. FPS is implemented by using a priority table, i.e. there are a finite number of priority queues and each one is popped according to FIFO policy when all queues of higher priority are empty. Each time a computation task wants to acquire the PE it is put in its corresponding priority queue. As for FIFO schedulers, one can define FPS globally or locally.

Strict Priority Scheduling

It is a way to model static scheduling where the schedule is defined deterministically, i.e the task ordering is fixed and known before execution. Static schedule are given as a list of triples (τ i , t i , p i ) saying that task τ i will start at time t i on processing element p i . That can be interpreted as priority assignments on tasks that ensure the same execution order.

Each computation task is associated with one PE and a strict priority and each task mapped on the same PE has a different priority. For each PE all associated tasks will be executed according to a strict order. Each time a computation task wants to acquire the PE it is put in a waiting list and has to wait until all higher priority tasks have been executed.

Frequency Scaling Scheduling

Each computation task is associated with one PE , a fixed/strict priority, a starting frequency/speed to which the PE will switch before the beginning of the computation. Optionally an ending frequency/speed can be specified enabling switching at the end of the computation. This can be used, for example, for halting a PE after some computation.

Evaluation

The aim of this modeling framework is to provide design space exploration for performance evaluation. This is achieved by composing all automaton (application, environment, architecture and system) to yield a global timed automaton which captures the semantics (all behaviors ) of the system and this is the object of our various methods of analysis and simulation. For that we need a way to specify performance metrics that have to be measured. We focus here on property checking, that is how to ensure that some property is not violated. Quantitative evaluation will be done by statistical analysis on simulation traces and will be discussed in chapter 7.

Observers

For property verification with reachability analysis we use the concept of observers defined in the IF toolset that we have presented in chapter-3. Observers express in an operational way safety properties of a system by characterizing its acceptable executions sequences.

An example of property we are interested in is response time. We want to ensure that a job or a task always meets its deadline. For that we define an observer that monitors job/task behavior i.e it create a clock when the task becomes active and leads to an error state if the task does not finish until some specified deadline. The observer for this property is depicted in Fig- 6.33. In case of violation we can retrieve a trace of the execution leading to this state. We present trace generation in more detail in chapter 7. They include computation and data transfer tasks encapsulated into jobs on the application side, input generators that model job arrivals, architecture components such as processors and busses as well as deployment (mapping and scheduling) policies. All those components are translated into a unified semantic models of timed automata whose composition provides the model for the various performance evaluation methods. As is also described in Chapter 7, one can add new models, or refine existing ones to be more detailed, at relatively small investment. The effect of model refinement on the feasibility of analysis depends and the method used and is, of course, more significant for methods based on verification (reachability computation) than for simulation-based techniques.

Chapter 7

Realization: The DESPEX Tool

In the context of this thesis we developed tool for performance evaluation at early design stage, called DESPEX (DEsign SPace EXplorer). According to [START_REF] Edwards | Readings in hardware/software co-design[END_REF], a formal model of a design should consist of the following components:

• A functional specification of the system;

• A set of properties that the design must satisfy;

• A set of performance indices that evaluate the quality of the design (cost, reliability, speed, size);

• A set of constraints on performance indices.

We will discuss in this chapter how the above components are implemented and how one can use the tool for rapid design space exploration.

General architecture

Evaluating performances of an application on a given platform starts with the specification of the whole system. We provide a description language dedicated to this purpose. Users have two alternatives to describe an abstract MPSoC model, by using either textual or graphical modeling language. Once the model is defined, automatic translation to timed automata is performed by generating IF code. The IF code is then compiled using the IF toolset and provides an executable model on which one can perform reachability analysis or simulation. The result of such analysis is a timed trace on which several processing can be done such as graphical visualization or statistical analysis. Simulation results can be saved by automatic report generation in various formats. We will discuss in the following how the different steps, shown on fig- 7.1 are done. We provide a command-line tool chain and a graphical user interface. The tool consists mainly of 25K lines of C++ code, developed with a concern for easy scalability, using established software design concepts.

Model description

Performance analysis is based on models which are generally defined using some specification language. We developed a textual language for modeling MPSoCs and applications at a high level of abstraction. An aim of this language is to remain as generic as possible while being easily expandable. As shown in chapter 6, our model is structured in four parts: application, environment, architecture and system. Each of their components is specified by a set of high level characteristics influencing timed automaton behavior. This can be viewed as hierarchical components defined with typed parameters. Fig- 7.2 shows this hierarchy for application and environment components. -Communication tasks are characterized by a quantity of data to be transferred from a source to a destination -Precedence links models precedence constraints over entities and can be labeled with a quantity of data to specify data flow.

• The environment is specified using input generators characterized by particular parameters that define triggering scheme (period, jitter . . . ) .

• The architecture is specified by a graph structure connecting the following components with specific parameters:

-Processor: frequency, power consumption values.

-Memory: R/W rate, access latency, power consumption values.

-Bus: bandwith, access latency, power consumption values.

-DMA: access latency, power consumption values.

• The system is defined by:

-A list of local schedulers depending on the number of processors within the platform, or by a global scheduler. Each scheduler is typed according to its policy and is characterized by a mapping table, which associates tasks with processors.

a list of data mappers that associates abstract data with memory elements.

Concretely, the implementation of this model relies on what we call abstract model, allowing genericity and easy scalability of our modeling framework. The abstract model provides independently from the factual model, basic operations for parsing a textual description, edition through a graphical user interface (GUI) or exploration. We present, in the sequel, its structure more in detail.

The abstract model defines generic hierarchical objects on which basic operations can be applied. Basically, it is structured as a generic hierarchical graph pattern, on which textual description is built. We implement an abstract component as an object with generic parameters and possibly containing other components based on composite design pattern. Basically, the implementation is based on Model-View-Controller (MVC) design pattern. Any textual description that follows the grammar defined above, can be read by the parser. Therefor, object assignment is managed by a factory component. Model exploration uses a visitor design pattern, that gives the ability to add new operations to existing structures without modifying those structures. Visitors are used for different processing like timed automata generation, textual printing of the model or for graphical viewing.

Graphical language intends to help users describe models in a graphical style, like Statecharts [START_REF] Harel | Statecharts: A visual formalism for complex systems[END_REF] or UML [START_REF] Rumbaugh | Unified Modeling Language Reference Manual[END_REF]. We provide both a textual language and a graphical language for model specification. An overview of the graphical interface editors is shown in Fig 7 .7 and Fig 7 .8. The graphical interface, written using Qt [START_REF] Blanchette | C++ GUI Programming with Qt 4 (2nd Edition)[END_REF], works directly with the abstract model, that is, each abstract component is associated with a different graphical view which allows model edition. The reason for working on the abstract model is the same as for the textual language, it gives more genericity, that is, the GUI is not only dedicated to a specific language, but language extension does not imply much implementation work.

Graphical views depend on component or parameter type. A composite component is defined through a scene editor in which one can add some other components by pushing graphic items. Components parameters are viewed and editable through dedicated items depending on their type and are collected in a treeview. As for the textual language parser, a factory component is responsible for graphical objects creation.

Property Definition

The evaluation of a model is done by estimating performance indices. By specifying constraints on those indices, one can perform reachability analysis to check whether the model satisfies a set of properties. As explained previously, these properties are encoded as timed automata observers and can also be used during stochastic simulation. In that case, they are assimilated to monitoring processes, close to the work done in [START_REF] Nickovic | Amt: A property-based monitoring tool for analog systems[END_REF] using a temporal logic front-end. Timing behavior can be described by the time interval between a specified pair of events. A property on such interval is then defined by associating a deadline constraint. On the other hand, statistical estimation on these intervals, is provided by stochastic simulation and trace analysis.

We provide an XML-based language for properties specification, as constraints on time intervals between start and end events, in timed automata models. An example of definition for the response time of a job is shown in Listing-7.1 and the language grammar is shown on Fig- 7

Model Extension

The model can be easily extended with minimal programming effort. Adding new parameters is the simplest operation, consisting simply in adding them in a concrete object and will automatically be propagated in graphical views and in the textual language without any reprogramming.

Adding new components consists in defining a new object deriving from any abstract component and some coding is required in the various component factory. Finally, a timed automaton for the new component has to be provided in the IF printer.

Translation to Timed Automata

Once specification is done, we provide automatic translation to timed automata by generating IF code. Each component is associated with a timed automaton communicating via signals. One can see the overall architecture as a library of timed automata and extending or adding new component in the model implies defining its corresponding automaton as an IF process properly managing input and output signals. if specified generate simulator for reachability analysis otherwise simulator is compiled for stochastic simulation -p <file> :

properties file input

This generates an executable simulator.x, if option -a is not specified, simulator.x is compiled with all needed library for stochastic simulation including random number generation utility.

Reachability Analysis

The goal of reachability analysis is to check whether some properties are satisfied or not. For a given model and a property we construct an observer, an automaton that monitors the global behavior and reports an error on property violation. The verification process consists of exploring the state space of the product system. In case of property violation, one get an error trace which can be visualized with our tool to give designers a better understanding on components behaviors that leads to an undesirable state.

In the same spirit as observers we use observer variables to store some specific values, like worst case response time of a job, during the exploration process. These variables are simply defined as static global variables and are not part of the state variables, i.e they do not influence system dynamics. For example, to get the worst case response time of a job, we can use an observer automata (DPA) is investigated theoretically in Chapter 4 and 5 while here we focus on using it for simulation based statistical analysis. The idea, here, is to define a random variable for each uncertainty interval, and to replace every guard which is in the form of interval by drawing from the random variable. To illustrate this, consider the automaton of Fig- 7.14. Clock c, which is set to zero upon the start transition, measures the time elapsed since the activation. This start transition is instantaneous and can be initiated by some external supervisor. The timing of leaving state q is based on the clock value and the temporal guard φ(c), which is simply the condition c ∈ [l, u]. In the stochastic model, we associate a probability density with the duration of such step, which is technically expressed as the distribution over the values of clock c when we leave state q . We use a slightly modified (but equivalent) version of the basic automaton, as shown at Fig- 7.15. Rather than having the start transition deterministic and delegating the non-determinism to the end transition, we use an auxiliary variable y which is assigned non-deterministically upon start and which should be equal to c upon end. In the set-theoretic setting this means an assignment y ∈ [l, u] while for stochastic model this means drawing a value for y according to distribution φ, which we denote by y := φ(). Models remain the same as those used in reachability analysis except for timing transitions that are translated into stochastic ones. Random variables associated with intervals are uniformly distributed in our model. This choice was made because it is the simplest one, and at the level of abstraction on which we work, it may be difficult for designers to estimate precise characteristics. Based on past experiences it seems quite easy to give lower and upper bounds, but without further information on how it may be distributed between them, uniform distribution could be considered as a good assumption. In the case where more information is available one can define other bounded-support distributions. For example, finding precise values for number of cycles in a task can be a difficult work at early design stage. One can estimate lower and upper bounds or if it is possible one can discretize the distribution by splitting interval into smaller one as depicted on Fig- 7.16. Concretely, we extend the IF toolset with random number generators that performs correctly according to given probability distribution. Since we want to be able to compare, by statistical simulation the performance of different deployments of the same application with the same distributions on duration, we should be careful to ensure experimental repeatability and sample the random variables in a way which is independent of the order of execution of different tasks. Because of the use of a random number generator, this will not happen if we draw the duration just before we start the task. Instead, we draw from all the duration random variables at initialization time, and repeat the same values when we compare deployments.

Command Line Usage

Running a stochastic simulation is done by: simulator.x -simDuration <num> -savesim <traceFile> -simDuration <num>:

simulation length where <num> is in tick unit -savesim <traceFile>: generated trace file

Graphical Interface Usage

Simulation and reachability analysis can be done through the GUI. One can do interactive or step by step simulation and visualize timed traces on the fly or offline for error traces resulting from reachability analysis. Fig- 7.17 gives an overview of the tool capabilities.

Timing Evaluation

To properly design an embedded system it is important to understand the effect that scheduling has on system performance. Scheduling analysis calculates worst-case and best case task response times, i.e the time between task activation and task completion. Worst case response time can then be compared against deadlines. We have seen that computing worst case response time or checking deadlines can be achieved with reachability analysis. In addition to the best-case, worstcase bounds, it can also be very helpful to know how response time is distributed between bounds. This is achieved by statistical analysis of traces from simulation. Typical statistical measures are:

• State distribution for components (ex: processor or bus utilization)

• Response time distribution, mean, maximum and minimum values.

• Latency (bus access, memory R/W . . . )

These measures are done according to properties specification, defined as timed intervals. For each interval, we get general statistical information like maximal, minimum and mean values together with probability distribution as shown on Fig- 7.19.

Power Consumption Estimation

Recall that power information transforms the timed automaton into a linearly-priced timed automaton [START_REF] Behrmann | Minimum-cost reachability for priced timed automata[END_REF][START_REF] Kim Guldstrand Larsen | As cheap as possible: Efficient cost-optimal reachability for priced timed automata[END_REF] whose analysis is implemented in UPPAAL [START_REF] Behrmann | Efficient guiding towards cost-optimality in uppaal[END_REF] but not in IF. For this reason (and also due to scalability) we avoid reachability computation and focus on simulation. Energy consumption estimation is done via trace analysis. Each state of an architecture component is associated with a power value. So we can derive from a simulation trace the energy consumption for each component. Let δ s i be the time duration between entering and leaving state s i and P s i be the power value associated with state s i . The energy consumption for a component C j is then

E C j = s i δ s i • P s i
and the mean power for component C j is

P C j = E C j δ sim
with δ sim is the simulation duration. The energy consumption E S and mean power P S for the whole system are given by:

E S = C j E C j P S = C j P C j
Complementary we can estimate maximal power as max t (

s k P s k )
with s k all enabled state at time t.

As an example Fig- 7.20 shows energy consumption proportion between hardware components and power of the whole system during time on Fig- 7.21.

Statistical Evaluation with TraceNavigator

The first functionality of TraceNavigator is to provide trace visualization as shown on Fig- 7. [START_REF] Baier | Model-checking algorithms for continuous-time markov chains[END_REF]. In addition, it gives a view of quantitative estimation for a given set of metrics like power consumption of different hardware components (Fig- 7

Case Studies

In this chapter we demonstrate the application of the tool to several examples. We show first on a synthetic example how temporal uncertainty influences performances analysis. We then present two case studies: an evaluation of various alternatives for an image processing application and the deployment of a radio sensing application on an embedded platform.

Reachability vs. Corner-Case Simulation

This section will demonstrate on a simple example that an analysis based exclusively on worst case execution times might not catch the worst case behavior.

Model Description

The application consists of the task graph of -8.1 (for simplicity we normalize processors speeds to 1). We assume one instance of this job produced by a single-shot generator at time 0. We assume a FIFO scheduler for each processor which executes, without preemption, the appropriate tasks in the order they become enabled.

Analysis

For that example, the property to verify is that the response time of the task-graph does not exceed 20. We first do analysis based on deterministic values (lower and upper) and then show some results using non-deterministic workloads for computation tasks.

Worst Case Analysis

We take the application model with a deterministic workload for each task. It is common to take the worst case execution time for each task in Table-8.1, in order to get a worst scenario for the whole execution. The analysis gives a response time of 19 time units which is less than the deadline [START_REF] Basten | Model-driven designspace exploration for embedded systems: the octopus toolset[END_REF]. The execution trace is depicted in Fig- 8.3. Colors are associated with component states, executing in red, waiting for predecessors in purple and waiting for the processor in yellow. Based on this result, one might conclude naively that the timing requirement is satisfied because the worst case response time is under the deadline.

Best Case Analysis

Likewise we could take the best case for each task from table-8.1 in order to get an estimation of the best scenario. The analysis gives a response time for the task graph of 13 time units. The execution trace is shown on Fig- 8.4. Based on worst case and best case analysis one might therefore conclude that response time will be in [START_REF] Asarin | Timed regular expressions[END_REF][START_REF] Balarin | Hardware-Software Co-Design of Embedded Systems: The Polis Approach[END_REF] and so the timing requirement is satisfied. We see that lower and upper bounds on task durations do not allow us to infer the correct bounds on the response time for this particular example. If this application is executed in a safety critical environment, with hard real time constraints, conclusion of the analysis is that the deadline can be violated. However, in case of soft real time constraints, QoS (Quality of Service) evaluation in a quantitative way is more appropriate.

Quantitative Estimation

In addition to bounds on execution time, it can also be very helpful to know how the response time is distributed. To get more quantitative informations we use stochastic simulation in order to answer questions like: what is the mean response time? What is the probability that the response time is greater than 20 time units?

For the purpose of this quantitative estimation we make the hypothesis that the execution times are uniformly distributed in the intervals. We draw 10000 duration vectors randomly and perform

Summary

With this simple example we have shown that analysis based on local extremal values (lower and upper) might give incorrect bounds on the global response time. On the other hand timed automata reachability analysis gives us the correct bounds, but no quantitative information about the distribution of values between them. In the case where timing constraints are not critical such pessimistic estimation can lead to over-designed and under-utilized systems, thus resulting in unnecessarily increased costs. Moreover, stochastic simulation does not catch tight bounds but gives more useful quantitative information about average performance.

Video Processing on P2012

Platform 2012 (P2012, [START_REF] Stmicroelectonics | Platform 2012: A many-core programmable accelerator for ultra-efficient embedded computing in nanometer technology[END_REF]) is an ongoing project of ST Microelectronics (the largest European semi-conductor manufacturer) and CEA-LETI to develop a multi-core architecture to serve as an accelerator (computation fabric) for high throughput computational tasks (video processing, radio sensing, image analysis) for embedded (smart phones) and other (TV set top boxes) devices. P2012 is viewed as an alternative to GPUs as a replacement of dedicated hardware currently used for these functions. The flexibility and productivity gains of software are supposed to compensate for a tolerable degradation in performance compared to hardware. However, writing parallel software is not a trivial matter and deploying it efficiently on the multi-core platform (mapping, memory allocation, scheduling of computations and data transfers) is a hard combinatorial optimization problem with a significant variations in performance over its feasible solutions.

STMicrolectronics has defined a benchmark based on typical applications in the context of P2012. It is an augmented reality application called FAST (Features from Accelerated Segment Test). This application was developed and parallelized on P2012 virtual architecture and a sequential version (set as reference and easier to analyze) was given to us. In this section we demonstrate the applicability of our tool in exploring and comparing different deployment solutions for this application.

We will use two variants of the application and of the P2012 architecture to demonstrate the functionality of our tool. All these experiments should be taken with a grain of salt concerning their realism since the development of P2012 and its applications was in a stage where models were very approximate. The main purpose of the exploration is to illustrate the types of analysis provided by our framework.

Model description

The P2012 Platform Merely, P2012 is a many-core computing fabric based on multiple clusters. Clusters feature up to 16 processors sharing multi-banked memories, a DMA engine and are connected via a highperformance network-on-chip. In the context of this case study we restrict our models to one such cluster.

The model of P2012 architecture used in this section is shown on Fig- 8.8. It consists of 16 processing elements sharing a local memory and connected through a bus which models the actual network-on-chip. The entire cluster is connected to an external memory via another bus and a DMA engine is used to communicate data between local and off-chip memories. In the context of this case study we explore different alternatives by playing with the number of available processors and their frequency parameters to have a picture of their influence on performance.

FAST Algorithm Presentation

The FAST algorithm, developped by Edward Rosten et Tom Drummond [START_REF] Rosten | Machine learning for high-speed corner detection[END_REF], is a corner detection method, used to extract feature points and later used to track and map objects in many computer vision tasks. It mainly consists in computing the detection (function circular detection) on a chunk of an image. From an architectural point of view, the image resides initially in the off-chip memory and has to be brought to local memory and dispatched to the processors for execution.

The whole image does not fit into the local memory inducing several alternatives for its splitting and transfer to local memories. For our case study, we consider two different implementations one based on bands and one based on blocks.

Band Treatment

This approach consists in dividing the image into bands and bringing each band to local memory, then available processors work on different parts of this band. The number of parts will depend on the number of processors available in the target platform. Fig- 8.9 shows this splitting with 8 available processors. After computation is completed for the entire band, a synchronization is done between all working processors and the result for the whole band is stored on off-chip memory.

We model this algorithm with our tool as a task graph (Fig- 8.10). The entire image is modeled as an abstract data and nodes read and write are communication tasks for accessing the data. Task split and join model the synchronization process. This task graph represents the computation of one band. Notice that the task graph is cyclic, that is it executes a finite number of iteration, corresponding to the number of bands, for the computation of the entire image. In this case study the size of a band is kept fixed.

Blocks Treatment

The second version consists in dividing the image into blocks directly and each read/write operation is done independently for each available processor. An abstract model of this second version can be represented by one task for reading data, one for computation (circldetect task) and one task for writing data back. This model, depicted in Fig- 8.11, consisting in several jobs, each dedicated to the computation of each block. Notice that as for the first model, each job does several computations sequentially, that is the start of an iteration is triggered by the end of the previous one until the whole image has been processed.

Parameters Estimation

In order to perform analysis, one has to specify parameters such as computational workload for tasks and quantity of transferred data. Profiling of the sequential implementation showed us that the main computation is done by the circular detection function and all other functions have negligible workload. This is why our model contains only one computational task. Based on the sequential implementation we were able to extract workloads for the computational tasks, i.e, minimum and maximum number of cycles needed for the treatment of one pixel. Based on those values, we compute estimations for the execution of one block of pixels depending on its size. In our model, those execution vary up to 20% around the mean value. Note that the size of the output is 6 times larger than the size of the input.

Analysis

Worst Case vs Statistics

Consider the first implementation depicted by the task-graph of Fig- 8.10 which represents the treatment of a horizontal band (16 blocks) of the image. All the blocks are fetched by a single read command and the data is split onto 16 tasks whose output is merged and written back to the offchip memory. Execution times for processing a single block admit roughly up 20 % deviation from their average.

We first run a timed automata (TA) based analysis of the execution of this job on architecture instances with various numbers of processors to obtain the respective lower-and upper-bounds on execution times. Then we apply statistical analysis, based on 100 random simulation runs. Fig- 8.12 shows a histogram of these runs for different number of processors. Note that when there is one processor per task, the average is close to the worst-case (for that configuration) because the total termination time is defined as the max of individual task termination times. On the other hand, when the number of processors is smaller and some tasks are executed sequentially, the convolution effect renders the distribution more normal-like. Analysis and simulation results are summarized in Table-8.4.

Reading Granularity

We make a comparison between the previously mentioned strategies for fetching the data based on bands and blocks. We assume here, an image made of 256 blocks and a band consisting of 16 blocks for the first strategy with associated task graph is depicted in Fig- 8.10. The second one is an alternative specification where each block is read separately (Fig- 8.11). The whole job for 256 blocks is represented by sequential concatenation of 16 copies of the basic task-graphs.

Fixed vs Flexible Mapping

Next we move to a situation where there is a very large variability in the execution times of the tasks, namely [START_REF] Milner | A Calculus of Communicating Systems[END_REF]2100], and compare a fixed mapping with a local FIFO scheduler for each PE against a flexible mapping by a global scheduler on an instance of P2012 with 4 processors. We take the task graph of Fig- 8.11 and use a periodic event generators with jitter. Using 4 processors, each PE is assigned 4 tasks (exactly for the fixed mapping policy and approximately for the flexible policy) and hence the worst-case execution time for a job instance is around 8400. For arrival periods which are smaller than the worst-case execution time, a worst-case analysis naturally shows the possibility of an unbounded accumulated backlog and, hence, unbounded latency. We perform simulations with arrival periods 7000, 6000, 5000, and 4500. Not surprisingly, the global strategy yields a much better average performance and its advantage increases with the arrival rate. Decreasing the period to 4000 (below the average execution time) leads to frequent overflows.

Power Consumption

In the last experiment we compare different configurations of P2012 for the trade-offs between response time and power consumption that they provide. We consider again a job consisting of a concatenation of 16 copies of the task graph of Fig- 8.10 and execute it on instances of the architecture with 1, 2, 4, 8 and 16 active processors, all running in either 200, 400 or 600 MHz. For each configuration we run 100 simulations and compute the average response-time and consumption. Fig- 8. [START_REF] Asarin | Controller synthesis for timed automata[END_REF] shows the trade-offs obtained. Such plots are extremely useful for detecting regions where power consumption can be significantly reduced with a modest performance degradation which still meets the system requirements. For example several configurations (16PE-600Hz, 16PE-400Hz, 8PE-600Hz) give a response time around 100 ms with consumptions ranging over [400, 640] mW. Opting for configurations such as 16PE-200Hz, 8PE-400Hz or 4PE-600Hz reduces power consumption, on average, by 2 while the response time is very slightly degraded.

Summary

We have demonstrated how DESPEX can be used to solve very realistic problems in design-space exploration, quantify the performance differences between different design choices and represent available cost/performance trade-offs.

A Radio Sensing Application

Finally we demonstrate how the tool was used for evaluating a radio sensing application developed by Thales. The goal of this case study was to check the feasibility of porting the application, currently running sequentially on a powerful desktop, to an embedded multi-processor platform.

This case study demonstrates more the power of the methodology supported by our tool framework than performance itself. Porting a sequential implementation onto an embedded system involves several difficulties. The ability to perform rapid design space exploration at early stages is a key to identify difficult issues as soon as possible. Depending on the availability of simulators at different level of accuracy, models are then refined and DESPEX fits well into the classic Y-chart based design space exploration [START_REF] Kienhuis | A methodology to design programmable embedded systems -the y-chart approach[END_REF] presented in Fig- 2.4 of Chapter-2.

Model Description

The application was evaluated on the P2012 platform [START_REF] Stmicroelectonics | Platform 2012: A many-core programmable accelerator for ultra-efficient embedded computing in nanometer technology[END_REF] described previously and the xSTream platform [START_REF] Berenguer | xstream : Architecture multi-coeur sur puce pour des applications multimédia[END_REF]. As shown in Fig- 8.17, the xSTream architecture is defined as a computing nodes fabric connected to a system bus. Each node admits a processing element (xPE) and has its own local memory (LM) and communicates through a high-performance network on chip (xSTNoc). Note that the processing elements of the two architectures belong to the same ISS family.

Radio Sensing Application

Sensing is one function of cognitive radio. A cognitive radio is a transceiver which automatically detects available channels in the wireless spectrum and accordingly changes its transmission or reception parameters so that more wireless communications may run concurrently in a given spectrum band. According to [START_REF] Akyildiz | Next generation/dynamic spectrum access/cognitive radio wireless networks: A survey[END_REF] the main functions of cognitive radio are:

• Sensing: detecting unused spectrum and sharing the spectrum without harmful interference with other users;

• Management: capturing the best available spectrum to meet user communication requirements;

• Mobility: maintaining seamless communication requirements during the transition to a better spectrum;

• Sharing: Providing the fair spectrum scheduling method among coexisting users.

We focus on sensing which consists in two steps: extraction of the spectrum (GSM in this example) and then extraction of the different channels inside the spectrum (200 in GSM).

For this example we consider one step of the sensing function, the so called characterization that consists in several operations such as transposition, quantification and filtering on chunks of the signal to be processed. Splitting of the signal is done according to [START_REF] Yi | Ccs + time = an interleaving model for real time systems[END_REF]

Parameters Estimation

Parameters have been estimated using an Instruction Set Simulator (ISS) provided in the context of the ATHOLE project. That is, workload and amount of produced data are obtained for each function after instrumentation and execution of the concrete C code . Note that the results obtained for the PE of xSTream can be extrapolated to the PE of P2012 due to similarity. This work shows that the sequential implementation is easily parallelizable and MPSoCs can, in principle, be a solution to execute this kind of application. However, the modeling and analysis effort has revealed that the amount of data transfer is huge and memory capability of embedded architectures can be a bottleneck. Actually, the application is highly parallelizable because the same computation is done on different chunks of data, nevertheless the workload required depends on the size of the blocks, currently limited by local memory capacity.

Evaluation

According to the analysis performed with DESPEX, the application in its current form cannot be ported to MPSoCs such as xSTream and P2012 while providing a real-time response. One conclusion from this experience is that porting to embedded devices requires re-design of the Methodologically, this case study demonstrates the advantage of separating as much as possible the models of the architecture and the platform. We have profiled the tasks on the processor of xSTream and could use the numbers, slightly calibrated, to estimate their execution time on P2012 (featuring processors of the same ISS family) and evaluate the overall execution time on the new architecture without much effort.

Summary

With this example, we have shown how our tool can fit into classical design flow for rapid design space exploration. The modeling and re-design effort needed for using our tool, may serve for detecting bottlenecks (such as memory data transfer) at early design stage. Such re-design is, anyway, an unavoidable step in rewriting the application for parallel execution. Once parameters have been extracted correctly, models can be used for evaluating several configuration in short time without having to wait the availability of accurate system-wide simulators.

Chapter 9

Conclusions and Future Work

This thesis constitutes a contribution to the important problem of designing embedded multi-core architectures and efficiently deploying application programs on these platforms. We have provided a tool-supported methodology for high-level modeling of the major components that participate in the execution: hardware architecture, application program, external environment and mapping/scheduling policies. These models abstract away from many low-level details of the program and the architecture and provide for rapid simulation and performance evaluation, as a complement to the more detailed and accurate models used in the development process. These models are then translated into timed automata and are analyzed by complementary techniques that include standard timed automata reachability, Monte Carlo simulation and analytic calculation of performance indices. The modeling framework and analysis techniques have been implemented into an extensive and extendible toolset, DESPEX, the design-space explorer, featuring many important functionalities. The tool, which served as a major deliverable in an academic-industrial collaborative project, has been applied to several interesting case studies.

From a theoretical standpoint, we provided novel ideas and results concerning analysis and scheduler synthesis for continuous-time stochastic processes where task durations are distributed uniformly over a bounded interval. Compared to exponential "memoryless" distribution often treated in the literature, for our distributions the clock values which represent the time elapsed since the beginning of each active step, influence the temporal probability of future events. Hence, analyzing such systems required several conceptual innovations including the delegation of timing uncertainty into the duration space to facilitate volume computation and the definition of density function families parameterized by clocks values. Realizing the proposed algorithms required an implementation of a specialized integration package.

As for the future, we foresee numerous research directions in all dimensions of this work: theory, implementation, methodology and application. We list a few of them below.

• The tool itself, like all tools developed within a project and a thesis, will require a major re-design and implementation in the future before it could be given at the hands of real users. 1 Such modifications include the improvement of the translation of components into timed automata, accelerating the simulation (currently performed on top of IF which is not optimized for such simulations), compacting the generated traces which are currently too verbose and improving the user interface.

• From a methodological point of view, a more systematic way to populate the high-level models with performance numbers should be developed. It should be based on a combination of profiling the available components by low-level simulation and interaction with the user in the style of decision-support systems. In general, a tighter integration with the software development flow (which is still under construction for multi-core systems) is needed.

• On the application side, our ambition is to see DESPEX adapted and applied more extensively to P2012 in the framework of a new forthcoming project. This will involve more refined modeling of the specific components of the architecture as well as a tighter integration with the software development process for this platform. It should be noted that the application and architecture concepts developed here are not restricted to the scale of MPSoCs, and the problematics of finding the right balance between computations and data transfers can be found in other scales such as distributed or scientific computing.

• On the theory side, the work on optimal scheduler synthesis is still incomplete. The exact form of the boundaries in the decision space between the domains of the different actions should be characterized and an approximation algorithm with guaranteed bounded error should be implemented. Synthesis itself (in the sense of scheduler/controller synthesis) is an open unsolved problem in terms of complexity, and some of the ideas developed in this part can be used to find a more compositional way to achieve it. Finally, a more thorough comparison of the computational trade-offs between analytic and statistical methods will help in assessing their relative advantages and shortcomings.

taken in (q, x ) can lead to a state at least as advanced as the state reached via the same action from (q, x). For an immediate start transition this is evident. Suppose we take action w at (q, x ) and (q, x). Then there are three possibilities: if the race winner at (q, x ) is some P i , i = i, taking an e i transition to q , then the same P i will win the race from (q, x) within the same time, landing in q with value of x i less advanced by δ and the inductive hypothesis holds, see Figure Suppose, on the contrary, that P i , the process whose clock is more advanced in x than in x, wins the race from (q, x ) within t time. If P i is also the winner from (q, x), the e i transition will be taken by ξ x after t + δ time. By waiting at q for δ time, run ξ x can reach the same state as ξ x , see

ξ x : (x i + δ, x i ) t -→ (x i + δ + t, x i + t) e i -→ (⊥, x i + t) δ -→ (⊥, x i + t + δ) ξ x : (x i , x i ) t+δ -→ (x i + δ + t, x i + δ + t) e i -→ (⊥, x i + t + δ).
Finally, suppose the race winner from (q, x) is P i within some t + δ time, δ < δ, leading to state q . This splits into two sub-cases. If at q the run ξ x does not start a new step, then, by waiting at q for δ -δ time, ξ x can reach within t + δ the same extended state that ξ x has reach in more time t + δ: If, on the other hand, during the interval of duration δ -δ in which ξ x catches up with the progress of ξ x in P i , ξ x makes an s i transition to start a next step of P i , so can ξ x and they will reach the same state:

ξ x : (x i + δ, x i ) t -→ e i -→ (⊥, x i + t) δ -→ (⊥, x i + t + δ )
ξ x : (x i + δ, x i ) t -→ e i -→ (⊥, x i + t) δ -→ (⊥, x i + t + δ ) e i -→ s i -→ (⊥, 0) δ-δ -→ (⊥, δ -δ ) ξ x : (x i , x i ) t+δ -→ e i -→ s i -→ (x i + δ + t, 0) δ-δ -→ (x i + δ + t, δ -δ ) e i (⊥,δ-δ ).
-→

These two cases are illustrated in Figure A.1-(c).

The bottom line of this case analysis is that for every action taken in (q, x) and (q, x ) and for every y, there exist durations t y and t y , such that 0 ≤ t y ≤ t y , a state p y such that q ≺ p y and clock valuations z y and z y such that z y ≤ z y in the value of one clock (as in the premise of the lemma) and (q, x) ty -→ (p y , z y ) and (q, x ) Since the cost to go from (q, x) can be written as V (q, x) = ψ(y) • (t y + V (p y , z y ))dy and since for every y, t y ≤ t y and V (p y , z y ) ≤ V (p y , z y ) by the inductive hypotheses, we have V (q, x ) ≤ V (q, x). Note that although the lemma can be interpreted as saying that always a more advanced state has a better value, this is true in general only for progress that does not increase the possibility of blocking due to resource conflicts. Advancing the clock of an already-active step, or starting a step on a resource that has no other future users are such forms of progress while starting a step on a resource that has other users in its horizon is not. Otherwise, FIFO schedulers were always optimal. Proof of Theorem 3: Imagine a strategy Ω which is lazy at (q, x) and takes its earliest start at (q, x + t), as illustrated in Let us repeat that the theorem does not say that a FIFO scheduler which makes a start transition as soon as possible is optimal. It might be useful to delay starting until one of the competing tasks has used the resource. Only delays that are shorter than that are considered lazy.

To illustrate the limited scope of the lemma and theorem consider a task with whose duration characterized by a discrete probability with probability p for a and 1 -p for b. In this case, the value function associated with waiting is V (x) = p(a -x) + (1 -p)(b -x) when x < a 0(a -x) + 1(b -x) when x > a

Here at x = a there is a jump in V from (1 -p)(b -a) to (b -a) which is, intuitively, due to the accumulation of information: after a time, the non-occurrence of an end event tells us that the duration is certainly b. Such a situation contradicts the lemma, because for x < a < x we may have V (x ) > V (a). This jump in the expected time-to-go for waiting can also justify laziness: when x < a waiting can be better then starting, but after x = a the relation between these two values may change.

A.2 Upward Closed Strategies and Rectangular Approximations

In the sequel we present the implications of non-laziness on the structure of the optimal scheduler. To simplify notations, but without loss of generality, we assume throughout this part that each resource m ∈ M is used by exactly one step of each of the processes. Although formally the Q-Q0 Q1 q q Q+ Figure A.3: The timeline of a process partitioned with respect to a resource used in state q and the duration of a conflicting step of another process.

strategy is defined over Q, it can be decomposed into nk partial strategies, each representing a start/wait decision associated with one step of one process. The strategy can be written as

Ω = m∈M i∈N Ω i m
where Ω i m corresponds to the step where P i uses resource m, say step j. In this case Ω i m has the form

Ω i m : Q 1 × • • • {q i j } • • • × Q n → {s i j , w}.
We call the domain of Ω i m the decision surface associated with s i j . In general, the state space of a process P which uses a resource m in state q can be partitioned as

Q = Q -∪ {q} ∪ {q} ∪ Q + ,
namely the states before the step in question, the waiting state (where decisions are to be made), the active state (where other processes cannot use the resource) and the states after that, see Figure A.3. When the scheduler has to decide whether to let another process P take resource m, the only reason for not doing so could be the possibility of blocking P in the future if P is in some preconflict state in Q -. However, not all pre-conflict states represent a real conflict with P . If the upper bound on the duration of the step of P is b, and P is in a state in Q -whose minimal distance to q is larger than b, P will release the resource before P becomes enabled and no blocking will occur. This justifies a finer refinement of the pre-conflict states, Q -= Q 0 ∪ Q 1 , with Q 0 consisting of states of P where we need not worry about its being blocked by P (see Figure A.3). Note that Q 0 is a static under-approximation of the set of states having this property under a given scheduling strategy because it is based on a minimal distance, assuming P progresses toward q without waiting. We stress again the fact that the boundary between Q 0 and Q 1 is specific to each P .

We illustrate the implications of arithmetics, mutual exclusion and non-laziness on the partition of the state space induced the optimal strategy on a system of of 3 processes where we analyze the decision surface Q 2 × Q 3 for the sub-scheduler

Ω 1 m : {q 1 } × Q 2 × Q 3 → {s, w}
for process P 1 . First we partition the timelines of the competing processes P 2 and P 3 with respect to the duration of the relevant step of P 1 . One can observe that:

• If the other processes are in (Q 2 × {q 3 }) ∪ ({q 2 } × Q 3 ), that is, one of them uses the resource, then only action w is possible;

• If the other processes are in (Q

2 0 ∪ Q 2 + ) × (Q 3 0 ∪ Q 3 + )
then action s is chosen because there will be no blocking;

• The strategy needs really to be computed over (Q 2 1 × (Q 3 -{q 3 })) ∪ ((Q 2 -{q 2 })) × Q 3 1 ) and there we can enjoy the monotonicity property. The decision surface for P 2 × P 3 for the decision of P 1 . Only in the grey area the decision is not self-evident and there the domain of w is upward closed; (b) A query-based rectangular approximation of the optimal strategy. In the blank area the optimal strategy is not known but approximated.

Figure 2 . 3 :

 23 Figure 2.3: Generic Embedded System Design Flow

CHAPTER 2 .

 2 MULTI-CORE EMBEDDED SYSTEM software developers can begin earlier with development and verification of the hardware dependent software. Platform To give an overview about the different levels of abstraction and to illustrate their interrelation to the different specification domains, the Y-Chart of Fig-2.4 proposed by Gajeski is commonly used [96].

Figure 2 . 4 :

 24 Figure 2.4: Gajski-Kuhn Y-chart

Figure 2 . 5 :

 25 Figure 2.5: Abstraction levels

Figure 2 .

 2 Figure 2.6: Y-chart based design space exploration (obtained from [162])

Figure 3 . 1 :

 31 Figure 3.1: Operations on timed zones

Figure 3 . 2 :

 32 Figure 3.2: Example of timed automaton

  .3 and the corresponding IF code is shown in Listing-3.1.

Figure 3 . 3 :

 33 Figure 3.3: Example of a multi-threaded server

Definition 4 . 2 . 1 (

 421 Uniform Distribution). A uniform distribution inside an interval I = [a, b] is characterized by a density ψ defined as ψ(y) = 1/(b -a) if a ≤ y < b 0 otherwise and in terms of distribution as

Figure 4 . 1 :

 41 Figure 4.1: An automaton view of a process.

1 Figure 4 . 2 :e 2 1 e 2 2 e 3 1 e 2 3 e 1 2 e 1 3 e 3 2 e 3 3

 1423 Figure 4.2: A global behavior w = e 1 1 e 2 1 e 2 2 e 3 1 e 2 3 e 1 2 e 1 3 e 3 2 e 3 3 obtained by merging local behaviors. The dashed line indicate the minimal set of additional inter-process constraints that characterize w.

3 Figure 4 . 3 :e 2 1 e 2 2 e 3 1 e 2 3 e 1 2 e 1 3 e 3 2 e 3 3

 3433 Figure 4.3: The product automaton for a process system with n = 2, k = 3. The thick arrows indicate the path corresponding to the qualitative behavior w = e 1 1 e 2 1 e 2 2 e 3 1 e 2 3 e 1 2 e 1 3 e 3 2 e 3 3 . The race between e 13 and e 2 2 in state (q 1 3 , q22 ) is indicated by the dashed arrows.

Figure 4 . 4 :

 44 Figure 4.4: Incremental constraint construction: constraints for e 11 and then for e 1 1 e 2 1 . The constraint t 1 1 < t 3 1 becomes redundant after the second event.

  x

Figure 4 . 5 :

 45 Figure 4.5: Zone volume computation by splitting into integration domains in two different integration orders which yield 3 and 2 domains, respectively.

Figure 4 . 6 :

 46 Figure 4.6: (a) Two parallel processes admitting a resource conflict and their product automaton. The dashed arrows indicate start transitions which should be under the control of a scheduler while the dotted arrows indicate post-conflict start transitions; (b) The automaton resulting from composition with a FIFO scheduler and the 4 potential conflict resolution and resource utilization scenarios.

P1 { [ 2 , 8 ]

 28 [ 3 , 7 ] [ 4 , 8 ] } P2 { [ 4 , 1 0 ] [ 4 , 1 2 ] [ 2 , 5 ] } s h a r e d : = STRICT { P1 . s 2 , P2 . s 2 } Listing 4.1: Example of description

/

  / o r d e r : / / o r d e r : / / o r d e r : / / o r d e r : / / [ 1 , 4 , 2 , 5 , 3

Listing 4 . 2 : Case 1 }}}

 421 Listing 4.3: Case 2 Listing 4.4: Case 3 Listing 4.5: Case 4

P1 { [ 3

 3 r e d : = FIFO { P1 . s 2 , P2 . s 4 } s h a r e d : = FIFO { P1 . s 4 , P2 . s 3 }

. 5 .

 5 Column < 3 min indicates the percentage of examples which have been computed in less than 3 minutes.

Definition 5 . 1 . 1 (

 511 Bounded Support Time Density). A time density is a function ψ : R + → R + satisfying ∞ 0 ψ[t]dt = 1. A time density is of bounded support when ψ(t) = 0 iff t ∈ I = [a, b]. A partial time density satisfies the weaker condition: ψ[t]dt < 1. A time density is uniform if ψ[t] = 1/(b -a) inside its support [a, b].

Figure 5 . 1 : 2 .Definition 5 . 1 . 2 (

 512512 Figure 5.1: The shift operator ψ /x . left: x < a; right: a < x < b. The intuition is that the passage of time shifts the rectangle for ψ backward by x until ψ[x + t] coincides with ψ /x [t]. When x > 0 the rectangle reaches the zero (causality) wall and the (fixed) volume is pushed upwards.

  b a ψ[t]dt/ b x ψ[t]dt.

  x

Figure 5 . 2 :

 52 Figure 5.2: A simple DPA.

  4.6-b) renders it input-deterministic in the sense that any point y ∈ D induces a unique 4 run of the automaton composed of an alternation of discrete transitions and periods of time elapse. Definition 5.3.4 (Steps and Runs). The steps of a controlled DPA A • Ω, induced by a point y ∈ D are of the following types:

Figure 5 . 3 :Figure 5 . 4 :

 5354 Figure 5.3: The value function V (q 11 , q 2 2 , x 1 , ⊥)

  and compare it with the clock-free technique developed in the previous chapter. The results are indeed identical.

Figure 5 . 5 :

 55 Figure 5.5: The value functionV (q 1 1 , q 2 1 , x 1 , x 2 )

  = [ 1 0 , 2 0 ] x2 = [ 2 0 , 3 0 ] x2-x1 = [ 1 0 , 2 0 ] E: ( 3 6 5 / 8 -7 / 1 6 * x1 -3/80 * x1 * x2 +1/1600 * x1 * x2 ˆ2 + 3 / 1 6 0 * x1 ˆ2 -1/1600 * x1 ˆ2 * x2 +1/4800 * x1 ˆ3 -9/16 * x2 +3/160 * x2 ˆ2 -1/4800 * x2 ˆ3 ) N2 : Z : x1 = [ 0 , 1 0 ] x2 = [ 1 0 , 3 0 ] x2-x1 = [ 1 0 , 3 0 ] E: ( 3 6 5 / 8 -7 / 1 6 * x1 -3/80 * x1 * x2 +1/1600 * x1 * x2 ˆ2 + 3 / 1 6 0 * x1 ˆ2 -1/1600 * x1 ˆ2 * x2 +1/4800 * x1 ˆ3 -9/16 * x2 +3/160 * x2 ˆ2 -1/4800 * x2 ˆ3 ) N3 : Z : x1 = [ 1 0 , 2 0 ] x2 = [ 0 , 1 0 ] x2-x1 =[-20,-10] E: ( 3 6 5 / 8 -9 / 1 6 * x1 -3/80 * x1 * x2 -1/1600 * x1 * x2 ˆ2 + 3 / 1 6 0 * x1 ˆ2 + 1 / 1 6 0 0 * x1 ˆ2 * x2 -1/4800 * x1 ˆ3 -7/16 * x2 +3/160 * x2 ˆ2 + 1 / 4 8 0 0 * x2 ˆ3 ) N4 : Z : x1 = [ 0 , 1 0 ] x2 = [ 0 , 1 0 ] x2-x1 =[ -10 ,10] E: ( 5 4 5 / 1 2 -1 / 2 * x1 -1/40 * x1 * x2 +1/80 * x1 ˆ2 -1/2 * x2 +1/80 * x2 ˆ2 ) N5 : Z : x1 = [ 1 0 , 2 0 ] x2 = [ 0 , 1 0 ] x2-x1 =[ -10 ,0] E: ( 5 4 5 / 1 2 -1 / 2 * x1 -1/40 * x1 * x2 +1/80 * x1 ˆ2 -1/2 * x2 +1/80 * x2 ˆ2 ) N6 : Z: x1 = [ 1 0 , 2 0 ] x2 = [ 1 0 , 3 0 ] x2-x1 =[ -10 ,10] E: ( 5 4 5 / 1 2 -1 / 2 * x1 -1/40 * x1 * x2 +1/80 * x1 ˆ2 -1/2 * x2 +1/80 * x2 ˆ2 ) N7 : Z : x1 = [ 0 , 1 0 ] x2 = [ 1 0 , 2 0 ] x2-x1 = [ 0 , 1 0 ] E: ( 5 4 5 / 1 2 -1 / 2 * x1 -1/40 * x1 * x2 +1/80 * x1 ˆ2 -1/2 * x2 +1/80 * x2 ˆ2 ) N8 : Z : x1 = [ 1 0 , 2 0 ] x2 = [ 4 0 , 5 0 ] x2-x1 = [ 3 0 , 4 0 ] E : ( 2 0 0 0 + x1 * x2-50 * x1-40 * x2 ) / (50-x2 ) N9 : Z : x1 = [ 0 , 1 0 ] x2 = [ 4 0 , 5 0 ] x2-x1 = [ 3 0 , 5 0 ] E : ( 2 0 0 0 + x1 * x2-50 * x1-40 * x2 ) / (50-x2 ) N10 : Z : x1 = [ 0 , 1 0 ] x2 = [ 3 0 , 4 0 ] x2-x1 = [ 3 0 , 4 0 ] E : ( 2 0 0 0 + x1 * x2-50 * x1-40 * x2 ) / (50-x2 ) N11 : Z : x1 = [ 1 0 , 2 0 ] x2 = [ 3 0 , 4 0 ] x2-x1 = [ 1 0 , 3 0 ] E: ( 4 22 5 / 2 -1 5 5 / 4 * x1 +1/4 * x1 * x2 +1/80 * x1 * x2 ˆ2 + 3 / 8 * x1 ˆ2 -1/80 * x1 ˆ2 * x2 +1/240 * x1 ˆ3 -205/4 * x2 +3/8 * x2 ˆ2 -1/240 * x2 ˆ3 ) / ( 5 0 -x2 ) N12 : Z : x1 = [ 1 0 , 2 0 ] x2 = [ 4 0 , 5 0 ] x2-x1 = [ 2 0 , 3 0 ] E: ( 4 2 2 5 / 2 -1 5 5 / 4 * x1 +1/4 * x1 * x2 +1/80 * x1 * x2 ˆ2 + 3 / 8 * x1 ˆ2 -1/80 * x1 ˆ2 * x2 +1/240 * x1 ˆ3 -205/4 * x2 +3/8 * x2 ˆ2 -1/240 * x2 ˆ3 ) / ( 5 0 -x2 ) N13 : Z : x1 = [ 0 , 1 0 ] x2 = [ 3 0 , 4 0 ] x2-x1 = [ 2 0 , 3 0 ] E: ( 4 2 2 5 / 2 -1 5 5 / 4 * x1 +1/4 * x1 * x2 +1/80 * x1 * x2 ˆ2 + 3 / 8 * x1 ˆ2 -1/80 * x1 ˆ2 * x2 +1/240 * x1 ˆ3 -205/4 * x2 +3/8 * x2 ˆ2 -1/240 * x2 ˆ3 ) / ( 5 0 -x2 ) N14 : Z : x1 = [ 2 0 , 3 0 ] x2 = [ 0 , 2 0 ] x2-x1 =[-30,-10] E:(2625 -125/2 * x1 -1/2 * x1 * x2 -1/40 * x1 * x2 ˆ2 + 3 / 4 * x1 ˆ2 + 1 / 4 0 * x1 ˆ2 * x2 -1/120 * x1 ˆ3 -75/2 * x2 +3/4 * x2 ˆ2 + 1 / 1 2 0 * x2 ˆ3 ) / ( 6 0 -x1 ) N15 : Z : x1 = [ 3 0 , 6 0 ] x2 = [ 0 , 3 0 ] x2-x1 =[-30,-10] E:(2625 -125/2 * x1 -1/2 * x1 * x2 -1/40 * x1 * x2 ˆ2 + 3 / 4 * x1 ˆ2 + 1 / 4 0 * x1 ˆ2 * x2 -1/120 * x1 ˆ3 -75/2 * x2 +3/4 * x2 ˆ2 + 1 / 1 2 0 * x2 ˆ3 ) / ( 6 0 -x1 ) N16 : Z : x1 = [ 2 0 , 3 0 ] x2 = [ 2 0 , 3 0 ] x2-x1 =[ -10 ,10] E:(7850/3 -60 * x1 +1/2 * x1ˆ2-40 * x2 +1/2 * x2 ˆ2 ) / ( 6 0 -x1 ) N17 : Z : x1 = [ 3 0 , 4 0 ] x2 = [ 2 0 , 3 0 ] x2-x1 =[ -10 ,0] E:(7850/3 -60 * x1 +1/2 * x1ˆ2-40 * x2 +1/2 * x2 ˆ2 ) / ( 6 0 -x1 ) N18 : Z : x1 = [ 2 0 , 3 0 ] x2 = [ 1 0 , 2 0 ] x2-x1 =[ -10 ,0] E:(7850/3 -60 * x1 +1/2 * x1ˆ2-40 * x2 +1/2 * x2 ˆ2 ) / ( 6 0 -x1 ) N19 : Z : x1 = [ 4 0 , 6 0 ] x2 = [ 0 , 3 0 ] x2-x1 =[-60,-30] E:(2400 -40 * x1+x1 * x2-60 * x2 )/(60 -x1 ) N20 : Z : x1 = [ 3 0 , 4 0 ] x2 = [ 0 , 1 0 ] x2-x1 =[-40,-30] E:(2400 -40 * x1+x1 * x2-60 * x2 )/(60 -x1 ) N21 : Z : x1 = [ 4 0 , 6 0 ] x2 = [ 3 0 , 5 0 ] x2-x1 =[-30,-10] E:(111000 -3050 * x1 +50 * x1 * x2 -1/2 * x1 * x2 ˆ2+30 * x1 ˆ2 -1/6 * x1 ˆ3-3000 * x2 +30 * x2 ˆ2)/(3000 -50 * x1+x1 * x2-60 * x2 ) N22 : Z : x1 = [ 3 0 , 4 0 ] x2 = [ 3 0 , 5 0 ] x2-x1 =[ -10 ,20] E : ( 3 3 2 5 0 0 / 3 + 6 0 * x1 * x2-3000 * x1 -1/2 * x1 ˆ2 * x2 +25 * x1 ˆ2-3050 * x2 +25 * x2 ˆ2 -1/6 * x2 ˆ3)/(3000 -50 * x1+x1 * x2-60 * x2 ) N23 : Z : x1 = [ 2 0 , 3 0 ] x2 = [ 3 0 , 5 0 ] x2-x1 = [ 0 , 3 0 ] E : ( 3 3 2 5 0 0 / 3 + 6 0 * x1 * x2-3000 * x1 -1/2 * x1 ˆ2 * x2 +25 * x1 ˆ2-3050 * x2 +25 * x2 ˆ2 -1/6 * x2 ˆ3)/(3000 -50 * x1+x1 * x2-60 * x2 ) N24 : Z : x1 = [ 4 0 , 6 0 ] x2 = [ 3 0 , 5 0 ] x2-x1 =[ -10 ,10] E : ( 3 3 2 5 0 0 / 3 + 6 0 * x1 * x2-3000 * x1 -1/2 * x1 ˆ2 * x2 +25 * x1 ˆ2-3050 * x2 +25 * x2 ˆ2 -1/6 * x2 ˆ3)/(3000 -50 * x1+x1 * x2-60 * x2 ) Listing 5.1: The value function V (q 1

Figure 6 . 1 :

 61 Figure 6.1: Model description

Figure 6 . 2 :

 62 Figure 6.2: Application model

Definition 6 . 2 . 2 .

 622 (Communication task) A communication task is defined by a triple τ c = (src, dst, δ) where δ = [l τ c , u τ c ] defines a quantity of data measured in bytes to be communicated from a software component src to another software component dst.

Figure 6 . 4 :

 64 Figure 6.4: Timed automaton for a communication task

Figure 6 . 5 :

 65 Figure 6.5: Example of communication task usage

Figure 6 . 6 :

 66 Figure 6.6: Job instantiation

Figure 6 . 7 :Figure 6 . 9 :

 6769 Figure 6.7: Timed automaton for a single shot generator

Figure 6 . 10 :

 610 Figure 6.10: Periodic generator with uncertainty

Figure 6 . 11 :

 611 Figure 6.11: Timed automaton for a periodic generator with uncertainty

Figure 6 . 12 :

 612 Figure 6.12: Periodic generator with jitter smaller than period

Figure 6 . 14 :

 614 Figure 6.14: Timed automaton for periodic generator with jitter

Figure 6 .

 6 Figure 6.15: A bounded variability generator

Figure 6 . 16 :

 616 Figure 6.16: Timed automaton for bounded variability generator

Figure 6 .

 6 Figure 6.17: A Bi-bounded variability generator

Figure 6 .

 6 Figure 6.18: Bi-bounded variability generator timed automaton

Figure 6 .

 6 Figure 6.19: processor timed automaton

Figure 6 . 20 :

 620 Figure 6.20: Power state machine of StrongARM SA-1100 from [27]

Figure 6 . 21 :

 621 Figure 6.21: Timed automaton for a memory component

Figure 6 . 22 :

 622 Figure 6.22: Memory architecture example

6. 4

 4 .3.3 DMA-based Communication DMA are dedicated processing elements that can transfer large amounts of data between memory locations without processor intervention. They can be used in a double buffering scheme shown in Fig-6.25, to improve performance.

Figure 6 . 25 :

 625 Figure 6.25: Data transfer: single versus double buffering

Figure 6 .

 6 Figure 6.26: DMA architecture with local memory for each PE

Figure 6 . 29 :

 629 Figure 6.29: Abstract NoC timed automaton

Figure 6 .

 6 Figure 6.30: System model

Figure 6 . 31 :

 631 Figure 6.31: Global FIFO scheduler

Figure 6 .

 6 Figure 6.32: Local FIFO scheduler

Figure 6 . 33 :

 633 Figure 6.33: Observer for checking the deadline of a task

Figure 7 . 1 :

 71 Figure 7.1: Tool architecture

Figure 7 . 2 :

 72 Figure 7.2: Component characteristics

Fig- 7 .

 7 [START_REF] Ackland | A single-chip 1.6 billion 16-b mac/s multiprocessor dsp[END_REF] shows the class hierarchy.

Figure 7 . 3 :

 73 Figure 7.3: Class hierarchy

Figure 7 . 4 :

 74 Figure 7.4: Abstract components grammar

Figure 7 . 5 :

 75 Figure 7.5: Abstract parameters grammar

Figure 7 . 6 :

 76 Figure 7.6: Model implementation

Figure 7 . 7 :

 77 Figure 7.7: Textual editor.

Figure 7 . 8 :

 78 Figure 7.8: Graphical editor.

. 9 <p

 9 r o p e r t y name=" R e s p o n s e T i m e j o b " d e a d l i n e =750> < s t a r t p r o c e s s =" { j o b }0 "> < s t a t e name=" i n i t " f l a g =" IN ">< / s t a t e> < / s t a r t> <end p r o c e s s =" { j o b }0 "> <e v e n t name=" k i l l " >< / e v e n t> < / end> < / p r o p e r t y> Listing 7.1: Property definition example 7.2. MODEL DESCRIPTION

Figure 7 . 9 :

 79 Figure 7.9: Properties language grammar

Figure 7 . 10 :

 710 Figure 7.10: Power consumption specification grammar

Figure 7 . 11 :

 711 Figure 7.11: Timed automata translation

Figure 7 .

 7 Figure 7.12: Simulation flow

Figure 7 .

 7 Figure 7.14: Standard description

Figure 7 . 15 :

 715 Figure 7.15: Non determinism is decoupled through random variable y

Figure 7 . 16 :

 716 Figure 7.16: Uniform versus discretized distribution

Figure 7 .

 7 Figure 7.17: GUI for simulation and reachability analysis

Figure 7 . 18 :

 718 Figure 7.18: Simulation trace visualization with TraceNavigator

Figure 7 . 19 :

 719 Figure 7.19: Example of response time distribution

  .22), response time of software components (Fig-7.24) or states distribution (Fig-7.23).

Figure 7 . 22 :Figure 7 . 23 :

 722723 Figure 7.22: Consumption overview with TraceNavigator

  Figure-8.1 and the architecture consists of two processors of different types P 1 and P 2 as shown in Figure-8.2. The tasks are partitioned into two types with A tasks running on P 1 and B tasks on P 2 . The lower and upper-bound on the task durations are shown in Table

Figure 8 . 1 :

 81 Figure 8.1: Task graph example

Figure 8 . 3 :

 83 Figure 8.3: Execution trace for worst-case duration

Figure 8 . 4 :

 84 Figure 8.4: Execution trace for best-case duration

Figure 8 . 5 :

 85 Figure 8.5: The execution trace which gives the worst response time

Figure 8 . 6 :

 86 Figure 8.6: The execution trace which gives the best response time

Figure 8 . 8 :

 88 Figure 8.8: A model of a 16-processor instance of P2012

Figure 8 . 9 :

 89 Figure 8.9: Bands splitting and dispatching on PEs

Figure 8 . 10 :

 810 Figure 8.10: One centralized read, split and merge

Figure 8 .

 8 Figure 8.11: 16 independent reads and writes

Figure 8 . 12 :

 812 Figure 8.12: The distribution of total termination times using 1, 2, 4, 8 and 16 processors working at 600Hz. The red vertical lines indicate the lower-and upper-bounds. Note the change of scale.

Fig- 8 .

 8 Fig-8.[START_REF] Asarin | Timed regular expressions[END_REF] shows the speedup obtained by the second, more flexible policy, as the number of processors grows. Note that the speed-up in the average-case is much more significant. Fetching data by bands requires a synchronization for writing back the results. This synchronization implies a latency coming from the slower computation. On the other hand block treatment is more flexible, once a computation terminates the transfer of the next block can start immediately and communication becomes more fluid.

Figure 8 . 13 :

 813 Figure 8.13: The speed-up obtained by reading single blocks compared to reading 16-block bands

  (a) Processor utilization under fixed mapping strategy. (b) Processor utilization under flexible mapping strategy.

Figure 8 .

 8 Figure 8.14: Processor utilization

Figure 8 . 15 :

 815 Figure 8.15: Comparing the average performance of the fixed and flexible mapping strategies as a function of the arrival period.

Figure 8 .

 8 Figure 8.16: Power-performance trade-offs obtained on different configurations (number of processors and frequencies)

Figure 8 . 17 :

 817 Figure8.17: The xSTream architecture from[START_REF] Berenguer | xstream : Architecture multi-coeur sur puce pour des applications multimédia[END_REF]

Figure 8 . 18 :

 818 Figure 8.18: The xSTream model

  different channels. A task-graph model of this application is shown on Fig-8.19. Boxes represent the concatenation of several computations into task for the model used in our tool which is shown on Fig-8.20.

Figure 8 .

 8 Figure 8.19: Sensing Application

Figure 8 .

 8 Figure 8.20: Sensing Application Model

  Figure A.1-(b) and the corresponding runs:

  ⊥, ⊥)ξ x : (x i , x i ) t+δ -→ e i -→ (x i + δ + t, ⊥) δ-δ -→ (x i + δ + t, ⊥)

  p y , z y ).

Figure A. 1 :Figure A. 2 :

 12 Figure A.1: Proof of lemma: (a) P i wins from both x and x ; (b) P i wins from both. (c) P i wins from x and P i wins from x. Here either ξ x reaches point A in less time than does ξ x , or both reach point B at the same time.

  Figure A.2-(a). A alternative strategy that would start at x, can be after t time in a state where one clock is more advanced (Figure A.2-(b)) and hence satisfying the condition of Lemma 1.

  Figure A.4: (a)The decision surface for P 2 × P 3 for the decision of P 1 . Only in the grey area the decision is not self-evident and there the domain of w is upward closed; (b) A query-based rectangular approximation of the optimal strategy. In the blank area the optimal strategy is not known but approximated.

  that is the smallest (in terms of inclusion) zone containing both Z 1 and Z 2 , see (fig3.1-(c)). Since zones are not closed under union, Z 1 Z 2 is used as an over-approximation of Z 1 ∪ Z 2 .

Z is the forward projection of Z, i.e. all clock valuations that can result by applying time progress to element of Z (fig 3.1-(f)):

Table 4 .

 4 1: The zones corresponding to the four possible outcomes of the resource conflict of Fig. 4.7-(b). Constraints on t 13 and t 2 3 as well as the bounding constraints on t 1 1 and t 2 1 are omitted.

Table 4 .

 4 4.2.

	Case	Probability	Expected time
	1	0.143017	20.2595
	2	0.000501644	15.654
	3	0.844586	21.9855
	4	0.0118956	17.9216
	global	1	21.6867

2: Expected time for example of Listing-4.1

Table 4 .

 4

5: Experiments results 4.6. CONCLUSIONS Chapter 5

Table 6 .

 6

		1: Characteristics of the different generators
					Inter-arrival
	Generator	Min(e)/∆ Max(e)/∆ ∆	Min	Max
	Periodic	1	1	P	P	P
	Periodic with jitter	0	J P

Table 6 .

 6 6.2 2: Routing table for processing element pe 0

Table 8 . 2

 82 Table-8.2 and Fig-8.7.

	Min value	12.97
	Max value	22.17
	Mean value 16.82

: Statistics Figure 8.7: Distribution

Table 8 . 3

 83 We associate with each component a list of synthetic parameters for power consumption shown in Table-8.3. The realism of these parameters is limited due to the difficulty to get real values from a virtual platform.

	Component	Frequency State Consumption
		200Hz	idle busy	42 212
	Processor	400Hz	idle busy	72 362
		600Hz	idle busy	121 606
	Memory		idle busy	61 91
	LogInterconnect		idle busy	12 61
	BusExt		idle busy	121 606

: Power consumption values for HW components

Table 8 . 4

 84

			TA Analysis		Simulation
	Frequency PE nb	Min	Max	Min	Mean	Max
	200		1165.552 1651.184 1377.174 1405.946 1426.697
	200		593.392	836.208	715.049	728.614	741.454
	200		307.312	428.720	378.453	386.348	394.134
	200		164.272	224.976	216.509	206.045	212.247
	200	16	92.752	123.104	119.776	121.214	122.258
	400		593.392	836.080	702.889	713.974	725.086
	400		307.312	428.656	368.718	374.989	383.316
	400		164.272	224.944	200.303	203.442	206.939
	400		92.752	123.088	113.498	116.687	118.317
	400	16	56.992	72.160	70.304	71.232	71.690
	600		402.672	564.464	474.497	483.100	493.192
	600		211.952	292.848	253.268	257.086	260.640
	600		116.592	157.040	140.468	142.829	145.902
	600		68.912	89.136	83.690	84.835	86.063
	600	16	45.072	55.184	54.137	54.611	54.998

: Results of TA Analysis versus Simulation

  A.1-(a) and the corresponding runs ξ x and ξ x , depicted below while omitting the discrete state and the other clocks:ξ x : (x i + δ, x i )

t -→ (x i + δ + t, x i + t) e i -→ (x i + δ + t, ⊥) ξ x : (x i , x i ) t -→ (x i + +t, x i + t) e i -→ (x i + t, ⊥).

Tradition aside, the term non-Markovian is misleading. These processes are Markovian (state-based) with respect to extended states that include clock values.

2.1. MPSOC ARCHITECTURE

2.2. DESIGN FLOW CHAPTER 2. MULTI-CORE EMBEDDED SYSTEM

2.2. DESIGN FLOW

2.3. MODELS OF COMPUTATION FOR EMBEDDED SYSTEMS DESIGN

2.4. PERFORMANCE EVALUATION

2.5. OUR MODELING FRAMEWORK

2.6. RELATED TOOLS CHAPTER 2. MULTI-CORE EMBEDDED SYSTEM

2.6. RELATED TOOLS

3.1. CLOCKS, TIME CONSTRAINTS, ZONES

3.2. TIMED AUTOMATA: SYNTAX AND SEMANTICS CHAPTER 3. TIMED AUTOMATA

3.2. TIMED AUTOMATA: SYNTAX AND SEMANTICS

3.3. REACHABILITY ANALYSIS

3.4. IMPLEMENTATION

3.4. IMPLEMENTATION CHAPTER 3. TIMED AUTOMATA

4.1. SCHEDULING UNDER STOCHASTIC UNCERTAINTY

4.2. PRELIMINARIES

In the computer science tradition the term language is often used to denote a set of sequences or other objects that define dynamic behaviors.

These are the timed traces used originally in[START_REF] Alur | A theory of timed automata[END_REF] to give semantics to timed automata. More about the relation between semantic models of timed behaviors can be found in[START_REF] Asarin | Timed regular expressions[END_REF].

4.2. PRELIMINARIES CHAPTER 4. DURATION PROBABILISTIC AUTOMATA: ANALYSIS

Since we are dealing with volumes, our neglect of the possibility of events occurring at exactly the same time and not paying too much attention to the distinction between strict and non strict inequalities is justified.

4.2. PRELIMINARIES

4.3. COMPUTING VOLUMES

We consider schedulers that by construction cannot make the system enter a forbidden state.

Note that we restrict ourselves to non-lazy schedulers: if they do not issue an s i j command at some point, they will not issue it later unless another process has utilized the resource. This class has been shown[START_REF] Abdeddaïm | Scheduling with timed automata[END_REF] to contain the optimal schedulers for deterministic problems and its extension to our setting is discussed in Chapter 5.

4.4. CONFLICTS AND SCHEDULERS

4.4. CONFLICTS AND SCHEDULERS CHAPTER 4. DURATION PROBABILISTIC AUTOMATA: ANALYSIS

4.5. IMPLEMENTATION AND EXPERIMENTAL RESULTS

4.5. IMPLEMENTATION AND EXPERIMENTAL RESULTS CHAPTER 4. DURATION PROBABILISTIC AUTOMATA: ANALYSIS

4.6. CONCLUSIONS

We define a priority order among the s i -actions so that in the (measure zero) situation where two actions are taken simultaneously we impose the order to guarantee a unique run and avoid the artifacts of the interleaving semantics.

5.3. CONFLICTS AND SCHEDULERS

It is worth noting that the dependence on the time already elapsed is in contrast with the memoryless exponential distribution where this time does not matter for the future. For those distributions the time-to-go is associated only with the discrete state and is much easier to compute, see[START_REF] Abdeddaïm | Scheduling with timed automata[END_REF] for the derivation of optimal schedulers for DPA with exponential distribution.

5.5. COMPUTATIONAL ASPECTS

5.6. IMPLEMENTATION

5.7. AN EXAMPLE

5.8. CONCLUDING REMARKS

6.2. APPLICATION MODEL CHAPTER 6. MODELING EMBEDDED SYSTEMS WITH TIMED AUTOMATA

6.2. APPLICATION MODEL

6.3. ENVIRONMENT MODEL

6.3. ENVIRONMENT MODEL CHAPTER 6. MODELING EMBEDDED SYSTEMS WITH TIMED AUTOMATA

6.4. ARCHITECTURE MODEL CHAPTER 6. MODELING EMBEDDED SYSTEMS WITH TIMED AUTOMATA

6.4. ARCHITECTURE MODEL

6.5. SYSTEM MODEL

6.6. EVALUATION

7.2. MODEL DESCRIPTION

7.3. TRANSLATION TO TIMED AUTOMATA CHAPTER 7. REALIZATION: THE DESPEX TOOL

7.3. TRANSLATION TO TIMED AUTOMATA

7.4. TRACE ANALYSIS

7.4. TRACE ANALYSIS CHAPTER 7. REALIZATION: THE DESPEX TOOL

8.1. REACHABILITY VS. CORNER-CASE SIMULATION

8.1. REACHABILITY VS. CORNER-CASE SIMULATION CHAPTER 8. CASE STUDIES

8.2. VIDEO PROCESSING ON P2012

8.2. VIDEO PROCESSING ON P2012 CHAPTER 8. CASE STUDIES

8.3. A RADIO SENSING APPLICATION

Although the case study described in Section 8.3 was conducted by Thales working directly with the tool.

Or if some information gathered during the period has increased the expected time-to-go associated with waiting, which is impossible in our setting, see discussion.

A.1. NON-LAZY SCHEDULERS

A.2. UPWARD CLOSED STRATEGIES AND RECTANGULAR APPROXIMATIONS

The derivative of V represents the progress toward the average duration, minus the growth of the average itself when x > a.

Definition 5.4.3 (Race Winner). Let q be a state where n processes are active, each in a step admitting a time density ψ i . With every clock valuation x = (x 1 , . . . , x n ) ≤ (b 1 , . . . , b n ) and every i we associate the partial density:

Definition 5.4.4 (Computing Stochastic Time-to-go). For every i, the function µ i is defined inductively as µ i ((. . . q i k+1 . . .), x) = 0 (5.6) µ i (q, x, s i ) = µ i (σ i (0, q, x)))

(5.7)

For any global state where P i is in its final state, µ i is zero (5.6). Each enabled start action s i leads immediately to the successor state and the cost-to-go is inherited from there (5.7). For waiting we make a convolution between the probability of P i winning the race and the value of µ i in the post-transition state and sum up over all the active processes (5.8). The basic iterative step in computing the value function and strategy is summarized in Algorithm 3. A dynamic programming algorithm starting from the final state and applying the above procedure will produce the expectedtime optimal strategy for this scheduling problem. Since we are dealing with acyclic systems, the question of convergence to a fixed point is not raised at all. The only challenge is to show that the defined operators are computable.

Algorithm 3 Value Iteration

Input: A global state q such that Ω(q , x) and µ i (q , x) have been computed for each of its successors q and every i Output: Ω(q, x), and µ i (q, x) % COMPUTE: for all s ∈ Σ s ∪ {w} do for i = 1 → n do compute µ i (q, x, s) according to (5.7-5.8) end for compute µ(q, x, s) max of random variables compute V (q, x, s) expected makespan end for % OPTIMIZE: for all x ∈ Z q do V (q, x) = min s (V (q, x, s)) s * = arg min s V (q, x, s) Ω(q, x) = s * end for % UPDATE: for i = 1 → n do µ i (q, x) = µ i (q, x, s * ) end for

Stochastic Simulation

Depending on the size of the model it may be difficult or even impossible to perform reachability analysis due to state space explosion. We provide stochastic simulation as an alternative on semantically equivalent models. Timed automata can be used to perform discrete event simulation by using a randomized reachability exploration. One point which is not defined in timed automata formalism is how timing uncertainty are distributed. The stochastic model can be viewed as a refinement of the TA model. It has the same set of behaviors but with a probability measure defined on the space of behaviors which is non-zero exactly on the feasible ones.

From Timed Automata to Duration Probabilistic Automata

We restrict ourself to bounded uncertainty and we explain in this section how we integrate probabilistic information into timed automata model. The resulting model of duration probabilistic

Non-Lazy Schedulers

To complete the implementation we need to handle the optimization part of the iteration, computing V (q, x) = min s (V (q, x, s)) for every x. In other words we should trace the boundary in the clock space between subsets where waiting or starting are preferred. To facilitate the task we first prove an important property of optimal strategies which simplifies the partition of the clock space according to the optimal action. This "non-laziness" property has been formulated in the deterministic setting in [START_REF] Abdeddaïm | Scheduling with timed automata[END_REF] and it simply captures the intuition that waiting and refraining from taking a resource is not useful unless some other process benefits from the resource during the waiting period. 1 The proof in the deterministic setting is based on taking a schedule that admits laziness and transforming it iteratively into a schedule with less laziness (but no inferior performance) until a non-lazy schedule is obtained. The proof in the non-deterministic context is more involved.

Definition A.1.1 (Laziness). A scheduling policy Ω is lazy in (q, x) if Ω(q, x + t) = s i for some i and Ω(q, x + t ) = w for every 0 ≤ t < t. A schedule is non-lazy if no such (q, x) exists.

Theorem 3 (Non Lazy Optimal Schedulers). The optimal value V can be obtained by a non-lazy strategy.

To prove the theorem we first need the following lemma.

Lemma 1 (Value of Progress). Let q be a state and let x and x be two clock valuations which are identical except for x i = x i + δ. Then the value of (q, x ) is at least as good as the value of (q, x), that is, V (q, x ) ≤ V (q, x).

Sketch of Proof:

We prove it by induction on the number of transitions remaining between q and the final state.

Base case:Base case: When there is only one end transition pending and one active clock working toward a duration characterized by a time density ψ, the value is defined as

and the derivative dV /dx is negative (-1 and then -1/2). Hence V (q, x ) < V (q, x). Inductive case: suppose the lemma holds for all states beyond q. We will show that each action

The optimal partition of the decision surface is illustrated in Figure A.4-(a) with the grey areas indicating the subsets where where we need to compute. In each of this areas, the set Ω -1 (w) is upward closed with respect to . Any upward closed set can be written as a union of rectangular cones, but this union can be infinite, for example for a half-space which is not axes parallel and certainly for sets with a curved boundary. In the absence of some algebraic miracle that will turn Ω -1 (w) to be a finite union of zones, the best we can hope for is an approximation scheme.

In [START_REF] Legriel | Approximating the pareto front of multi-criteria optimization problems[END_REF], a multi-dimensional binary search algorithm was presented for approximating the boundary between an upward-closed set and its downward-closed complement. We show below how it can be applied to approximate the boundary between Ω -1 (w) and Ω -1 (s). Suppose we fix a point (q, x) in the decision surface and compute its value under s and under w. If V (q, x, w) < V (q, x, s) the optimal strategy satisfies not only Ω(q, x) = w but also Ω(q , x ) = w for any (q , x ) in the upward rectangular cone above (q, x), that is, any state satisfying (q, x) (q , x ) with no resource utilization between q and q . Likewise if V (q, x, w) > V (q, x, s) the optimal strategy is s for all points in the downward cone of (q, x).

By continuing in this manner, evaluating V on various states, we reach a situation in which the decision surface is partitioned into at most 3 parts: Ω s consisting of states where the optimal decision is known to be s, Ω w where the optimal decision is known to be w, and Ω ? which is the rest of the decision surface where we do not know yet, see Fig. A.4-(b). The technique of [START_REF] Legriel | Approximating the pareto front of multi-criteria optimization problems[END_REF] is geared toward reducing the distance between the boundaries of Ω s and Ω w and hence reducing the size of Ω ? . For any desired distance ε, the algorithm will converge after a finite number of evaluations of V .

Based on this partial knowledge we can derive an approximately optimal strategy, by selecting an arbitrary decision for all states in Ω ? . In the sequel we consider eager approximations that make s in all the states in Ω ? . How far is such a strategy from the optimal one? The following lemma bounds the derivative of V with respect to any of the clocks.

Lemma 2 (Derivative of V ). Let V be the value function associated with a problem then for every (q, x) and for every i ∂V ∂x i (q, x) ≥ -1

Sketch of Proof: Consider first the local value function of a process in isolation. In any state q, the domain of the clock is split into two parts. When x < a, the derivative is naturally -1.

When x > a the rate of progress is slower (because progress is combined with accumulation of optimism-contradicting information) and the magnitude of the derivative is smaller. 2 When running together, the progress of each process is bounded by its progress in isolation or by the progress of another process that blocks it. The progress of the expected termination of the last process (makespan) is bounded by the progress of each of the processes.

Lemma 3 (Approximation). Let x, x be two points such that x < x , d(x, x ) < ε, Ω(q, x) = s and Ω(q, x ) = w for the optimal strategy Ω. Consider an eager approximation Ω making s in all states (q, x ) ∈ Ω ? such that x ≤ x < x . Then for every such x we have |Ω(q, x ) -Ω (q, x )| ≤ ε.

Proof:

According to what we know about the optimal strategy we have V (q, x , w) < V (q, x , s) < V (q, x, s) < V (q, x, w)

and according to Lemma 2, V (q, x, w)-V (q, x , w) ≤ ε. For any x , V (q, x , s) and V (q, x , w) are inside the interval and the distance between them is bounded by ε.

00000000000000 00000000000000 00000000000000 00000000000000 00000000000000 00000000000000 00000000000000 00000000000000 00000000000000 00000000000000 00000000000000 00000000000000 00000000000000 00000000000000 00000000000000

This result gives a basis for an approximation procedure, however there will be, at least theoretically, a wrapping effect, because the approximation of the value at q will be used for computing the value of its predecessors, and a path that makes k decisions, in all of which the boundary is approximated with accuracy ε relative to its successor, can in principle, deviate from the optimal time-to-go by kε. But this is very theoretical and we expect real-life to behave much better.

Unfortunately, this part of the work has not been fully completed at the time of writing and we had to postpone the complete implementation and experimental evaluation to the future.