Le deuxième problème d'ordonnancement étudié analyse la consommation d'énergie sur une plate-forme multiprocesseur. En eet beaucoup de CPS évoluent dans des environnements restreints avec une quantité limitée d'énergie. Le dé principal de ce type de systèmes est de s'assurer qu'ils puissent accomplir leurs missions uniquement avec la quantité d'énergie initialement allouée. Pour formaliser les systèmes d'ordonnancement multiprocesseurs avec ressources énergétiques, nous étendons les modèles formels précédents avec des informations sur la consommation d'énergie. Après cela, en utilisant Cinco, nous donnons une représentation graphique au modèle formel. Ce modèle est constitué de deux couches. La première couche modélise la plate-forme matérielle avec un système d'ordonnancement composé de tâches temps réel et de CPUs. La deuxième couche modélise l'application qui est composée d'un ensemble d'actions. Une des contributions de la thèse est de proposer une nouvelle technique d'optimisation pour les ordonnanceurs multiprocesseurs. Cette technique détermine les mappages optimaux des tâches aux processeurs an de minimiser la consommation d'énergie du système et/ou le temps de réponse en utilisant des tests statistiques (ANOVA et Tukey HSD). Tout d'abord, nous déterminons tous les mappages possibles entre tâches et processeurs. Ensuite en utilisant Uppaal SMC nous évaluons la consommation d'énergie moyenne et le temps de réponse moyen de chaque mappage. Enn en utilisant les tests ANOVA et Tukey HSD nous comparons les moyennes et classons les mappages selon leurs consommation d'énergie et/ou temps de réponse. Nous présentons aussi un algorithme statistique de détection de changement appelé CUSUM. Le principe est de suivre l'évolution d'une mesure de probabilité à des intervalles de temps successifs au cours d'une seule exécution du système. L'algorithme détecte ensuite la position où la probabilité de satisfaire la propriété change de façon signicative. Pour mieux expliquer notre approche pour le problème de consommation d'énergie, nous proposons comme cas d'étude un système multiprocesseur se composant de deux niveaux. Le premier niveau consiste à un ensemble de composants qui comporte une série d'action à accomplir. Le deuxième niveau comporte un nombre de processeurs sur lesquels les tâches vont être exécutées. Chaque tâche est destinée à exécuter un ou plusieurs composants du système étudié. Les résultats des expériences réalisés sur ce modèle et leurs synthèses sont présentés en n du Chapitre 5. Le dernier problème étudie les fuites d'informations lorsque des processus avec différents niveaux de sécurité se partagent l'espace mémoire lors de leurs exécutions. Typiquement cela inclut le chargement d'informations condentielles, telles que les clés de chirement, les données médicales et les coordonnées bancaires, pour les utiliser dans des processus de haute sécurité. Ces informations condentielles doivent être étroitement contrôlée et ne pas être divulgué à des processus de faible niveau sécurité. Dans cette thèse nous proposons de traiter la condentialité, mesurée par le résultat de fuite d'informations sécurisées, en tant que ressource quantitative que l'ordonnanceur peut exploiter. Ce qui permet une meilleure quantication de la fuite qui en résulte dans diérents scénarios, ainsi que d'avoir une mesure claire du coût des diérents choix d'ordonnancement. En outre, cela permet la création de planicateurs qui peuvent faire de meilleurs choix de programmation et aussi respecter les contraintes de fuite d'informations condentielles. Nous présentons pour cela un nouveau modèle qui considère que les tâches doivent être composées d'étapes, chacune d'entre elles à un temps d'exécution, une valeur de fuite d'information et un niveau de sécurité. Chacune de ces étapes est implicitement une séquence atomique d'actions qui peuvent être prises dans une tâche sans interruption par le planicateur. Ainsi, une tâche consiste en une séquence ordonnée d'étapes à eectuer, qui donne le comportement total de la tâche.

Nous présentons aussi dans ce manuscrit une nouvelle approche pour résoudre le problème de fuite de l'information. Cette approche consiste à appliquer une procédure combinent des Pré-processus qui intervient sur un ensemble initial de tâches pour produire un nouveau ensemble de tâche. Les Post-processus interviennent sur la trace résultante de l'application d'un algorithme d'ordonnancement classique sur l'ensemble de tâche à planier. Pour cela, on a proposé un ensemble d'algorithmes pour les deux phases de notre procédure an de trouver la bonne combinaison pour réduire la fuite d'information.

Pour mieux illustrer notre approche, on a présenté les résultats des expériences qu'on a réalisées en n du Chapitre 6.

First of all, I have to thanks God who give me courage and faith that help me to nish this modest work.

I would like to thank my supervisor, Professor Axel Legay, for the patient guidance, encouragement and advice he has provided throughout my time as his student. I have been extremely lucky to have a supervisor who cared so much about my work, and who responded to my questions and queries so promptly. I would also like to thank all the members of TAMIS team who helped me in my work.

In particular I would like to thank Louis-Marie Traounouez, Thomas-Given Wilson and Fabrizio Biondi for their trust and invaluable support. I am very honored to thank the presence on my thesis jury and I would like to thank: Mr. Olivier Barais, Professor at the University of Rennes, for the honor he gave me by accepting to be the president of my thesis jury. I wish to assure him of my deep appreciation for his interest in this work.

Mrs Cristina Secelenau, Associate Professor at Malardalen University in Sweden, for the honor she gave me for her participation in my thesis jury as rapporteur of my work, for the time spent reading this thesis, and for the suggestions and the judicious remarks that she indicated to me. Mrs Tiziana Margaria, Professor at the University of Limerick, for the honor she gave me for her participation in my thesis jury as rapporteur for my work and for all the interesting remarks she made me made.

Mr Kim Guldstrand Larsen, Professor at Aalborg University, for having accepted to be part of the jury of this thesis. I thank him for the scientic advice he has given, and for his immense help in carrying out this work.

Mr. Saddek Bensalem, Professor at Grenoble Alpes University, for his interest in participating as a guest member of this jury.

On a more personal note, I warmly thank my wife Naima, for her continued support and encouragement. I also want to thank the patience of my mother, my father and my 1 brother who have experienced all the ups and downs of my research.

Completing this work would have been all the more dicult were it not for the support and friendship provided by the other members of TAMIS team, and the IRISA laboratory members in Rennes. I am indebted to them for their help. Those people, such as the postgraduate students at MathSTIC doctoral school, who provided a much needed form of escape from my studies, also deserve thanks for helping me keep things in perspective.

Résumé

De nos jours, les machines sont devenues une partie intégrante de notre vie quotidienne, elles sont utilisées dans diérents domaines comme les transports, l'industrie ou la médecine. Ces machines sont contrôlées par des logiciels et des programmes très complexes qui assurent la bonne exécution des taches aectées à ces machines. La plupart de ces machines doit communiquer avec le monde extérieur pour accomplir leurs missions, cette interaction exige que les systèmes qui contrôlent ces machines devraient avoir la possibilités de recevoir des données extérieurs, les traiter et donner les réponses adéquates dans le temps opportun. Ce type de systèmes est appelé Systèmes Temps Réel.

Les systèmes temps réel sont des systèmes de traitement d'information qui doivent répondre aux entrées reçues de l'extérieur, en vériant des contraintes temporelles strictes sur leur temps de réponse. Ces systèmes sont fréquemment utilisés dans des systèmes critiques tels que les systèmes embarqués, ce qui exige un très haut niveau de sécurité.

Une des principales problématiques pour développer ces systèmes est de vérier que ces contraintes temporelles seront toujours vériées, quelques soient les entrées reçues. En plus des contraintes de temps, d'autres contraintes peuvent être prises en considération, comme la consommation d'énergie ou la sécurité des données.

Plusieurs méthodes de vérication ont été utilisées ces dernières années, comme la révision attentive du code des programmes qui s'applique essentiellement sur les logiciels, ou le test qui consiste à réaliser un prototype et puis appliquer diérents tests pour vérier son exactitude. Cependant, avec la croissance de la complexité des logiciels embarqués, ces méthodes ont atteint leur limitation. C'est pourquoi les recherches se concentrent actuellement à développer de nouvelles méthodes et formalismes pour pouvoir vérier l'exactitude des systèmes les plus complexes.

Le principal travail de ce manuscrit porte sur le développement de techniques avancées d'ordonnancement basées sur des modèles formels. Le but est d'analyser et de valider la satisfaction d'un certain nombre de propriétés sur les systèmes temps réel, dont des propriétés non temporelles telles que la consommation d'énergie ou la fuite d'informations.

L'ordonnancement est un processus de prise de décision utilisé dans de nombreux domaines tels que la fabrication, l'industrie, la médecine et ainsi de suite. Il traite de l'allocation des ressources aux tâches sur une période donnée, et son but est d'optimiser un ou plusieurs objectifs.

Les ressources et les tâches peuvent prendre plusieurs formes diérentes. Les ressources peuvent être des machines dans un atelier, des pistes dans un aéroport, des unités de traitement dans un environnement de calcul, et ainsi de suite. Les tâches peuvent être des opérations dans un processus de production, l'atterrissage dans un aéroport, l'exécutions de programmes informatiques, etc. Chaque tâche peut avoir un certain niveau de priorité, un instant de début et une date d'échéance. Les objectifs peuvent également prendre plusieurs formes diérentes. Un objectif peut être la minimisation du temps d'achèvement de la dernière tâche. Un autre peut être la minimisation du nombre de tâches accomplies après leurs échéances respectives. L'ordonnancement, en tant que processus décisionnel, joue un rôle important dans la plupart des processus de fabrication et des systèmes de production ainsi que dans la plupart des environnements de traitement de l'information. Dans les systèmes temps réel l'ordonnancement consiste à planier de l'utilisation des ressources de calcul de façon à satisfaire toutes les contraintes temporelles. Pour illustrer les travaux réalisés pour résoudre ce premier problème, nous présenterons les résultats de nos expériences réalisées sur un cas d'étude qui consiste en un système de contrôle d'un aéronef. Ces expériences qui consistent à vérier la possibilité dâordonnancement des tâches du système étudié de façon hiérarchique, du plus bas niveau vers le haut. Le but nal est de calculer le budget minimal nécessaire pour l'ordonnancement du système global.

Introduction

Softwares became an important part of our daily life as they are now used in many heterogeneous devices, such as our phones, our cars, our home appliances, etc. Modern cars for example are dotted with a number of embedded softwares, each handling a specic task, like braking, airbags or fuel injection. These embedded softwares are designed to run inside larger systems with various and heterogeneous hardware and limited resources.

Communication systems, mobile phones, medical systems, transport are using a vast amount of embedded software. The use of embedded softwares is motivated by the exibility and the simplicity that these softwares can guarantee, and to minimize the cost.

These embedded softwares are designed to run in specic environments with limited resources. This forces the developers to optimize the size, the cost, the power consumption, the reliability and the performance.

Cyber-Physical System (CPS) are softwares used to control physical systems. CPS are often embedded and run in real-time, which means that they must react to external events. A complex CPS can contain many real-time systems. Then a major challenge is to nd an optimal policy to share system resources that guarantee the accomplishment of the missions of the CPS. The fact that these systems can be used in critical domains like medicine or transport requires a high level of safety for these systems.

Real-Time Systems by denition are processing information systems that have to respond to externally generated inputs, and they are called real-time because their response must respect strict timing constraints. Therefore, the correctness of these systems does not depend only on the correctness of their treatment results, but it also depends on the timings at which these results are given.

The main problem with using real-time systems is the diculty to verify their timing constraints. A way to verify timing constraints can be to use Scheduling theory which is a strategy used in order to share the system resources between its dierent components. In addition to the timing constraints, other constraints should be taken into consideration, like energy consumption or security.

Several verication methods have been used in the last years, but with the increasing complexity of the embedded softwares these methods reach their limitation. That is why researchers are now focusing their works on nding new methods and formalisms capable of verifying the correctness of the most complex systems.

Today, a well-used class of verication methods are model-based techniques. These techniques describe the behavior of the system under consideration using mathematical formalisms, then using appropriate methods they give the possibility to evaluate the correctness of the system with respect to a set of properties.

The main work in this manuscript is about using model-based techniques for developing new advanced scheduling techniques in order to analyze and validate the satisability of a number of properties on real-time systems. The main idea is to exploit scheduling theory to propose new techniques in order to analyze dierent properties like energy consumption or information leakage.

Thesis Structure The remainder of the manuscript is composed as follows:

Chapter 1 presents an introduction about scheduling real-time systems. Scheduling is a decision-making process that is used in many domains such as manufacturing, industry, medicine and so on. It deals with the allocation of resources to tasks over given time periods and its goal is to optimize one or more objectives.

The resources and the tasks can take many dierent forms. The resources may be machines in a workshop, runways at an airport, processing units in a computing environment, and so on. The tasks may be operations in a production process, take-os and landings at an airport, executions of computer programs, and so on. Each task may have a certain priority level, an earliest possible starting time and a due date.

The objectives can also take many dierent forms. One objective may be the minimization of the completion time of the last task and another may be the minimization of the number of tasks completed after their respective due dates.

Scheduling, as a decision-making process, plays an important role in most manufacturing and production systems as well as in most information processing environments.

It is also important in transportation and distribution settings and in other types of service industries. methods presented before show their limitation to handle these kinds of systems.

Another kind of methods can be used to verify the correctness of complex real-time systems, basing on the behavior of these systems a model is created and using appropriate algorithms and techniques the correctness of the system can be checked. In this chapter, we present general models that can be used in order to represent the behavior of the system under consideration.

Finally, we present in this chapter dierent types of real-time scheduling algorithms.

Scheduling algorithms are categorized according to the policy used to assign resources to the dierent processes that need to be executed.

Chapter 2 presents the models used to describe the behavior of real-time systems.

First, we dene transition systems which are oriented graphs that can be used to describe the behavior of the system under consideration using locations to dene the dierent states of the system and edges to describe the transition from a state to another.

Second, we introduce timed automata for specifying timing constraints. Timed automata are an extension of transition systems with timing aspects called clocks. Clocks are used to describe the timing constraints during the execution of real-time systems.

In particular clocks control the amount of time that the system can stay in each state, and the timing constraints for a transition from a state to another. We also introduce extensions of timed automata for specifying scheduling mechanisms or energy concerns.

In this chapter, we present our rst contribution that consists of a new stochastic model for stochastic tasks and a dispatcher in order to model the variation of execution time with respect to the computation logic. This representation is very important in order to model complex real-time systems behavior.

Finally, we present the model-based approach used in our work to specify scheduling problems with the formal models previously introduced. We rst give a view about precedent works done in this eld. Then we present the formal models of the components of the scheduling systems analyzed in our work.

Chapter 3 presents the languages used to express correctness properties of RTS and the techniques used to verify these properties. Temporal logics are formalisms used to express the timing constraints of the properties needed to be veried with a mathematically precise notation. Temporal logics express constraints over sequences of events.

After that, we present an automated verication method called model checking (MC) that we use to verify the satisability of properties described using the logic above on a given model. This method proceeds by exploring all possible executions of the model in a brute-force manner and checks the satisability of the property under consideration on each execution. The result will be positive, i.e. the model satises the property, or negative, i.e. the model does not satisfy the property. If the result is negative, a counter example will be given and analyzed to explain the violation of the property, and to update the model or the system design to correct these problems. . We also present an alternative to model checking called statistical model checking (SMC) that reasons about average scenarios to quantify the probability of satisfying a property. This method is used to handle the state explosion problem, i.e. the number of states needed to model the system accurately may easily exceeds the amount of available computer memory.

The last part of this chapter presents a high level language called Cinco that we used in our work to have a graphical description of the models under consideration.

Cinco can be used to make a graphical representation of the models that describe the dierent components of the system. This graphical representation will be translated to formal models and then the dierent properties can be checked on these models using the model-checking tool Uppaal. The results of the formal verication can be parsed and the most relevant information can be graphically displayed.

Chapter 4 presents our rst model for analyzing Hierarchical Scheduling Systems (HSS). HSS are complex scheduling systems with multiple scheduling algorithms. We rst introduce a new model-based compositional framework with stochastic real-time tasks in a HSS. This framework is designed with timed automata and probabilistic timed automata that constitute a model bank to describe HSS. In particular we introduce new probabilistic timed automata (PTA) models to instantiate stochastic tasks where task real-time attributes, such as deadline, execution time or period, are characterized by probabilities. This allows to design generic models that cover more cases of CPS.

Then we encapsulate this formal framework into Cinco, a generator for domainspecic modeling tools. Cinco allows to specify the features of a graphical interface in a compact meta-model language, and it generates automatically from this meta-model specication a domain specic analysis tool with a graphical interface. scheduling system. Finally, we illustrate our framework with a case-study and the results of our experiences.

Chapter 5 presents our study of Energy Consumption of Multi-Processor Scheduling Systems. Many CPS are mission critical systems, it means that these systems have a specic mission to achieve with a limited amount of energy. Number of researches focused on analyzing these systems by verifying that the system can accomplish its mission only using its initial budget of energy.

To formalize multi-processor scheduling systems with energy resources, we extend formal models presented in the precedent chapter with information about energy consumption. After that, using Cinco we give a graphical representation of the formal model.

The graphical representation consists of two layers. The rst layer, platform layer, models the hardware platform with a scheduling system composed of real-time tasks and CPUs. The second layer, application layer, models the application that is composed of a set of actions.

In this chapter we present a new optimization technique for multi-processor scheduling system. It determines optimal mappings from tasks to processors in order to minimize the energy consumption of the system and/or response time using statistical tests (ANOVA and Tukey HSD). First, we determine all the possible schedulable mapping from tasks to processors. Using Uppaal SMC we evaluate the energy consumption and the response time of each schedulable mapping. After that, using statistical test ANOVA we determine if the means of the treatments are signicantly dierent. If it is the case we use Tukey HSD to compare the means of every treatment to the means of every other treatment. Based on this comparison, we classify the precedent mapping according to their energy consumption and/or response time. Finally, we choose the appropriate mapping according to the property needed to be veried.

In this chapter also, we present a statistical algorithm for change detection called CUSUM. The principle is to monitor the evolution of a probability measure at successive positions during a single execution of the system. The algorithm then detects the position where the probability to satisfy the property changes signicantly. use within high-security processes. These condential pieces of information may be vital to the operation of the high-security processes, but must also be tightly controlled and not be leaked to low-security processes.

In this chapter we propose to treat condentiality, measured by the resulting leakage of secure information, as a quantitative resource that the scheduler can exploit. This allows for a better quantication of the resulting leakage in dierent scenarios, as well as having a clear measure of the cost of dierent scheduling choices. Further, this allows for the creation of schedulers that can make better scheduling choices and also respect condential information leakage constraints.

In this chapter we present also a new model that considers tasks to be composed of steps, each of which has an execution time, leakage value, and security level. Each one of these steps is implicitly an atomic sequence of actions that can be taken within a task without preemption by the scheduler. Thus a task consists of an ordered sequence of steps to be performed, that yields the total behavior of the task.

Chapter 1

Real-Time Scheduling

In this chapter, we give a brief introduction about real-time systems scheduling theory.

Scheduling this kind of systems must take on account the timing constraints of these systems. Generally speaking, scheduling these systems consists in nding a schedule for the processes of the system such that all the processes respect their timing constraints.

Solution will be considered true if all the processes respect their timing constraints. First, we introduce the main techniques for analyzing real-time system. Second, we present the main concepts of tasks and jobs used to design real-time scheduling systems. Finally, we present some examples of scheduling algorithms and we list the properties that must be satised.

Introduction

Cyber Physical System (CPS) are software-implemented control systems that control physical objects of the real world. The physical system observes the environment by means of its sensors. The software receives the information from the sensors and sends signals to actuators. The information sent by sensors can be periodic or irregular depending on the events happening in the environment. In all cases the system must react to these demands, and there will be a time bound for the response that must be respected.

The software must be able to deal with the case where there is more than one treatment to do and where each one of these treatments have a time constraints.

CPS have to schedule the computation between all the received requests in order to satisfy each treatment to get response within its required time bound. The no respect of the treatment time bound by the software can have dierent consequences, in some cases it can have no negative consequence, in other cases it can have a few negative consequences that can be solved, but in other case it can have disastrous consequences.

The correctness of these systems is not only based on the correctness of the results given by the system, but on the time when those results are given too. That is why the timing constraints are as important as the correctness of the results given.

In this chapter we present basics about the model formalizing of the CPS systems used in our work. First we give a brief denition of the dierent methods used to analyze real-time systems, then we present the formalizing model used in our work. After that we present the dierent algorithms used to analyze scheduling problems. Finally, we present the dierent kinds of properties that can be analyzed on this model.

Analysis Techniques for Real-Time Systems

The criticality of the real-time systems requires ecient analysis methodology to verify the correctness of these systems. A number of existing techniques can be used to analyze these systems. Peer reviewing and testing are the most used verication techniques for the software systems in practice. For hardware analysis there exists other techniques like emulation or simulation.

Peer reviewing consists of the inspection of the software statically in order to nd any problem, this inspection is done before the compilation of the software by a neutral engineer group, preferentially that has not been involved in the software development. The testing technique gives test values to the compiled software and observes the treatment results, basing on this observation weather the correctness of the system is satised or not.

The emulation technique is a kind of testing used to verify hardware systems, it consists of conguring the emulator to behave like the hardware under consideration and in the same way as the testing technique, it gives test values to the emulator and compares the generated output with the expected output to decide the correctness of the system under consideration. Simulation consists in constructing a model for the hardware that simulates this hardware. Simulation is like testing, but it is applied on a model. The main limitation of this method is that simulation gives a possible scenarios to the system execution, but the number of scenarios to be checked to get high condence about the correctness of the system can be very high and cannot be accomplished by a simulator in a reasonable way.

Formal techniques are very used to analyze complex real-time systems, the general idea is to apply a number of mathematical techniques on a Model to verify the satisability of a number of Properties. The model is an abstraction describing the real-time system, it represents the behavior of the system respecting the time constraints. The properties can be results that the system must produce or specic behaviors of the system.

In the next section, we will present a general model to describe dierent components of real-time systems.

Tasks and Jobs

In this section we present a formalization of a real-time system. As we mentioned before, real-time systems are such that the correctness do not depend only on the correctness of the results, but also on the time when these results are given. A real-time system is normally composed of a number of tasks, also called threads. Each task is designed to accomplish a specic work. Each time the task recurs it is called a job. The job is instantiated at a regular time or not depending on the task nature, the jobs are periodically produced if the task is periodic. According to the system architecture the Jobs are executed on one or dierent processors, but at given instant a processor is able to execute only one Job, processor here refers to a single core architecture.

We can divide the nature of the tasks on two categories, soft and hard tasks. Denition 1.1 (Soft tasks). We designate soft tasks those for which meeting their time constraints is not necessary, this means it is acceptable that this category of tasks do not nish its work before its deadline. Denition 1.2 (Hard tasks). We designate hard tasks those for which meeting their time constraints is mandatory, this means it is not acceptable that this category of tasks do not nish its work before its deadline. The no respect of their time constraints can have disastrous consequences on the system.

The events happening in the environment in which the real-time system performs are picked up by the system sensors. The system receives the information given by sensors and aects each treatment to a specic task. The tasks can be periodic or aperiodic depending on the nature of the treatment. Denition 1.3 (Periodic tasks). We call periodic tasks those where the task is repeated after a xed amount of time called Period P , they are called Time-triggered.

A simple example of real-time systems with periodic tasks, is the trac light system. Each light is turned on for a xed amount of time, that can be modeled as the execution time E before it is turned o. The amount of time between every two activations of the light can be modeled as the period. Denition 1.4 (Aperiodic tasks). We call aperiodic tasks those which have an irregular arrival time, they are called Event-triggered.

A simple example of an aperiodic task is the air-bag activation system, if there is a collision the sensor sends the signal to the system, the system takes the power of the collision and evaluates the necessity to activate the air-bag or not, if yes the system sends a signal to the actuator to activate the air-bag, all these treatments must be done with a time constraint to guarantee the safety of the conductor.

It is a great diculty to represent such aperiodic tasks. A solution is to model these kinds of tasks using sporadic tasks. Denition 1.5 (Sporadic tasks). Sporadic tasks are such that their period can be modeled using dierent probability distributions in order to have a bound on the task arrival time.

Each task or job is characterized by the following parameters, the release time, execution time and the deadline.

Period P is the minimal amount of time between two consecutive jobs. For periodic task, period P is a xed value. For aperiodic tasks, period P cannot be dened because their arrival time are irregular. For sporadic tasks, period P is a bound on the task arrival time that can be modeled using dierent probability distributions.

Release Time is the date at which a job is instantiated. If the job is instantiated from periodic tasks, the release time R of the job is computed by the following formula: R = (n -1) * P , where n is the number of the job and P is the period of the task. If the job is instantiated from aperiodic task, the release time R of the job cannot be predicted because the release time of the task is irregular.

Execution time E is the time needed by each task or job to nish its execution. We can dene several types of execution time: best case execution time BE, is the minimum time needed by the task or job to nish its execution; worst case execution time W E, is the maximum time needed by the task to nish its execution.

Deadline D is the time at which the task or job must nish its execution relative to the release time, we call it relative deadline.

Scheduling Algorithms

For a given set of jobs, the scheduling problem is to nd an order for which all the jobs are executed satisfying all their time constraints. Usually, each job is parametrized by its release time R, its absolute deadline A, its execution time E and resource requirements.

Each job execution may or may not be interrupted (preemptivity). The order given by the scheduler must be respected, it means that each job cannot be executed before the complete execution of its predecessors.

We can distinguish two types of scheduling techniques, static techniques called o-line techniques and dynamic techniques called on-line techniques.

O-line Scheduling Algorithms

We designed an o-line scheduling algorithms systems that have an entire knowledge about the set of jobs scheduled, the scheduler have knowledge about each task, its release time, execution time and deadline before beginning the execution. This type of algorithms is mostly used when the system contains periodic tasks only.

On-line Scheduling Algorithms Contrary to the o-line algorithms, the on-line algorithms have a partial knowledge about the set of jobs scheduled, the scheduler receives requests at any time and must answer these requests. This kind of algorithms is suited to handle the scheduling of aperiodic tasks, because the aperiodic tasks produce jobs at an irregular time. That is why the scheduler cannot have an entire knowledge about the arrival time of the aperiodic tasks.

Scheduling algorithms can also be classied according to the policy used for the classication of the ready jobs for execution. The jobs are classied according to their criticality, the most critical job must be executed in rst and so on. This criticality can be expressed using a priority value where the job with the highest priority value will be executed rst. The scheduling algorithms can be classied into two classes xed priority and dynamic priority scheduling algorithms.

Fixed Priority Algorithms Fixed priority algorithms are those where the priorities of the tasks do not change during the execution time. The priority of each task is xed at the design time according to the criticality of the task, and this priority will not be aected during the execution.

A good example of the xed priority algorithms is the Rate Monotonic Algorithm (RM), this algorithm assigns the highest priority to the task with the smallest period P . Dynamic Priority Algorithms Dynamic priority algorithms are those where the priorities of the tasks are calculated on the y during the execution time of the system.

The scheduler calculates the priorities depending on the tasks parameters.

An example of the dynamic priority algorithm is the Earliest Deadline First (EDF).

EDF determines the priority of jobs according to their absolute deadline, at any given point of time, out of the currently available jobs, the job with the earliest absolute deadline is scheduled rst.

In some cases, the real-time system requires that some specic tasks must be executed in priority over the other tasks. For that, the scheduler can stop the execution of a lower priority task in order to promote another high priority task. The interruption action called preemption can be used by preemptive scheduling algorithms. Other algorithms are non-preemptive scheduling algorithms.

Preemptive Scheduling Algorithms We call Preemptive Scheduling Algorithms those accepting that a job in execution can be preempted (stopped) by another job with a higher priority. The precedent job is returned to the ready queue in order to nish its execution.

Non-Preemptive Scheduling Algorithms Contrary to the precedent kind of algorithms, the non-preemptive ones do not accept that a running job can be preempted.

The running job keeps all the necessary resources until nishing its execution even if there is another job with a higher priority that needs to be executed.

The preemptivity of the scheduling algorithms depends on the nature of the job and the priority of its execution, some jobs must be executed rapidly because of their criticality. That is why these jobs must have a higher priority value. The priority of each job can be xed by the system constructor in advance, or can be calculated according to the tasks attributes. Mixed systems are also possible, the system can accept preemptivity but in the same time can guarantee for some jobs to be executed without be preempted.

Example Let consider the two periodic tasks T 1 (3, 3, 2) and T 2 (6, 6, 2), where T 1 has a period of 3 units time and must nish its computation before 3 units time with an execution time of 2 units time. T 1 has a period of 6 units time and must nish its computation before 6 units time with an execution time of 2 units time. Let consider that T 1 has a higher priority than T 2 . Figure 1.1 represents a possible execution of T 1 , T 2 on a single processor platform using a non-preemptive scheduling algorithm. Let consider that the release time of both tasks is zero, the task T 1 is executed rst because its priority is higher. Task T 1 nishes Figure 1.1 Example of scheduling two tasks using a non-preemptive Scheduling algorithm its execution after 2 time units. Then the task T 2 begins its execution. A new job of task T 1 is instantiated at time 3, but at this moment the processor is not available because the task T 2 is running. Task T 1 must wait until task T 2 nishes its execution. Even if we know that T 1 has a higher priority than T 2 , the non-preemptive algorithm protects T 2 from any interruption before nishing its execution. Figure 1.2 represents another possible execution of the precedent model using a preemptive scheduling algorithm. Task T 1 is executed rst because its priority is higher.

Task T 1 nishes its execution after 2 time units. Then task T 2 begins its execution.

A new job of task T 1 is instantiated at time 3, this time the algorithm interrupts the execution of the running job since a higher priority task needs to be executed. The job instantiated by task T 1 at time 3 will interrupt the execution of T 2 in order to be executed. Task T 2 will resume its execution when T 1 nishes its execution. The principal objective of analyzing real-time systems is to verify that these systems accomplish their designated work correctly while respecting time constraints. The correctness of the results, and the time constraints are modeled as properties. These properties can be classied generally on two main classes, safety and liveness properties.

Safety Properties Safety Properties are those that declare that something bad never happens. Generally, safety requirements means that the system does not have any deadlock or any similar state that can crash the system.

Deadlock is considered as a safety property. We call deadlock the states where the system cannot progress, like interminable loops or terminal states. In such systems terminal states are undesirable and mostly represent a design error. A simple example of deadlock scenario occurs when several components wait for the progress of the other component.

A way to verify safety properties is to search using specic algorithms in the set of states of the system about any undesirable state like state where the system do not nish its work but in the same time the system cannot progress any more. This search should outputs a trace with a counter example leading to the deadlock problem.

Another important safety property is the schedulability property, this property consists of verifying that each component of the system nishes its treatment respecting its time constraints.

Example An example of safety property, the mutual exclusion problem. A simple logical representation of this problem is ¬(T 0 ∧T 1 ), it means that the Task T 0 and Task T 1 cannot be in the critical section at the same time.

Liveness Properties Contrary to safety properties, liveness properties attest that something good will eventually happen, safety properties are violated within a nite time, while liveness properties are violated in an innite time. For example the liveness property in the mutual exclusion problem can be presented as follow:

Each task must enter its critical section.

Each task must enter its critical section each time it is needed.

Each waiting task must enter its critical section in some time in the future.

From what we see above, the fact that real-time systems are today used in many critical domains of our live, their correctness becomes a primordial necessity. Over the years, many methods have been used to analyze the correctness of these kinds of systems. In this thesis, we focus our work on model-based methods. These methods design a model to describe the behavior of the real-time system under consideration, and apply dierent techniques to analyze the correctness of this system. The next chapter describes a wellused model to describe this kind of systems.

The next chapter presents formal models used in our work to model, veries and validates real-time systems.

Chapter 2

Formal Models for Scheduling

Real-Time Systems

This chapter introduces formal methods in order to model, verify and validate real-time systems using discrete event models extended with time. This formal model gives us the possibility to represent the behavior of complex systems with their timing constraints. This representation can be exploited by formal methods in order to verify the satisfaction of specic properties on the system under consideration. In this chapter we present the transition system theory to represent the discrete behavior of the system. Then we add timing constraints to represent real-time systems, and stochastic constraints to represent systems with complex behaviors or real-time systems. To do that, we use the time automata. Finally we present the model-based method that we use in our work, and we present some models of scheduling components.

Key Contributions

In this chapter we present new stochastic models for stochastic tasks and dispatcher in order to model the variation of execution time with respect to the computation logics. This representation is very important in order to model complex real-time systems behavior.

Introduction

Today, formal methods became one of the most used techniques for analyzing real-time systems. The possibility of analyzing complex systems make the use of this methods very desirable in the design process of the real-time systems. During the last two decades, research in formal methods has led to the development of some very promising verication techniques that facilitate the early detection of defects. These techniques are accompanied by powerful software tools that can be used to automate various verication steps.

Model-based verication techniques are based on models describing the possible behavior of the system under consideration in a mathematically precise and unambiguous manner. Such problems are usually only discovered at a much late stage of the design.

The system models are accompanied by algorithms that systematically explore all states of the system model in order to detect any undesirable behavior. This chapter rst introduces transition systems, a standard class of models to represent systems under consideration. Dierent aspects for modeling concurrent systems are treated, ranging from the simple case, in which processes run completely autonomously to more realistic settings, where processes communicate in some ways.

Then to model real-time systems we need a model that takes into account timing aspects. For that we introduce timed automata. That is an extension of transition systems with clocks to handle timing aspects. Finally, we present a model-based framework based on timed automata to describe scheduling systems.

Transition Systems

Denitions

Transition systems can be used to model the behavior of real-time systems. Transition systems are oriented graphs containing nodes and edges. The nodes represent the state (or location) of the system in a specic moment of its behavior. The edges represent the transitions from a state to another state. As an example the state of the trac light is the current color of the light and the edge is the switch from one color to another.

There exist dierent types of transition systems. In our work we decide to use transition systems with action names on the edges and atomic propositions on the locations.

The action names on the edges describe communication mechanisms of the system processes controlling the transition from one location to another. The atomic propositions express dierent characteristics of the system at this moment. AP is a set of atomic proposition; L : S → 2 AP is a labelling function.

The transition system starts at some initial location l 0 , where l 0 ∈ I, and progresses according to its set of transitions E. The transition system moves from location l to another l and executes an action α ∈ Act, which we write l α -→ l . In case the location l has more than one outgoing edge, it is important to precise that the next edge is chosen in a non-deterministic manner. In the following we denote actions using Greek alphabet (such as α or β).

Each location in the transition system contains one or more atomic proposition a ∈ AP . These propositions express some knowledge about the system at this state. The atomic propositions will be denoted using letters from the beginning of the alphabet (such as a, b, c ..). Examples of atomic propositions are "light is green" or "x equals 2".

The labeling function L relates a set of atomic propositions L(l) to a location l. The labeling function stands for the atomic propositions a ∈ AP satised by the location l. --------→ of f Denition 2.2 (α_successors and α_predecessors). Let consider T S = {Loc, Act, E, I, AP } a transition system. For l ∈ Loc and α ∈ Act, the set of α_successors of l is dened as follow:

P ost(l, α) = {l ∈ Loc | l α -→ l }.
To generalize we write P ost(l)

= α∈Act P ost(l, α)
The set of α_predecessors is dened as follow:

P re(l, α) = {l ∈ Loc | l α -→ l}.
To generalize we write P re(l) = α∈Act P re(l, α) Each location l in the α_successors (resp. α_predecessors) set is a direct successor (resp. predecessor) of the location l.

Denition 2.3 (Terminal Location

). Terminal locations, also called blocking locations, are locations without any outgoing transition. When a transition system reaches a terminal location the system execution terminates.

It is important to precise that terminal locations are used to represent the ending of the system running. In some type of systems, this kind of locations is undesirable.

Paths and Traces

Let consider T S = (Loc, Act, E, I, AP ) a transition system, the executions (or paths) of the transition system dene its possible behaviors. Denition 2.4 (Path Fragment). A sequence of locations, π = l 0 l 1 l 2 ...l n (when the sequence is nite) or π = l 0 l 1 l 2 ... (when the sequence is innite) is called:

A path fragment if ∀i, l i+1 ∈ P ost(l i ), it means for each location l i in the path the next location l i+1 is a direct successor of the state l i . Initial path fragment if the sequence is a path fragment and the rst location of the sequence l 0 is an initial location, i.e l 0 ∈ I.

Maximal path fragment if the sequence is a path fragment and the last location of the sequence do not have a direct successor, i.e P ost(l n ) = ∅ or the sequence π is innite. Denition 2.5 (Path). A sequence of locations is called a path if the sequence is an initial and maximal path fragment.

As an example π = off on off on... is a path of the transition system describing the behavior of the light switch example.

Let consider a transition system TS. Let Paths(TS) denote the set of all paths in TS. Denition 2.6 (Trace). Let TS be a transition system with no terminal locations, it means that all its paths are innite. If π = l 0 l 1 l 2 ... is an innite path, its trace is dened as follow:

T race(π) = L(l 0 )L(l 1 )L(l 2 )... We denote by Traces(TS) the set of all traces of the transition system (TS), it is dened by T races(T S) = {T race(π), π ∈ P aths(T S)}

Timed Automata

In the precedent section, we have presented transition systems as a way to model the behavior of real-time systems. But until now, we did not present how to model the timing aspects of these systems, that is, information about residence time in a state or the possibility of taking a transition within a timing interval. These information give us the possibility to verify the satisability of the timing constraints of the real-time system under consideration.

As a modeling formalism for real-time systems, the notion of timed automata has been developed, an extension of transition systems with clock variables that measure the elapse of time. This model includes means to impose constraints on the residence times of states, and on the timing of actions.

Clocks and Clock Constraint

Timed automata are used to model the behavior of time-critical systems, time is a continuous entity. That is why to express the timing information it uses real-valued variables called clocks. All clocks in a system progress at the same rate. The only operations possible on a clock are reading the value of the clock and resetting the clock to zero.

Intuitively, a clock represents the amount of time elapsed since the last reset of the clock.

In timed automata we reason about timing aspects in an abstract way as a sequencing of events.

To express the variations of the clocks values, we use a valuation function v : C → R + that assigns to each clock c ∈ C a non-negative value v(c). For an element t of R + and a subset x ⊆ C, the valuations v + t and v[x ← 0] are dened as follow:

(v + t)(c) = v(c) + t for each clock c ∈ C v[x ← 0](c) =          0 if c ∈ x v(c) otherwise
To express conditions over clocks, we use clock constraints. Clock constraints can be used on location and transition. In the rst case, it is called a location Invariant.

The location invariant represents the time allowed to the system to stay in this location.

When the invariant does not hold, the location must be left. In the second case, it is called a Guard. A transition is available as long as the guard holds. When the guard evaluates to false, the transition cannot be taken. Denition 2.7 (Clock Constraint). A clock constraint over a set of clocks C can be written according to the following grammar:

g ::= c < k | c k | c > k | c k | g ∧ g
where k ∈ N, and c ∈ C. We denote CC(c) the set of clock constraints over the set C. We write v ϕ when valuation v satises the clock constraint ϕ.

Note that:

A clock constraint can be written in an abbreviated mode, i.e. (c

k 1 ) ∧ (c k 2 ) can be written as c ∈ [k 1 , k 2 ], where k 1 , k 2 ∈ IN; Clock dierence constraints as c 1 -c 2
k can be added using a more complex theory, in this work we focus on atomic clock constraints, without any dierence.

Syntax and Semantics of Timed Automata

A timed automaton is a transition system extended with a nite set of real-valued clock variables and clock constraints.

Denition 2.8 (Timed Automaton). A timed automaton is a tuple T A = (Loc, Act, C, E, I, Inv, AP, L) where:

Loc is a set of locations;

Act = Act i Act o { }
is the set of actions, where Act i is a set of input actions, Act o is a set of output actions and is an internal action;

C is a set of clocks;

E ⊆ S × CC(C) × Act × 2 C × S is a set of edges.
I ⊆ S is a set of initial locations;

Inv : S → CC(C) is a

function assigning invariants to locations;

AP is a set of atomic propositions;

L is a set of labelling.

Edges are labeled with the tuple (g, α, D), where g ∈ CC(C) represents the guard that must hold to enable the transition, α ∈ Act is an action and D ∈ 2 C is the set of clocks that must be reset to zero when the transition is taken. Intuitively, l g:α,D

---→ l means that the timed automaton can move from location l to location l when the guard g holds. When moving from location l to location l , each clock in the set D will be reset to zero and the action α is carried out. The function Inv assigns to each location a location invariant that indicates the amount of time that the timed automaton can stay in the designated location.

To represent timed automaton we adopt the drawing conventions for transition sys- Example Figure 2.2 describes a simple timed automaton with a single clock x and some possible evolution of this clock through time. In Figure 2.2a, we can distinguish two guards, the rst guard x 2 means that the system cannot move from location l 0 to location l 1 before (2) time units, the second guard x 4 means that the system can move from location l 1 to location l 0 if the clock x is less or equal to (4) time units. When the system takes the transition from location l 1 to location l 0 the clock x is reset to zero. have any restriction about the time passed in each location, that is why if the system stays in one of the two locations more than (4) time units, then the system cannot take anymore the transition from location l 1 to the location l 0 due to the restriction on the clock x.

In Figure 2.2c, we add two invariants, the rst invariant y 3 in location l 0 to ensure that the system cannot stay more than (3) time units in location l 0 , the second invariant y 4 means that the system must move from location l 1 to location l 0 before (4) time units. These two invariants avoid that the system is blocked in any location.

Operational Semantics The semantics of a timed automaton are dened as a transition system where a state or conguration consists of the current location and the current values of clocks. There are two types of transitions between states. The automaton may either delay for some time (a delay transition), or follow an enabled edge (an action transition). Denition 2.9 (Operational Semantics). The semantics of a timed automaton is a transition system (also known as a timed transition system) where states are pairs (l, u), and transitions are dened by the rules:

l, u d -→ l, u + d if u ∈ I(s) and (u + d) ∈ I(l) for a non-negative real d ∈ R + ; l, u a -→ l , u if l g:a,r ---→ l , u ∈ g, u = [r → 0]u and u ∈ I(l ).

Parallel Composition of Timed Automata

A practical manner to model complex systems consists of using parallel composition of timed automata. This makes it possible to model time-critical systems in a compositional manner. We consider a parallel composition operator, denoted .

Let consider the two following timed automata

T A 1 = (Loc 1 , Act 1 , C 1 , E 1 , I 1 , Inv 1 , AP 1 , L 1 ) and T A 2 = (Loc 2 , Act 2 , C 2 , E 2 , I 2 , Inv 2 , AP 2 , L 2 ), with Act 1 0 ∩ Act 2 0 = ∅. The timed automaton T A = T A 1 T A 2 is a tuple T A = (Loc, Act, C, E, I, Inv, AP, L)
dened as follow:

Loc = Loc 1 × Loc 2 is the set of locations; Act = Act i Act o , where Act i = Act 1 i \Act 2 o ∪ Act 2 i \Act 1 o and Act o = Act 1 0 ∪ Act 2 o is the set of actions; C = C 1 C 2 is the set of clocks; I = I 1 ∪ I 2 is the set of initial locations; Inv(s 1 , s 2 ) = Inv 1 (s 1 ) ∧ Inv 2 (s 2
) is the set of invariants for the new location (s 1 , s 2 );

L( l 1 , l 2 ) = L(l1) ∪ L(l 2 ) is the set of labels
The set of the edges is dened as follow:

If (l 1 , a, α 1 , c 1 , l 1 ) ∈ E 1 with a ∈ Act 1 \Act 2 then for each location l 2 ∈ Loc 2 ((l 1 , l 2 ), a, α 1 , c 1 , (l 1 , l 2 )) ∈ E; If (l 2 , a, α 2 , c 2 , l 2 ) ∈ E 2 with a ∈ Act 2 \Act 1 then for each location l 1 ∈ Loc 1 ((l 1 , l 2 ), a, α 2 , c 2 , (l 1 , l 2 )) ∈ E; If (l 1 , a, α 1 , c 1 , l 1 ) ∈ E 1 and (l 2 , a, α 2 , c 2 , l 2 ) ∈ E 2 with a ∈ Act 1 ∩ Act 2 then ((l 1 , l 2 ), a, α 1 ∧ α 2 , c 1 ∪ c2, (l 1 , l 2 )) ∈ E;
The location invariant of a composite location is simply the conjunction of the location invariants of its components. For α ∈ Act, the guard of the synchronized transition is dened by the conjunction of the guards of the transitions in the initial timed automata.

That implies that each action in Act can only be taken if it is true in both timed automata.

The clocks that are reset in the initial automata are all reset. The operator is associative for a xed set Act.

Example Parallel composition can be done by synchronizing inputs and outputs in a broadcast manner. This means that when an TA executes one output, all those TA that can receive it must be synchronized. We denote input actions with a channel name followed by ? and output actions with the channel name followed by !.

Hybrid Time Automata

Hybrid automata [START_REF] Henzinger | The Theory of Hybrid Automata[END_REF] are an extension of timed automata that extends the dynamic of clocks with ordinary dierential equations. Let X be a set of continuous variables. As for clocks, a variable valuation is a function ν : X → R. We write R X for the set of valuations over X. Valuations over X evolve according to delay functions F :

R ≥0 × R X → R X ,
where for a delay d and a valuation ν, F (d, ν) is a the new valuation. Delay functions are assumed to be time additive (

F (d 1 , F (d 2 , ν)) = F (d 1 + d 2 , ν). Denition 2.10. A hybrid automaton (HA) is a tuple H = (Loc, I, C, Act, E, F, Inv).
Loc is a nite set of locations;

I ∈ L is a set of initial locations;
C is a nite set of continuous variables.

Act = Act i Act o { } is a nite set of actions partitioned into inputs (Act i ), outputs (Act o ) or internal (labelled with ).

E is a nite set of edges of the form (l, g, a, φ, l ), where l and l are locations (resp. the source and the destination), g is a predicate on R X (called the guard), a ∈ Act is an action label, φ is a binary relation on R X that denes the clock updates.

For each location l, F (l) is a delay function;

Inv(l) is an invariant predicate.
The semantics of H are a transition system, whose states are pairs (l, ν) ∈ L × R X with ν |= I(l), and whose transitions are either, delay transitions (l, ν)

d -→(l, ν ) with d ∈ R ≥0 and ν = F (l)(d, ν), or, discrete transitions (l, ν) a -→(l , ν ) if there is an edge (l, g, a, φ, l ) ∈ E, such that ν |= g and φ(ν, ν
). An execution of H is an alternating sequence of delay and discrete transitions. As timed automata, HA can be combined in networks of HA via parallel composition.

The above denition deliberately left open the syntax for the delay functions F , the guards g, the update predicates φ and the invariants I. Their concrete denition depends on the class of hybrid automata that is considered.

Timed automata (TA) [START_REF] Alur | A theory of timed automata[END_REF] is the most restrictive class of HA we use as presented in Section. 2.3. This means that for any clock x ∈ X, the delay functions F (l) denes an implicit rate x = 1.

Stopwatch automata (SWA) [START_REF] Cassez | The impressive power of stopwatches[END_REF] extend TA by allowing to stop and resume clocks. The rates of the variables are therefore either x = 1 (for running clocks) or x = 0 (for stopped clocks).

Priced timed automata (PTA) [BFH + 01, ALTP04] allow the continuous variables to be either clocks as in TA, or cost-variables with a rate x = e, where e is an expression that only depends on the discrete part of the current state. These cost-variables cannot be used in guards, updates and invariants of the PTA, which implies that they cannot aect the behavior of the model.

Hybrid automata (HA) is the most general case. It allows to use ordinary dierential equations to dene delay functions F and invariants I.

Modeling Hybrid Automata in Uppaal

Uppaal is one the most famous tools for modeling and analyzing timed automata and their hybrid extensions. The tool has been developed for more than 20 years by a collaboration between Uppsala University in Sweden and Aalborg University in Denmark.

It allows to design models that belong to one of the four classes of hybrid automata presented previously. It additionally provides many syntactic constructions that help the design of complex models. In the following of the thesis we will heavily use these constructions for designing models of scheduling systems. We will succinctly explain the syntax and semantics of our models, but we cannot present here the full syntax of Uppaal models, and therefore we redirect the reader to the documentation of the tool (at http://www.uppaal.org/) for a more precise description. Some of the main capabilities oered by the tool are:

Data variables. In addition to clocks, the tool allows to use data variables (integer, oat, arrays, and structures). They can be updated during transitions, and tested in guards or invariants. Synchronization channels can also be dened in arrays.

Functions. The tool allows to write functions using a syntax similar to the C language. They can be used in guards, invariants, and updates of variables. When synchronizing transitions on a channel, the update functions of all the transitions involved in the synchronization are performed.

Templates automata. Hybrid automata can be dened as templates with input parameters. This allows to instantiate several automata in a model using the same template (for instance several tasks with dierent parameters).

In this thesis we will show several examples of hybrid automata by using screen captures from automata designed in Uppaal. In these gures the transitions have guards in green, synchronization actions in light blue (τ actions are omitted), updates in blue. Locations have a name and an invariant (possibly with clock rates) in purple.

Example We present in The model in Figure 2.3a implements a task with no preemption using a timed automata. It has a clock x to measure the length of the period and a clock y to measure the execution time. It starts its execution when receiving the event schedule?. It sends an event done! as soon as the clock y has reached the best case execution time (bcet) and before reaching the worst case execution time (wcet). Otherwise it goes to the location MissingDeadline with an internal transition when the clock exceeds the deadline. Finally it returns to location JobDone to wait for the next execution round and it sends the signal ready! to the scheduler.

The model in Figure 2.3b implements a preemptive task using a stopwatch automaton.

It renes the previous model with a stopwatch on clock y: the clock is stopped in location Ready (denoted y'=0), otherwise it is assumed that its execution rate is 1. The task can be preempted by the scheduler when it receives the signal not_schedule?, in which case it returns to location Ready.

The model in Figure 2.3c additionally computes the energy consumed by the running task using a priced timed automaton with a variable e to measure the energy. The energy can only increase in location Executing at a rate given by the constant POWER.

Finally, the model in Figure 2.3d is additionally aware of the frequency FREQ at which the processor is running. This frequency denes the rate at which the task executes by setting y'==FREQ in the invariant of location Executing.

Stochastic Hybrid Automata

Hybrid automata (and their sub-classes) may be used with a stochastic semantics [DLL + 11,

DDL

+ 12] that renes all non-deterministic choices with probability distributions. This impacts the choice of delay, output and next state. For each state s = (l, ν) of an HA H we assume there exists the following probability distributions:

the delay density function µ s over delays in R ≥0 , that denes when the component will perform an output, the output probability function λ s , that assigns probabilities to each available out-

puts o ∈ Σ o , the next-state density function η a
s , that provides stochastic information on the next state s = (l , ν ) ∈ R X given an action a.

Adding stochastic information Stochastic hybrid automata are analyzed with Uppaal SMC. Without additional information the tool is also able to run classical TA, SWA, PTA or HA with a stochastic semantics, that apply uniform distributions to delays in states with bounded delay, to outputs and to next states. Additionally the user can provide the rate of an exponential distribution for each location with unbounded delay, and discrete probability distributions between dierent outputs and the next states.

These distributions can be sampled from executions or simulations of the system, or set as requirements from the specications. For instance in avionics, display components have a lower criticality. They can include sporadic tasks generated by user requests. In that case, average user demand will be eciently modeled with a probability distribution.

Similarly, timing executions may vary due to the content being displayed and can be measured from the system.

If analyzed with Uppaal model-checker, stochastic information from a stochastic hybrid automaton is discarded to consider only the underlying non-deterministic model.

Example Stochastic hybrid automata with discrete probability distributions are useful to initialize the parameters of a model with random values, e.g., to specify that the period or the deadline of a task depends on some random information. They can be designed For instance, the simple automaton in Model-based approaches also enable to use stochastic tasks whose real-time attributes, such as deadline, execution time or period, are characterized by probability distributions. This is particularly useful to describe mixed-critical systems and to make assumptions on the hardware domains. These systems combine hard real-time periodic tasks, with soft real-time sporadic tasks. Analytical scheduling techniques can only reason about worst-case analysis of these systems, and therefore always return pessimistic results.

Using stochastic verication techniques like SMC we can instead analyze the system in an average scenario and provide more accurate measures.

Analytical Methods for Analysis of Sporadic Tasks Sporadic tasks were rst introduced in [BMR90, Mok83] as an extension of the Liu and Layland [START_REF] Liu | Scheduling algorithms for multiprogramming in a hard-real-time environment[END_REF] task model.

The authors in [START_REF] Sanjoy | Preemptively scheduling hard-real-time sporadic tasks on one processor[END_REF] proposed an exact schedulability analysis by providing some necessary and sucient conditions for a sporadic task system.

In

Model-based Analysis of Stochastic Sporadic Tasks

In the context of modelbased analysis, the authors in [CBF + 11] present a symmetric multi-core framework where a at scheduling system can be described in the Prelude language. The schedulability can be checked using generated Uppaal models.

The authors in [START_REF] Manolache | Analysis of monoprocessor systems[END_REF] formally characterize stochastic tasks for various platforms and presents a model-based analysis technique to check the schedulability of the tasks.

The main idea is to compute the probability distribution of a task termination time by a convolution of the probability density functions of the task starting time and execution time. However, it is restricted to non-preemptive stochastic tasks, and the analysis complexity is also exponential.

Using the statistical model checking technique in Uppaal, the work in [BDK + 14] proposes a way of estimating the "degree of schedulability" of sporadic tasks and also presents the Uppaal models used to implement the concepts as well as an avionics case- but with dynamic stochastic updates of real-time attributes. In this thesis, we reuse these models and extend them to dene stochastic tasks.

Formal Models of Scheduling Components

The formal models of our scheduling systems are inspired by [BDK + 13, BDK + 15a].

Stochastic Scheduling Systems

In [CKL + 16] we have extended these models to use stochastic tasks whose real-time attributes (period, delay, execution time) depend on probability distributions, and are dynamically chosen by a stochastic dispatcher. This stochastic feature is of interest to model the variation of execution time with respect to the computation logic and the capability of the execution environments (CPU, memory, I/O and caches, etc). Such real values can be obtained by sampling the execution times from the real world system.

Observe that other tasks parameters such as the deadline and the period are determined according to the timing requirements of the functionality implemented by a set of tasks.

For instance, some video decoder and encoder would update the deadline and period of tasks according to the frequency of input streams. For those reasons, they can also be represented by probability distributions.

In a stochastic task the stochastic attributes are determined by a stochastic dispatcher at each new instantiation of a job (when calling the functions setTaskAttribute and setJo-bAtt). The stochastic dispatcher is implemented with a stochastic timed automata using discrete probabilistic choices. Figure . 2.7 presents an example of a dispatcher that congures the three attributes with probabilistic choices between ve values.

Chapter 3

Model Checking, Statistical Model

Checking and High Level Language

In this chapter, we present model checking MC and statistical model checking SMC as formal methods that we used in our work to analyze real-time systems. We rst introduce the formal language used for the properties specication. Then we present the principals of MC and SMC. Finally we present high level languages that allow to embed these formal specications into a user friendly graphical interface.

Introduction

The formal models dened in the previous chapter can be used to perform automatic verications. For that, They must be accompanied by a specication of the properties of interest that need to be veried. This chapter introduces some important, though relatively simple, classes of properties. These properties are based on temporal logic to express requests about sequences of events. We present the syntax and semantics of this logic. Next, we present formal methods model checking (MC) and statistical model checking (SMC) to verify properties on a given model. Finally, we present a high level language called Cinco used to produce a graphical representation of the model and the properties under consideration.

Temporal logics

To express the timing constraints an appropriate formalism must be used. Here the timing constraints are dened as a sequence of events and not as a quantitative values.

Temporal logic is a formalism used to express the timing aspects of the property that needs to be veried with a mathematically precise notation. Temporal logic considers time in one of the two following manners. The rst one is in linear way, which means that at each state of execution the system has a unique possible future state. The second manner is to consider time in a branching way, which means that at each state of the execution of the model the system can have more than one possible future. The second one considers the structure of time as a tree.

Linear Temporal Logic

Linear Temporal Logic (LTL) reasons in linear way about time. At each moment in time LTL considers that there is only one possible future of the system. Formulas of LTL are constructed from the set of atomic proposition AP of the transition system using the usual boolean connectors (¬, ∧) and the temporal operators ( , ), where designs the temporal operator Next and designs the temporal operator Until.

Syntax

The LTL formulas over set of atomic proposition are constructed according the the following grammar:

ϕ = true | a | ϕ 1 ∧ ϕ 2 | ¬ϕ | ϕ | ϕ 1 ϕ 2
where a ∈ AP .

The operator is a unary prex operator.

ϕ holds if it holds in the next step.

The operator is a binary one. Formula ϕ 1 ϕ 2 holds at the current state l i if there is some state l j in the future for which the formula ϕ 2 holds and the formula ϕ 1 holds at all the states until l j .

The precedence order of the operators is given as follow. the unary operators are stronger than the binary ones. ¬ and are equal strong, the temporal operator takes precedence over ∧, ∨, and →. Operator is right associative, ϕ 1 ϕ 2 ϕ 3 means ϕ 1 (ϕ 2 ϕ 3 ).

From the negation and the conjunction we can dene the usual boolean connectors as disjunction and implication as follow:

ϕ 1 ∨ ϕ 2 = ¬(¬ϕ 1 ∧ ¬ϕ 2 ) (disjunction) ϕ 1 → ϕ 2 = ¬ϕ 1 ∨ ϕ 2 (implication).
Using the until operator, we can express the temporal modalities ♦ (eventually in the future) and (now and forever in the future) as following:

♦ϕ = true ϕ ϕ = ¬♦¬ϕ
Intuitively, ♦ϕ means that eventually in the future the property ϕ will be true. ϕ holds if and only if ¬ϕ do not holds eventually in the future. New temporal modalities can be obtained by combining the two temporal modalities ♦ and . For example, ♦a (always eventually a) means that at any moment i there is a moment j, j i at which the proposition a is true, it means that the proposition a will be true innitely often. Another example is ♦ a (eventually forever) which means that after some moment j only the proposition a will be true. Example Let consider two processes P 1 , P 2 . For each process we can dene three states.

A non critical section state non_crit i , a wait state wait i , when the process is ready to enter its critical section, and the critical section crit i . The LTL formula to express the requirement that the two processes can not enter their critical section simultaneously is:

(¬crit 1 ∨ ¬crit 2 )
This formula expresses that always ( ) at least one of the two processes is not in its critical section.

Semantics

LTL formula expresses properties on paths (or in fact their trace). This means that a path can either satisfy an LTL formula or not. To precisely formulate when a path satises an LTL formula, we proceed as follows. First, the semantics of LTL formula ϕ is dened as a language W ords(ϕ) that contains all innite words over the alphabet 2 AP that satisfy ϕ.

Denition 3.1 (Semantics of LTL). Let consider an LTL formula ϕ over atomic propositions AP . The language accepted by ϕ is:

W ords(ϕ) = {σ ∈ (2 AP ) w |σ ϕ} with σ = A 0 A 1 A 2 ... ∈ (2 AP ) w , σ[j...] = A j A j+1 A j+2 .
.. is the sux of σ starting in the (j +1)st symbol A j , and the satisfaction relation ⊆ (2 AP ) w ×LTL is the smallest relation with the properties:

σ true σ a i a ∈ A 0 (i.e. A 0 a) σ ϕ 1 ∧ ϕ 2 i σ ϕ 1 and σ ϕ 2 σ ¬ϕ i σ ϕ σ ϕ i σ[1...] = A 1 A 2 A 3 ... ϕ σ ϕ 1 ϕ 2 i ∃j 0, σ[j...] ϕ 2 , for all 0 i < j, σ[i...] ϕ 1
For the derived operators ♦ and the satisfaction relation will be:

σ ♦ϕ i ∃j 0, σ[j...] ϕ σ ϕ i ∀j 0, σ[j...

] ϕ

As a subsequent step, we determine the semantics of LTL formula with respect to a transition system. The LTL formula ϕ holds in location l if all paths starting in l satisfy ϕ. The transition system T S satises ϕ if T S satises W ords(ϕ), i.e., if all initial paths of P aths(T S) starting in an initial state l 0 ∈ I satises ϕ. Denition 3.2 (Semantics of LTL over Paths and States). Let consider ϕ as an LTL formula over atomic propositions AP , and let T S = (Loc, Act, E, I, AP, L) be a transition system without any terminal location.

For innite path fragment π of T S, the satisfaction relation is dened by:

π ϕ i T race(π) ϕ
For location l ∈ Loc, the satisfaction relation is dened by: l ϕ i ∀π ∈ P aths(l), π ϕ T S satises ϕ, denoted by T S ϕ, if T races(T S) ⊆ W ords(ϕ)

Computation Tree Logic

In a transition system a location can have more than one direct successor, it means that we can have dierent paths starting from the same location. The satisfaction of an LTL formula ϕ in a state requires that the LTL formula holds in the location l if all possible computations starting in l satises ϕ.

In LTL, it is not simple to verify the existence of some paths starting at location l that satises the property ϕ. For example, to verify if there exists some paths starting at location l and that satises property ϕ, we can exploit the duality between universal and existential qualications. We may check whether l ¬ϕ; if this formula is not satised, then there must be some computations satisfying ϕ.

For more complicated properties, like "for every computation it is always possible to return to the initial location", this is, however, not possible. A naive attempt would be to require ( ♦l 0 ) to hold for every computation, where the location l 0 uniquely identies the initial state. This is, however, too strong as it requires a computation to always return to the initial state, not just possibly. Other attempts to specify the intended property also fail, and it turns out that the property cannot be specied in LTL.

To overcome these problems, another kind of temporal logic can be used. Contrary to LTL, Computation Tree Logic (CTL) reasons about time in a branching manner, i.e at each state there can be several dierent futures. Due to this branching notion of time, this class of temporal logic is known as a branching temporal logic. The semantics of a branching temporal logic is dened in terms of an innite, directed tree of states rather than an innite sequence. Each traversal of the tree starting in its root represents a single path. The tree itself thus represents all possible paths, and is directly obtained from a transition system by "unfolding" at the state of interest.

The temporal operators in a branching temporal logic allow the expression of properties some or all paths that starts at location l. To that end, it supports an existential path quantier (denoted ∃) and a universal path quantier (denoted ∀). For instance, the property ∃♦ϕ denotes that there exists a path along which ♦ϕ holds. It means that there is at least one possible path in which a state that satises ϕ is eventually reached.

The property ∀♦ϕ, in contrast, means that all paths satisfy the property ♦ϕ.

Syntax

CTL distinguishes between state formula and path formula. State formula expresses a property of a state, while path formula expresses a property of a path, i.e. an innite succession of states. The temporal operators and have the same meaning as in LTL.

The CTL formula over a set of atomic proposition is dened as follow:

ϕ ::= true | a | ϕ 1 ∧ ϕ 2 | ¬ϕ | ∃Φ | ∀Φ
where a ∈ AP and Φ is a path formula. CTL path formulae are formed according to the following grammar:

Φ ::= ϕ | ϕ 1 ϕ 2
where ϕ, ϕ 1 , and ϕ 2 are state formulae.

Path formula can be turned into state formula by adding path quantier ∃ (pronounced it exists some paths) or the quantier ∀ (pronounced for all paths). Temporal modalities "eventually", and "always" can be derived as follow:

eventually: ∃♦ϕ = ∃(true ϕ) ∀♦ϕ = ∀(true ϕ) always: ∃ ϕ = ¬∀♦¬ϕ ∀ ϕ = ¬∃♦¬ϕ
Example Let consider the precedent example presented in section 3.2.1, the mutual exclusion property can be written in CTL as follow:

∀ (¬crit 1 ∨ ¬crit 2 )
It means that for all paths we have always one process at least out of its critical section. express the properties "there exists paths where gray holds until black holds" and "for all paths gray holds until black holds", respectively.

Semantics

CTL formulae are interpreted over the states and paths of transition system. Formally, given a transition system, the CTL formulae are dened by two satisfaction relations:

one for the state formula and one for the path formula. For the state formula, is a relation between the states in the transition system and the state formula Φ, we write s Φ, to mean that state s satises the state formula Φ. For the path formula, is a relation between maximal path fragment π and path formula ϕ, we write π ϕ, to mean that π satises the path formula ϕ.

Denition 3.3 (Satisfaction relation for CTL).

Let T S = (Loc, Act, E, AP, L) be a transition system without terminal state, a ∈ AP an atomic proposition, Φ, Ψ a CTL state formula, ϕ a CTL path formula. We dene the satisfaction relation as follow:

l a i a ∈ L(l) l ¬Φ i not l Φ l Φ ∧ Ψ i (l Φ) and (l Ψ) l ∃ϕ
i π ϕ for some π ∈ P aths(l) l ∀ϕ i π ϕ for all π ∈ P aths(l)

For paths π, the satisfaction relation is dened as follow:

π Φ i π[1] Φ π Φ Ψ i ∃j 0, (π[j] Ψ ∧ (∀0 k < j, π[k] Φ))
where for path π = l 0 l 1 l 2 ... and for i 0, π[i] denotes the (i + 1)th location of π.

In CTL atomic propositions, negation, and conjunction are interpreted over states, whereas in LTL they are interpreted over paths. State formula ∃ϕ holds in l if and only if there exists some paths starting in l that satises ϕ. The state formula ∀ϕ holds in l if and only if all paths starting in l satises ϕ. The semantics of path formula is identical to that for LTL. For instance, ∃ Φ holds in location l if and only if there exists paths starting in location l where the next location satises Φ, this is equivalent to the existence of a direct successor l of the location l where l Φ. ∀(Φ Ψ) holds is location l if and only if for all paths starting in location l there exists an initial nite prex such that Ψ holds in the last location of this prex and Φ holds for all the locations along this prex.

Model Checking (MC)

Model checking is an automated verication technique that explores all the possible executions of a model in a brute-force manner to verify if it satises a property written in a formal logic. Model-checking can thus be used to assess the schedulability of a system, for any of its executions. This corresponds to the so-called worst-case analysis. When using model checking to analyze a given system, we can distinguish the following phases:

Modeling The modeling phase consists of:

Model the system under consideration using the model description language of the model checker.

Make some initial simulations to detect and x any simpler errors before using any form of checking.

Formalize the properties to be checked using appropriate temporal logic.

Running The running phase executes the model checker to verify the satisability of the properties under consideration.

Analysis The analysis phase interprets the results of the model checker:

If the property is satised then check the next property if it exists. If all properties are checked and are satised, then we conclude that the model satises all the desired properties; If the property is not satised then:

1. analyze the generated counterexample;

2. rene the model, the system design, or the property; 3. repeat the entire procedure.

If the model is too large to be handled (state space of real-life system is often too large to be stored in the available memory) then reduce the model and try again.

Typically, properties of qualitative nature can be checked using model checking. For example, "is the generated result OK?" or "can the system reach a deadlock situation?".

Additionally, timing properties can be checked, like "can the system reach a deadlock situation within one hour after a system reset?", or, "is the response always received after sending a question?". In that case, model checking requires a precise and unambiguous statement of the properties to be examined. CTL checking problems are decidable for TA. Even basic model checking problems (reachability) are undecidable for SWA and HA. For these models it is only possible to perform exhaustive analysis with an over-approximation of the reachable states. The alternative is to exploit the stochastic semantics of HA and to resort to simulations and statistical model-checking (SMC).

The model checker Uppaal uses a restricted version of temporal logic CTL to express the properties under consideration. It is dened as follow:

ϕ ::= A[]P | A<>P | E[]P | E<>P
The operator A represents the operator for all paths" ∀ dened above in section. 3.2.2. In the same way E represents the operator "there exists a path" ∃. [] and <> are state operators, meaning respectively `"all states of the path" and "there exists a state in the path", the corresponding state operators dened in section. 3.2.2 are respectively and ♦. P is an atomic proposition that is valid in some state. For example the formula "A[] not error" species that in all the paths and all the states on these paths we will never reach a state labeled as an error. For instance for schedulability analysis, an error state is one where a task has missed a deadline.

Strengths and Weaknesses

The main important qualities that constitute the strength of model checking are:

It is a general verication approach that can be applied on dierent ranges of systems.

The properties can be checked separately, i.e. each property can be checked individually.

It gives diagnostic information if the property is not validate, these information are very important for debugging purposes.

It can be easily integrated in existing development cycles.

The main important weaknesses of model checking are:

It veries a system model not the actual system itself. Any obtained result is thus as good as the system model.

It checks only stated requirements, i.e., there is no guarantee of completeness. The validity of properties that are not checked cannot be judged.

It suers from the state-space explosion problem, i.e., the number of states needed to model the system accurately may easily exceeds the amount of available computer memory.

Its usage requires some expertise in nding appropriate abstractions to obtain smaller system models and to state properties in the logical formalism used.

Despite the above limitations we conclude that model checking is an eective technique to expose potential design errors. Thus, model checking can provide a signicant increase in the level of condence of a system design.

Statistical Model Checking (SMC)

To overcome the above diculties we also propose to work with Statistical Model Checking SMC [KZH + 11, You05, You06, SVA04, SVA05a, SVA05b], an approach that has recently been developed as an alternative to avoid an exhaustive exploration of the state-space of the model. SMC allows to reason on the average scenario, and to quantify the results with a probability measure. The principle is to combine formal verication and techniques from the statistic area in order to compute the probability that a system achieves a given objective.

There exists several SMC algorithms, see [START_REF] Legay | Statistical model checking: An overview[END_REF] for details. In this thesis, we focus on the Monte-Carlo algorithm. This algorithm performs N executions ρ and then estimates the probability γ that the system satises a logical formula ϕ using the following equation:

γ = 1 N N i=1 1(ρ |= ϕ)
where 1 is an indicator function that returns 1 if ϕ is satised and 0 otherwise. The number of simulations N denes the precision of the results. It guarantees that the estimate γ is close enough to the true probability γ, such that if N = (ln 2 -ln δ)/(2ε 2 ) the probability of error is P r(| γ-γ |≥ ε) ≤ δ, where and δ dene the condence interval and the condence level, respectively.

Bounded Linear Temporal Logic (BLTL) is a restricted version of LTL that expresses bounds on step or time units in order to reduce the paths or time on which the desired property will be veried. These bounds give the length of the run on which the property under consideration will be veried. Any decidable property on states or paths can be used in the formulae including BLTL operators. Thus, the semantics of BLTL logic is the semantics of LTL logic restricted to a time interval. The BLTL temporal operators are dened as follow:

"eventually within time t" : ♦ t ϕ = true t ϕ where t ∈ R + "always up to time t" : t ϕ = ¬♦ t ¬ϕ where t ∈ R +

The statistical model checker Uppaal SMC uses BLTL formulas to ask for the probability that a given property holds within a xed bound of time.

Uppaal SMC queries express properties over a single trace using BLTL. These queries associate an LTL formula and probability operator Pr and a time bound. The following query for instance "Pr[<=maxTime]( <> error)" asks to compute the probability of reaching an error state before maxTime. Additionally, Uppaal SMC allows writing simulate queries that only examine traces without computing a probability.

High Level Language: Cinco

Currently, many models and tools are successfully used to analyze properties of CPS. But they are domain-specic, which means they cannot easily be applied to other systems.

Moreover, these models and tools require high technical knowledge about the theoretical formalisms used to design models and write properties, which most system engineers do not master. In this section we demonstrate a exible and formal analysis engineering approach for analyzing scheduling properties of CPS.

We encapsulate the formal models for scheduling systems presented in Chapter 2.5.1 into Cinco [NLKS17, NTI + 14] a generator for domain-specic modeling tool, these mod- els constitute a model bank that will be used to represent the dierent systems under consideration. This bank will be enriched in the next chapters.

Cinco allows to specify the features of a graphical interface in a compact metamodel language, and it generates automatically from this meta-model specication a domain-specic analysis tool with a graphical interface. Inside this analysis tool we can specify scheduling systems and the properties they must satisfy. Cinco allows also to add implementations in order to achieve additive works, in our work we implement number of algorithms that are designed to:

Transform the graphical representation of the components and the properties specications of the system under consideration to timed automata; Allow to launch analyses in the graphical interface;

Call Uppaal [BDL + 06] and Uppaal SMC [DLL + 15] to perform the analysis;

Parse the results and displays them by modifying the graphical elements.

These transformations from the graphical representation to the formal models consist in translating the graphical components and the properties specications of the system under consideration using the appropriate timed automata from the model bank. Consequently it constructs a full formal model that can be analyzed by Uppaal in order to verify the satisability of the properties studied. This approach allows to completely hide the formal models being used from the system designer, who can concentrate on the structure and the parameters of the scheduling system.

The last challenge is to give signicant feedbacks to the user in the most friendly manner. Indeed, results of formal verication from academic tools like Uppaal can be dicult to interpret, all the more when the models used by these tools have been automatically generated. Cinco provides an API for model transformations that allows to program actions that can update the model. We have used this functionality to parse the results of the analyses output by Uppaal and to show graphically the most relevant information.

Domain-Specic Code Generator: CINCO

Cinco is a generative framework for the development of domain-specic graphical modeling tools. It is based on the Eclipse Modeling Project [START_REF] Gronback | Eclipse Modeling Project: A Domain-Specic Language (DSL) Toolkit[END_REF], but with a strong emphasis on simplicity [START_REF] Margaria | Simplicity as a Driver for Agile Innovation[END_REF], so that the user (i.e. the developer of a tool generated with Cinco)

does not need to struggle with the underlying powerful but complicated EMF metamodeling technologies [START_REF] Steinberg | EMF: Eclipse Modeling Framework (2nd Edition)[END_REF] directly. This is achieved by focusing on graph model structures (i.e. models consisting of various types of nodes and edges) and automatically generating the required Ecore metamodel as well as the complete corresponding graphical editor from an abstract specication in terms of structural constraints. In a sense, this approach turns constraint-based variability management [JLM + 12, LNS13] into a tool generation discipline, where a product line is just characterized by the tools' modeling capacities.

Meta-Modeling

Central to every Cinco product is the denition of a le in the Meta Graph Language or transforms the models. It automatically generates APIs specic to the model type and seamlessly integrates code implemented against it into a ready-to-run modeling tool, which is a realization of the one-thing-approach [START_REF] Margaria | Business Process Modelling in the jABC: The One-Thing-Approach[END_REF].

The main principles for the generation of a domain-specic tool with Cinco are depicted in Figure 3.5. From the MGL and Style denitions, Cinco generates an Ecore metamodel as well as a corresponding graphical editor for the domain-specic tool. The user can then create a model in the tool that conforms to the given specication. This model can be analyzed by custom Java code, embedded in the tool during the automatic generation by Cinco.

Domain Specic Tool

Besides the tool meta-modeling, the second important feature of Cinco needed to develop a domain specic tool is the possibility to enhance the graphical editor by adding custom code. This code can call an API generated by Cinco to interact with the meta-model.

Please refer to [NLKS17, NTI + 14] or the website 1 for more detailed introductions.

The easiest way to enhance the graphical editor is by adding a custom action to a node type, which is then available via the nodes' context menu or on double-click. For a custom action two methods need to be implemented: canExecute and execute. Both receive the node on which the action should be performed as a parameter. While the rst decides whether the action is available (i.e. not disabled/greyed out in the context menu), the second one actually performs it. The generated enhanced API for the metamodel simplies the implementation of those methods, as one can easily access related modeling elements in a semantic and type-safe way, e.g. by accessing all successors (i.e. target nodes of outgoing edges) of a certain type.

Furthermore, Cinco makes it especially easy to perform changes to the edited model. Usually, with the common Eclipse approaches, the visual representation as well as the underlying model structure need to be changed separately. The transformation API that Cinco generates for every model type handles the synchronous and consistent modication of both parts automatically, so that it becomes very straightforward to program transformations for the model, as the generated API provides the same actions the tool user can perform within the editor, e.g. change attributes, add new elements, connect them with edges, or move/resize/delete them.

Implementation of the Framework and Tool Chain

We have implemented the domain-specic analysis framework. The tool chain involved in the generation of these frameworks and then in their usage is described in Figure 3.6.

The framework is developed in Java and with Cinco. The graphical interface of the framework is specied with the meta-modeling languages of Cinco, presented in Section 3.5.1.1. Then we have developed Java programs for generating complete formal models from the high-level specications. These generators use existing formal models from a model bank (the models presented in Section 2.5.1). Finally we have developed Java custom analysis programs. These programs are linked to the code generated by Cinco such that they can be started directly from the graphical interface, either by a right-click menu or double-click actions. These programs solve the problems listed in Since the complexity of the entire HSS is too large to be analyzed with formal methods, we rely on compositional approaches that allow to analyze each local scheduler independently [START_REF] Shin | Periodic resource model for compositional realtime guarantees[END_REF].

Tool Generation

In our formal framework, a HSS is a set of scheduling units organized in a tree structure. Each scheduling unit is composed of a set of real-time tasks, a scheduler, that implements a scheduling algorithm, and a queue, that manages jobs instantiated by tasks. To perform a compositional analysis of the system, we provide each scheduling unit with a resource supplier that abstracts the behavior of the parent scheduling unit.

The models for tasks and schedulers are dened in Chapter 2.5.1.

Resource Supplier The resource supplier is responsible for supplying a scheduling unit with the resource allocated from a parent scheduling unit. We adopt the periodic resource model (PRM) [START_REF] Shin | Periodic resource model for compositional realtime guarantees[END_REF]. It supplies the resource for a duration of Θ time units every period Π. To speed up the schedulability analysis using model checking techniques, it only generates the extreme cases of resource assignment: either the resource is provided at the beginning of the period (from 0 to Θ) or at the very end (from Π -Θ to Π). The These interfaces use the PRM, each with a period of 100, and a budget of 35 for I 1 and 25 for I 2 . The lower schedulers schedule three real-time tasks each using the resource they receive from the interfaces I 1 and I 2 .

Scheduling Problems

In this section we present the dierent problems that we want to solve in scheduling systems.

Problem 1: Correctness and performance We want to evaluate several properties of the scheduling system to assess its correctness and measure its performances:

1. Absence of deadlock: We check that the formal models have been correctly designed, because they cannot reach a deadlock state in which time is blocked and no action is available.

2. Schedulability: We determine whether the tasks are schedulable, i.e, none of them misses a deadline. In case of HSS, we check that all the scheduling units are schedulable.

3. Maximum response time: We measure the maximum response time of tasks, i.e., the maximum time between a job instantiation and its completion.

Problem 2: Optimal conguration of the system Depending on their nature, our scheduling systems may admit dierent congurations. Then, we may evaluate each conguration according to one or several measures presented in Problem 1 in order to select an optimal conguration.

In a HSS, each scheduling unit is analyzed independently using the budget provided by the PRM. To congure the system we determine which budget values make the system schedulable. Our goal is to nd minimum budgets, such that all the scheduling units are schedulable.

Formal Model-based Compositional Framework for HSSs

Our model-based compositional analysis tool implements a model-based analysis framework of HSSs that is exible enough to represent any scheduling systems. If a process of the TA stochastic task at the Init location is instantiated, it reads the default attributes by function setTaskAttribute() and initializes a job. Then, the job requests the scheduler to assign a CPU by synchronizing the channel req_sched(pid) and queues at a resource (ready) queue by inserting its id (tid) to the queue.

A job process may stay at location Executing as long as job's execution time is not fullled and it does not miss the deadline. The process stops and resumes its execution on that location according to the availability of CPU resource, i.e. the job process can make progress when a CPU is available, otherwise, it must stop its execution.

In our model, there is no preemption location to denote that a task is waiting for CPU after it has been preempted but preemption is implemented by a stopwatch clock t_et[tid]. This clock measures the CPU-consuming time of a task since a job of the task has been instantiated; the clock can stop and resume when a CPU is available to the task.

At location Executing, the invariant expression t_et[tid]'=isSchedSuped(tstat [tid].pid),tid) is associated to the stopwatch clock. This condition is such that the clock progresses if the function isSchedSuped() returns 1, otherwise, it does not progress.

The process of a task exits from location Executing when it has fullled its execution time and it releases the CPU resource using function deque_tid(tstat[tid].pid, tid). Then, it joins the location WaitEndofMINIntv and waits the end of the minimal inter-arrival time. Finally, the process of a task joins the location JobWait to be instantiated by a job dispatcher.

Stochastic Dispatcher

These stochastic tasks are combined with a stochastic dispatcher that congures the real-time attributes of the tasks at each individual execution round. In other words, the stochastic dispatcher determines the conguration of tasks real-time attributes at the beginning of each execution round when the task is waiting at the location JobWait. On the initial location Stable, two recursive transitions trigger the events start_job [START_REF]2 Preemptive Scheduling algorithm[END_REF] and start_job [2] to instantiate the corresponding jobs if the conditions tstat [START_REF]2 Preemptive Scheduling algorithm[END_REF].status=WAITING and tstat [2].status=WAITING hold. Even if the transitions are enabled, they are actually taken by the exponential distribution with rate λ = 1/100. If the condition numof Jobs > h holds, the transition heading for location Unstable can be taken. Then, a new conguration on the real-time attributes of T 1 , T 2 and T 3 are made and, in particular, the real-time attributes of T 1 and T 2 are taken from the associated probability distributions, such as ρ e 1,2 , ρ p 1,2 , ρ d 1,2 , etc.

Formal Analysis Model of Scheduling Unit

The approach we pursue is compositional: each scheduling unit is individually analyzed with respect to an interface that abstracts the behavior of the other components. For the analysis of HSSs, the interface we are using is the PRM [START_REF] Shin | Hierarchical scheduling framework for virtual clustering of multiprocessors[END_REF] that assigns the amount Θ of resources every period Π. Once a job is instantiated by a task, it asks the scheduler for CPU computation time by ring the event req(tid,pid), which inserts the task's Id into the ready queue pq. Then, the scheduler sorts task's identities according to a scheduling policy and chooses the id of the task having the highest priority. This task can carry out its jobs until it nishes the jobs or it is preempted.

The model of the scheduling unit is extended with a resource model Γ P RM (Π, Θ) in .9 shows a simulation of the PRM behavior that provides a resource for 33 time units every 100 time units. The spike in blue denotes a period of the supply and the graph in red denotes a resource supply. Note that the resource supply begins and terminates in synchronization with the beginning and end of a period, which implies that the longest starvation of the supplying resources can occur extremely often.

Resource Model

Resolution of the Problems

In this section we detail the techniques we use to solve the scheduling problems presented in Section 4.2.

Checking Correctness and Evaluating Performances with MC and SMC

The properties associated to Problem 1 are translated into formal queries in the format of the tool Uppaal MC and Uppaal SMC.

Absence of deadlock We use the CTL formula A[] not deadlock that is checked with model-checking by the tool Uppaal.

Schedulability In our formal models we check schedulability by searching for error states in tasks, that correspond to the tasks missing their deadline. All these error states are identied by a single Boolean variable error, set to true when a task misses a deadlines.

Then, schedulability is analyzed by Uppaal SMC using the following probabilistic query:

simulate nbSim [<=runTime] {error} : 1 : {error} It asks to perform nbSim simulations of length runTime t.u., until one reaches a state labelled with error. If such a state is found, then the system is not schedulable.

Uppaal SMC performs a quick evaluation of the schedulability. If the system is not schedulable it may nd quickly a counterexample execution. However, for an exhaustive result, we rely on model-checking with Uppaal using the CTL formula A[] not error. If the system contains stopwatches the analysis is performed with an over-approximation:

if the result is true then the system is surely schedulable; if the result is false it may not be schedulable.

Maximum response time We measure this property using Uppaal SMC with the following query: E[<= runTime;nbSim](max:t_resp [2])

It runs nbSim simulations of runTime t.u. and it computes the average value over these simulations of the maximum response time of the task with ID 2 (the response time of task 2 is measured in the model with a variable t_resp [2]).

Optimization of a Hierarchical Scheduling System

To optimize a HSS we must determine the minimum budgets for the resource suppliers such that all the scheduling units are schedulable. For this purpose we use the stochastic model of the resource supplier presented in Figure 4.1 that species a range of possible budgets Θ. Then we use Uppaal SMC to randomly select a value within this range and check whether the scheduling unit is schedulable with this value.

We use the following probabilistic BLTL formula:

Pr[estBudget [START_REF]2 Preemptive Scheduling algorithm[END_REF]<=runTime](<>globalTime>=runTime and error)

It computes the probability distribution of all the possible budget values that are not schedulable. With Uppaal SMC we can plot the probability density distribution in a graph, as shown in Figure 4.10. By looking at the support of this distribution we can determine the minimum budget whose probability is zero, that is the minimum budget necessary to schedule all the tasks of the scheduling unit.

Example We consider the HSS example presented in Figure 4.2. We analyze scheduling unit C 1 to compute the possible budgets for the resource supplier of this scheduling unit (such that the unit is schedulable). In Figure 4.2, this budget was arbitrarily set at 35 over a period of 100. We would determine if this value is sucient and if it can be lowered.

We set the range of budgets between 0 and 100. Using Uppaal SMC we analyze the probabilistic BLTL formula presented above and we compute the probability density distribution shown in Figure 4.10. It tells us that all the budgets lower than 34 have a non zero probability of being not schedulable. Therefore the minimum budget needed for the scheduling unit is 35 over a period of 100.

High Level Framework

This section presents how to use the high-level domain-specic language presented in Section 3.5 in order to design our high-level framework dedicated to the design and analysis of hierarchical scheduling systems. example of an HSS designed in our framework. The nodes of the tree correspond to the components of the scheduling units (tasks, suppliers). In the rest of the section we detail the available components of our high-level language and their conguration parameters.

High-Level Framework for Hierarchical Scheduling Systems

Resource suppliers TopSupplier(policy), in blue, is the root of the HSS tree. It supplies the resource to all the scheduling units. Its only parameter is the scheduling policy. Queries Queries are associated to the suppliers. The following queries, that correspond to the formal properties presented in Section 4.4.1, are available: deadlock query, schedulability, maximum response time, and budget estimation. In Figure 4.11 for instance, PSupplier2 is assigned a budget estimation query and Supplier1 a schedulability query.

Queries that have been veried are colored automatically by the tool, in green if they are satised, or in red if they are not satised.

We detail below the basic steps performed by our analysis programs to solve the dierent scheduling problems. The absence of the deadlock is shown in a pop-up window. The color of the query is turned to green or red according to the result.

Correctness and performance

The schedulability analysis produces a pop-up window with the result. The color of the query is turned to green or red. Additionally, if the result is false the color of the task that has missed a deadline is turned to red.

The measures of maximum response times is displayed in pop-up windows and in the queries.

Optimisation of Hierarchical Scheduling Systems

Experiments

We apply our framework for HSS to model and verify an avionic scheduling system. We consider the specication of avionic tasks presented in [START_REF] Locke | Generic avionics software specication[END_REF]. This is a mixed-critical system with multiple tasks of various criticality running together. We arrange these tasks in a hierarchical scheduling system by grouping tasks from similar functions and criticality (Navigation, Targeting, Weapon control and Controls and displays). Each function is associated to a scheduling unit. The three scheduling units of the most critical functions (Navigation, Targeting and Weapon control) are further grouped under a Hard-Subsystem scheduling unit. These results in the hierarchical scheduling systems are presented in Figure 4.12.

The goal of our study is to determine if the complete system is schedulable and to nd appropriate parameters for each scheduling unit, such that they are all schedulable.

High-level model We design the HSS in our domain-specic tool generated by Cinco, using the high-level language presented in Section 4.5.1. Sporadic tasks are modelled with stochastic task nodes and are associated to probability distributions. To estimate their necessary budget, each scheduling unit is modelled using a probabilistic supplier.

Verication procedure We analyze each scheduling unit, starting from the bottom, with the budget estimation query. We congure the scheduling unit, by selecting several values for the period of the probabilistic supplier. The period must be lower than the minimum period of the tasks being supplied. Then, we congure the minimum and the maximum budget for the estimation between [1, period]. We can now replace these probabilistic Suppliers with normal suppliers and conrm the schedulability of the units using the schedulability query, that is checked either with MC or SMC.

We then determine the period and the budget for the Hard-Subsystem unit. Its period must be lower than 4, the chosen period of the Weapon control unit. Since the combined load factor of the 3 lower scheduling units is 0.92, only a budget of 4 over 4 can schedule the Hard Subsystem unit, which we verify with the schedulability query.

We also determine the necessary budget for the Controls and display scheduling units.

We found the best budget to be 1 over a period of 3.

From our results we conclude that the two upper scheduling units (Hard Subsystem and Controls and Display) are each schedulable. However since the load factor of the Hard Subsystem is already 1, it cannot be scheduled with the second unit using the same resources.

Introduction

Many Cyber Physical Systems (CPS) are mission critical systems. It means that these systems must complete their missions within a period of time. In some cases the system must also complete its mission with limited resources: in particular a limited amount of energy. Number of researches focused on analyzing these systems by verifying that the system can accomplish its mission only using its initial budget of energy.

Besides schedulability, various objectives can be asked upon the scheduler. One of these can be to measure and minimize the energy consumption. This is a great concern in energy limited systems, like cell phones or satellites, and more generally the power consumption of computing devices is an emerging topic.

In this chapter we present a new optimization technique for multi-processor scheduling systems. It determines optimal mappings from tasks to processors in order to minimize the energy consumption of the system and/or response time. We propose algorithms that use statistical tests (ANOVA and TukeyHSD) to determine the optimal mappings.

Related Work Scheduling problems with energy costs are studied in [START_REF] Oddi | A multi-objective large neighborhood search methodology for scheduling problems with energy costs[END_REF]. This There also exists approaches that perform scheduling via timeline-based planning.

The work of [START_REF] Cimatti | Validating domains and plans for temporal planning via encoding into innite-state linear temporal logic[END_REF] proposes such an approach and uses timed game automata (timed automata with controllable and uncontrollable actions) to nd strategies for the timelinebased planning problem. Timed games and satisability modulo theory are also used in [START_REF] Cimatti | Dynamic controllability of disjunctive temporal networks: Validation and synthesis of exe-cutable strategies[END_REF] to solve control problems with temporal constraints. Our model-based approach is also based on extensions of timed automata but we mostly rely on statistical modelchecking for nding solutions to the scheduling problems. This allows us to consider more complex scheduling systems, with sporadic tasks, hierarchical scheduling or energy constraints, that would not be solvable using exhaustive techniques such as model-checking or timed games.

Another work presented in [CFO + 11] uses a logic-based approaches. The planning problem is encoded in a high level action notation modeling language [START_REF] Smith | The anml language[END_REF] and then translated into linear temporal logic modulo rational arithmetic formula. In our work,

we introduce new high level graphical notations for complex scheduling problems. These notations are specic to the scheduling framework being studied (either hierarchical or multi-processor scheduling systems). These domain-specic notations allow to have a simpler and more accurate description of a scheduling system than using existing formalisms. Moreover we can rely on the tool generator Cinco for easily generating a domain-specic tool that implements a graphical editor for these notations.

Formalisation

To formalize multi-processor scheduling systems with energy resources, we use formal models presented in Section. 2.5.1, and we extend formal models to take into account the energy consumption.

Adding energy to our timed automata models requires to extend the models with continuous variables and costs, using priced timed automata and hybrid automata. For measuring energy consumption we consider a multi-processor scheduling system with processors of dierent capabilities (frequencies). Based on CMOS technology, the power consumption is dominated by dynamic power dissipation P d when the processor is used by some task, given by the following formula:

P d = C * V 2 * f
where C is the capacitance, V the voltage and f the frequency. The processor speed is almost linear to the voltage:

f = k • V -V t V
where k is a constant and V t is the threshold voltage. We therefore get an approximated power consumption:

P d = k * f 3 k being a constant (C * k).
In our study we want to compare dierent congurations of the system according to the trade-o between speed (higher frequency) and energy consumption (lower frequency). We will therefore consider that the dierent congurations have the same constant characteristics by setting k = 1 and only compare the energy consumption using the formula:

P d = f 3
Then, our formal models for multi-processor scheduling systems dene a set of pro-cessors, each having a frequency and its own scheduler. Processors can use dierent scheduling algorithms. Tasks are statically assigned to one processor.

To measure the energy consumption of the system, we add to our formal models a simple PTA. It denes a cost variable energy whose rate is energy'=totalPow, where totalPow is the power of all the running processors. If we increase the speed of a processor (the frequency f ) we increase the energy consumption, but in return the task using the processor can run faster. We take this into account in our task model. The stopwatch clock t_et[tid] becomes a continuous variable that progresses at a rate t_et[tid]'=f, where f is the frequency of the processor that executes the task.

Scheduling Problems

In this section we present the dierent problems that we want to solve on scheduling systems.

Problem 1: Correctness and performance

To analyze the correctness of multiprocessor scheduling systems, we evaluate the properties presented in Section 4.

(absence of deadlock, schedulability, and maximum response time), and additionally we evaluate energy consumption property:

Energy consumption: We measure the average and maximum energy consumed by the system over a period of time.

Problem 2: Optimization, Conguration We consider a multi-processor system, with CPUs having dierent frequencies, and a set of real-time tasks. Our goal is to assign each task to a CPU. Then we evaluate the congurations of the scheduling system in terms of schedulability, response time and energy consumption.

Problem 3: Change detection We now want to monitor our scheduling system in order to detect emerging behaviors or an expecting event. We consider a property of the system, based on the measures presented in Problem 1, e.g., the energy is always lower than a given value. We consider our system as a stochastic process and we evaluate the property at regular steps during an execution. This allows us to compute at runtime the probability to satisfy the property. Then, our goal is to detect an abrupt variation of this probability, which will be the sign that some event happened.

Formally, let S be a set of states and T ⊆ R be a timed domain. A stochastic process (S, T ) is a family of random variables X = {X t | t ∈ T }, each X t having range S. An following probabilistic BLTL formula:

Pr[<= runTime]([] PlatformEnergy.energy <= maxEnergy)

where runTime is the time length for the simulations and maxEnergy is an energy bound.

With Uppaal SMC we compute the probability that the property is satised.

Optimization of a Multi-processor Scheduling System with ANOVA

We consider a set of CPUs, C = (CP U 1 , CP U 2 , . . . , CP U k ) and a set of real-time tasks T = (T 1 , T 2 , . . . , T l ). A multi-processor scheduling system is congured by specifying a mapping γ : T → C.

For each possible mapping, we would like to evaluate rst, if the system is schedulable, and second, the average energy consumption and/or the maximum response time of a task T i ∈ T . The Uppaal query that we use to evaluate the energy consumption is: ϕ e = simulate nbSim[<= runTime]{PlatformEnergy.energy} : 1 : false and to evaluate the maximum response time of a task with id i:

ϕ t = simulate nbSim[<= runTime]{max_resp[i] } : 1 : false
Finally we would like to compare the dierent congurations in order to select a schedulable conguration that has a minimum energy consumption and/or a minimum response time. If we want to achieve both objectives we are faced with a multi-objective optimisation problem. A simple solution would be to analyze each conguration with SMC experiments in order to compute values for the energy consumption and the response time. However this requires a lot of simulations per conguration to be able to compare them, as the condence intervals should not overlap. Fortunately, there exists a more ecient statistical technique to solve this problem that is called analysis of variance (ANOVA). The test has already been used to perform optimisation with SMC [DDGL + 13]. We propose in this chapter new algorithms based on this test.

ANOVA is a statistical test used to compare several probability distributions. We use it in a single factor conguration with a xed eects model, as presented in [START_REF] Montgomery | Design and Analysis of Experiments[END_REF].

We have k treatments of a single factor (the system conguration dened by a mapping γ) that we wish to compare. For each 1 ≤ i ≤ k, the observed response for treatment i is a random variable X i (the energy or response time) for which we draw n random values x i,1 , . . . , x i,n (computed by running n simulations of the system using the mapping γ i and a property ϕ e or ϕ t ). We denote X i the mean of the random variable X i and X the total mean all the values. ANOVA tests the null hypothesis that all the means of the treatments are equal, against the alternative hypothesis that at least two treatments have dierent means.

ANOVA is based on a comparison between the variability observed between the treatments and the variability observed within the treatments using the following F-value:

F = 1/(k -1) k i=1 (X i -X) 2 1/(n -k) k i=1 n j=1 (X i,j -X i ) 2
If the null hypothesis is true this F-value should follow a F-distribution dened by the degrees of freedom of the experiment, that are k -1 and n -k. To determine if the null hypothesis holds a classical hypothesis testing solution is to compute the P-value of the test. The P-value is the probability of observing a more extreme F-value than the actual result. It corresponds to the area under the probability density function of the distribution greater than the F-value, as shown in Figure . 5.1. Therefore, the lower the P-value, the lower the probability that the F-value computed actually follows the Fdistribution, and consequently the more likely the null hypothesis should be rejected. To make a decision we compare this P-value to a condence level α, for instance α = 0.05 for a 95% condence. If P-value ≤ α then the null hypothesis is rejected, i.e. some treatments have dierent means, with a 5% chance of making a Type I error. Tukey HSD If ANOVA shows that the means of the treatments are signicantly dierent, then we would like to determine which treatments dier in order to compare them. In [DDGL + 13] the test was used with treatments that are continuous variables (temperature thresholds). In their context, using ANOVA alone, the authors were able to valid a linear regression over the continuous variables in order to optimize the system In our context, the treatments (the dierent mappings) cannot be compared directly with ANOVA. The result of the test is only that at least two treatments dier, but we do not know which ones. Therefore we need an additional test to compare the treatments. This cannot simply be done by a series of pairwise T-test, as it would greatly increase the likelihood of false positive.

There exists however a multiple comparison test called Tukey HSD (Tukey's Honest Signicant Dierence test) that compares the means of every treatments to the means of every other treatment. It computes the pairwise dierences X i -X j with a condence interval. If the endpoints of the condence interval have the same sign (both positive or both are negative), then 0 is not in the interval and we conclude that the means are dierent. If the endpoints of the condence interval have opposite signs, then 0 is in the interval and we cannot determine whether the means are equal or dierent. Tukey HSD is based on a studentized range distribution. As for the ANOVA test, each comparison of the Tukey test can be associated to a P-value to measure the level of signicance.

Note that if the number of mappings is reduced to two, then Tukey HSD should be replaced by a T-test.

Algorithms Using the two statistical tests previously presented, we propose two new algorithms to optimize multi-processor scheduling systems. The algorithms determine dynamically the number of simulations needed to compare the means of energy consumption and/or response time with a sucient condence. Algorithm 1 has a single objective (minimizing the energy consumption or the response time), while Algorithm 2 considers both objectives simultaneously.

In these algorithms Simulate is a function that performs n simulation of a mapping γ and computes the values specied in the property ϕ (e.g. energy consumption or the response time). RunANOVA runs the ANOVA test on the simulations to determine if the mappings values are signicantly dierent. It returns the P-value of the test.

RunTukeyHSDSingle runs the Tukey HSD test on the simulations and determines the best mappings, which can be a single mapping, or a set of mappings that cannot be distinguished because there is not enough signicance, or because they have the same probability distributions. RunTukeyHSDMulti runs the Tukey HSD test and returns True if all the dierences have either a signicant dierence (P-value ≤ α) or are equal (Pvalue ≥ 1 -α). ComputeMeans computes the means of the values for each mapping given in parameter over all the simulations of the mapping.

Finally we are able to select the best congurations. Let (γ 1 , γ 2 , . . . , γ n ) be the set of schedulable congurations. We denote energy(γ i ) the average energy consumed Algorithm 1: Single objective multiprocessor optimization Input:

Γ: list of mappings n: initial number of simulations α: condence level ϕ ∈ {ϕ e , ϕ t }: simulation property.

Output:

bestM appings: set of mappings with minimum energy consumption or response time.

min: minimum mean of energy consumption or response time.

Let conf be a Boolean, initialised conf ← F alse bestM appings ← Γ foreach γ ∈ Γ do

Let simulations[γ] be the set of simulations of the mapping γ, initially empty.

while not conf do foreach γ ∈ bestM appings do

simulations[γ] ← simulations[γ] ∪ Simulate(γ, n, ϕ) P-value ← RunANOVA(simulations) if P-value ≥ 1 -α then conf ← T rue if P-value ≤ α then bestM appings ← RunTukeyHSDSingle(simulations, α) if |bestM appings| = 1 then conf ← T rue foreach γ ∈ Γ \ bestM appings do
Remove simulations[γ] from simulations min ← Min(ComputeMeans(simulations, bestM appings)) over a xed period of time and resp(γ i ) the maximum response time of one task. If we consider only one objective we select the conguration with the minimum estimated value for energy(γ i ) or resp(γ i ). If we consider both objectives simultaneously we should select a conguration that is Pareto-ecient. Formally, a conguration γ i is Paretoecient if there exists no other conguration γ j such that energy(γ j ) ≤ energy(γ i ) and resp(γ j ) ≤ resp(γ i ). We can plot the results on a graph and draw a Pareto-eciency curve that links the Pareto-ecient congurations.

We consider that Algorithm 2 produces the results given in the graph shown in The principle is to monitor the evolution of a probability measure at successive positions during a single execution of the system. The algorithm then detects the position where it drastically changes from original expectation. We have previously adopted the CUSUM algorithm to monitor a BLTL property over an execution trace of a stochastic process and to detect the position in the trace when the probability to satisfy the property changes signicantly [START_REF] Legay | Statistical model checking with change detection[END_REF].

Let π = (s 0 , t 0 ), (s 1 , t 1 ), . . . , (s n , t n ) be an execution of the stochastic process and ϕ a BLTL property to monitor during this execution. As dened in Problem 3, Y i are Bernoulli variables such that Y i = 1 i π i |= ϕ. We note p k = P r[Y i = 1|i <= k] the probability of satisfying ϕ from (s 0 , t 0 ) to the state (s k , t k ). CUSUM will decide between the two following hypothesis:

H 0 : ∀ k, 0 ≤ k ≤ n, p k < p change , i.e., no change occurs. H 1 : ∃ l, 0 ≤ l ≤ n such that the change occurs at time t l : ∀k, 0 ≤ k ≤ n, we have t k < t l =⇒ p k < p change and t k ≥ t l =⇒ p k ≥ p change .
We assume that we know the initial probability p init < p change of P r[π |= ϕ] before the change occurs. One solution is to estimate this probability with the Monte Carlo algorithm using an ideal version of the system in which no change occurs.

Like the Sequential Probability Ratio Test (SPRT) [START_REF] Wald | Sequential Tests of Statistical Hypotheses[END_REF], the CUSUM comparison is based on a likelihood-ratio test: it consists in computing the cumulative sum S k of the logarithm of the likelihood-ratios s i over the sequence of samples Y 1 , . . . Y k . The change is detected as soon as S k satises a stopping rule.

S k = k i=1 s i s i =          ln p change p init , if X i = 1 ln 1-p change 1-p init , otherwise
The typical behavior of the cumulative sum S k is a global decreasing before the change, and a sharp increase after the change. Then the stopping rules purpose is to detect when the positive drift is suciently relevant to detect the change. It consists in saving m k = min 1≤i≤k S i , the minimal value of CUSUM, and comparing it with the current value. If the distance is suciently great, the stopping decision is taken, i.e., an alarm is raised at a time t a = min{t k : S k -m k ≥ λ}, where λ is a sensitivity threshold.

CUSUM Calibration

The eciency of the CUSUM algorithm depends on several parameters. First, it is important to note that the likelihood-ratio test assumes that the considered samples are independent. This assumption may be dicult to ensure over a single execution of a system, but heuristic solutions exist to guarantee independence. One of them is to introduce delays between the samples. In that case Monte Carlo SMC analysis can evaluate the correlation between the samples, and help to select appropriate delays.

Second, the CUSUM sensitivity depends on the choice of the threshold λ. A smaller value increases the sensitivity, i.e., the false alarms rate. A false alarm is a change detection at a time when no relevant event actually occurs in the system. Conversely, big values may delay the detection of the change. The false alarms rate of CUSUM is dened as E[t a ], the expected time of an alarm raised by CUSUM while the system is still running before the change occurs. Ideally, this value must be the biggest as possible (E[t a ] → +∞). The detection delay is dened as the expected time between the actual change at time t and the alarm time t a raised by CUSUM (E[t a -t | t < t a ]). Ideally, this value has to be as small as possible.

To calibrate the sensitivity a solution is to use two versions of the model: one in which the change never occurs and one in which it always occurs. Running the CUSUM on the rst model allows to determine the minimum sensitivity such that no detection occurs. Then, the CUSUM is run on the second model to determine the detection delay.

High Level Framework

This section presents how to use the high-level domain-specic language presented in Section. 3.5 in order to represent our high-level framework dedicated to the design and analysis of the multi-processor scheduling systems with energy constraints.

High-Level Framework for Multi-Processor Scheduling Systems

For the design of CPS with multi-processor we consider a two-layer approach as proposed in [KLL + 15a]. The rst layer models the hardware platform, with a scheduling system composed of real-time tasks and CPUs. The second layer models the application that is composed of a set of actions. The link between the two layers is implemented by a mapping from actions to tasks, that species for each action of the application on which task it is intended to run. In our current framework this mapping is static and determined before the execution.

This design allows a separation of concerns that facilitates the verication of formal properties:

Scheduling properties are veried on the platform layer only.

Logical properties of the application are veried on the application layer only.

Energy consumption or execution time properties need to consider both layers simultaneously.

We have implemented with Cinco a high-level framework that allows to design a two-layer multi-processor scheduling system.

Platform Layer The platform layer is composed of a set of processors and a set of real-time tasks. Each processor has its own scheduling mechanism and is parametrized by its own frequency. The frequency denes the speed of the processor and its energy consumption when running. Real-time tasks can be either hard real-time, with a deadline, a period and execution times, or soft real-time, with only period and execution times.

Tasks are statically assigned to a processor. A model of a platform layer designed in our framework is presented in Figure . 5.3. This model is translated into a set of timed automata, using the models presented in Section ??. Mapping between application and platform The mapping between the two layers is done by linking each action of the application to a real-time task, as presented in Queries: In this framework we consider dierent type of queries, some of them associated to the platform and some of them associated to the application. On the platform layer we verify schedulability queries and we determine optimal mapping between tasks and processors with ANOVA, as presented in Section 5.4.2. On the application layer we measure average energy consumption and we use CUSUM to detect changes in the application behavior.

Implementation of the Framework and Tool Chain

To implement our domain-specic framework dedicated to the design and analysis of multi-processor scheduling systems, we use the tool chain described in Section. 3.5.2. We detail below the basic steps performed by our analysis programs to solve the dierent scheduling problems.

Optimisation of Multi-Processor Scheduling Systems We have implemented Algorithms 1 and 2. Our program generates a set of Uppaal models, each corresponding to a conguration of the system with a mapping from tasks to processors. It then runs the optimisation algorithm. This algorithm launches some simulations with Uppaal SMC and extracts the numerical results. The results are written in some temporary les. that are analysed with the statistical tool R to perform the RunANOVA, RunTukeyHSDSingle, RunTukeyHSDMulti and ComputeMeans procedures. According to the results the program determines if more simulations are needed, or outputs the result.

For the single objective problem the program directly shows the optimal mapping by drawing it on the interface using the transformation API of Cinco.

Experiments

This section presents an example of a multi-processor scheduling system designed and analyzed in our framework. We rst describe the model and then we present the experiments performed in our framework to solve the problems presented in Section 5.4.

Example

The proposed example is composed of two layers, following the modeling framework presented in Section 5.5, a Platform layer and an Application layer.

The Platform Layer is composed of 3 periodic hard real-time tasks and 2 processors.

The tasks parameters are congured according to the following order: Task(period,deadline, bcet,wcet,priority), and are respectively T 1 (10, 10, 3, 4, 9), T 2 (20, 20, 5, 6, 8) and T 3 (30, 30, 6, 8, 7).

The 2 processors are P 1 , with a 1.5 MHz frequency and a FP scheduling policy,and P 2 , with a 1.0 MHz frequency and an EDF scheduling policy. We initially distribute T 1 and T 2 on processor P 1 , while T 3 is running alone on processor P 2 .

The Application Layer consists of 3 components, each composed of a succession of actions as presented in Figure . 5.6. Component C 1 is composed of actions A 1 , A 2 Each action has an energy parameter that denes how much energy it takes when running on a processor, with a maximum value of 1 meaning that it takes the full power of the processor.

Finally, random delays with uniform distributions are set between the execution of each actions. As explained in Section 5.5 the execution of each component is cyclic:

it runs sequentially each action, and then starts again at the rst action. Action A 8 is additionally delayed, such that is starts only after 50 or 100 executions of action A 7 .

Using the change detection problem and CUSUM we will try in our experiments to detect the beginning of execution of this action.

Checking Correctness and Evaluating Performances

Experiments Using SMC we perform the following experiments on the initial model:

1. Schedulability analysis.

2. Measure of energy consumption, considering the platform only and both the platform and the application.

3. Measure of the maximum response time for each task.

We use 100 simulations and a runtime of 60 t.u. This runtime allows to execute the model over the smallest common multiple of the periods of our tasks (the hyper-period).

Results The results of these experiments are presented in Experiment This second experiment consists in nding optimal mappings between tasks and processors, such that the system is schedulable and has optimal performances.

Therefore we start by removing in our model the mapping used in the previous section.

Then we use the ANOVA method with the multi-objectives Algorithm 2 proposed in Section 5.4.2. Our two objectives are to minimize the energy consumption of the scheduling system and the maximum response time of one of the tasks. The result is a Pareto eciency diagram.

For this experiment we will use SMC with 100 simulations to determine schedulability, and Algorithm 2 with ANOVA and Tukey HSD techniques with a 95% condence.

Results Table 5.2 presents the results of executing Algorithm 2. We perform 3 executions of the algorithm (Exec. 1, Exec. 2 and Exec. 3) that are dierentiated according to the task for which we want to minimize the maximum response time. One execution takes approximately 40 seconds. We determine that there are 8 mappings schedulable, simply named mapping-i with i from 1 to 8. Then for each execution we give in column E the energy consumption of the processors, and in column t(T i ) the maximum response time of a task T i .

Let us now consider that task T 2 is our critical task for which we want to minimize the maximum response time. From the results given in columns 4 and 5 we can plot in our framework a Pareto diagram in a pop-up window, as shown in Fig. 5.7. From this window we can select one of the Pareto-ecient mapping that will then be automatically Information Leakage

High-security processes have to load condential information into shared resources as part of their operation. This condential information may be leaked (directly or indirectly)

to low-security processes via the shared resource. In this chapter, we consider leakage from high-security to low-security processes from the perspective of scheduling. The workow model is here extended to support preemption, security levels, and leakage.

Formalization of leakage properties is then built upon this extended model, allowing formal reasoning about the security of schedulers. Several heuristics are presented in the form of compositional preprocessors and postprocessors as part of a more general scheduling approach. The eectiveness of these heuristics is evaluated experimentally, it shows signicantly better schedulability than the state of the art. Modeling of leakage from cache attacks is presented as a case study.

Key Contributions. The key contributions in this chapter are as follows:

A model to reason quantitatively on the amount of information leaked by scheduling tasks with dierent security levels on a shared resource system.

A scheduling approach with compositional and specialized pre-and postprocessors that schedule tasks while reducing the amount of condential information leaked.

Several heuristic pre-and postprocessing algorithms that can reduce leakage.

Experimental evaluation of the combinations of the pre-and postprocessors, showing that the approach provides signicantly better schedulability and lower information leakage than the state of the art.

A case study showing how to adapt the model to other scenarios and kinds of leakage, demonstrated with cache attacks.

Introduction

This chapter considers a shared resource system where processes are classied as either high-security or low-security. High-security processes work with condential information that should not be leaked to low-security processes. Typically, this includes loading condential information into memory for use within high-security processes. Examples of such condential information include encryption keys, medical data, and bank details.

This condential information may be vital to the operation of the high-security processes, but must also be tightly controlled and not be leaked to low-security processes. For instance, in an embedded sensor, high-security encryption processes handle encryption keys that must not be leaked to low-security data compression processes.

Example Consider the small example in Figure 6.1, written in Intel x86-64 assembly code for Linux compiled to ELF format 1 . There are two processes: Process 1 doing some (trivial) encryption operations, and Process 2 attempting to access the encryption key. Process 1 takes a key $KEY and a message $MSG then encrypts the message with the key using an exclusive or XOR operation. The result is then output to the disk (represented by $DISK1). Process 2 writes to a dierent disk location (represented by $DISK2) the content of register r13. It is clear that if Process 2 is executed after the rst operation and before the fourth operation of Process 1, then the value of the key is directly leaked.

However, high-security processes may not properly ush condential information from the shared resource, or context switching may interrupt their execution before such ushing can be applied. Consequently, condential information remaining in the shared resource becomes (directly or indirectly) available to low-security processes.

If a scheduler is aware of a process' access level, then the scheduler can take actions to prevent condential information being leaked to low-security processes. Recent work [MYPB14, PPY

+ 15] has explored these kinds of problems in a real-time setting by scheduling a complete resource (memory) ush after any high-security process that is followed by a low-security process. However, this provides only limited options to the scheduler since such a complete resource ush is expensive and may prevent real-time tasks from meeting their deadlines. Furthermore, when ushing is not possible, current approaches do not quantify the information leakage, simply considering any leakage unacceptable.

In this chapter we propose treating condentiality, measured by the resulting leakage of secure information, as a quantitative resource that the scheduler can exploit. This allows for a better quantication of the resulting leakage in dierent scenarios, as well as having a clear measure of the cost of dierent scheduling choices. Further, this allows for the creation of schedulers that can make better scheduling choices and also respect condential information leakage constraints.

We built our work upon the workow model commonly used to represent real-time systems [START_REF] Benoit | A survey of pipelined workow scheduling: Models and algorithms[END_REF][START_REF] Graham | Bounds for certain multiprocessing anomalies[END_REF][START_REF] Yoon | Taskshuer: A schedule randomization protocol for obfuscation against timing inference attacks in real-time systems[END_REF]. In the workow model a set of tasks periodically produces jobs that have to be scheduled to complete before deadlines.

The workow model is here extended by considering tasks to be composed of steps, each of which has an execution time, leakage value, and security level. Each one of these steps is implicitly an atomic sequence of actions that can be taken within a task without preemption by the scheduler. Thus a task consists of an ordered sequence of steps to be performed, that yields to the total behavior of the task.

Related Work

Real-time systems need to communicate with the outside world, such as receiving data from sensors or communicating with other systems, sometimes over unsecured networks.

This communication has allowed attacks against even air-gapped industrial control systems [START_REF] Falliere | [END_REF].

The real-time scheduling requirement itself can be exploited to generate additional vulnerabilities. For instance, a process can modulate its use of a resource to aect the scheduling of another process, and use this to covertly transmit information [START_REF] Son | Covert timing channel capacity of rate monotonic real-time scheduling algorithm in MLS systems[END_REF][START_REF] Hyuk | Integrating security and real-time requirements using covert channel capacity[END_REF].

Further vulnerabilities can occur in any system with shared resource. When processes with dierent security levels share the same memory resources, it is possible for lowsecurity processes to access condential information that should only be accessed by high-security processes [START_REF] Mohan | Realtime systems security through scheduler constraints[END_REF]. Using separated memories for processes with dierent security levels is expensive, particularly if the system has more than two security levels. Another less formal approach is that used in [START_REF] Varadarajan | Scheduler-based defenses against cross-vm side-channels[END_REF] where they limit the time between preemptions between virtual machines in an online scheduling scenario to prevent cache attacks. This could be analysed using the formal approach and methodology here, albeit as a specic case study.

Formal analysis of scheduling system under resource constraints has been performed by Kim et al. [KLL + 15b, KLT + 16b]. The proposed approach can be extended to con- dentiality as a resource using the model proposed in this chapter.

Model

The model here is based upon the workow model recalled in Section 1.3. The extension here is to represent more precise information about the internal operations and preemptivity of tasks by dividing them into steps. These steps include their own execution time (like a task or job from the workow model), and are extended to include leakage value and security level. Special tasks are also added to model other operations of the system.The rest of this section details this extended model and presents illustrative examples that motivate the choices in this chapter.

Concept

This section considers concepts and motivations behind our information leakage model.

In particular, the division of tasks into steps, how to account for leakage in practice, and justication for special tasks.

Steps. This model considers the possibility to divide tasks into ne-grained steps. A step represents an atomic sequence of operations that cannot be interrupted by preemption.

The practical implementation of steps depends on the architecture and granularity of the scheduling system.

The model is agnostic to step implementation details as long as an execution time, leakage value, and security level can be dened for each step. The most ne-grained approach would be to consider each CPU operation as a step. For instance, Process 1 in Figure 6.1 would be represented as a task divided into ve steps. Thus, a task could be preempted after each CPU operation. Although very simple, in practice this approach is too ne-grained. In lightweight and embedded systems it is common to delegate part of the handling of preemption and atomicity to the programmer, so it is reasonable to consider that the programmer itself could dene the steps.

Special Tasks. We consider two special tasks representing special system operations: ush and wait. The ush task ushes all condential information from the shared resource, for instance by overwriting all shared memory with zeroes. This preserves compatibility with the state of the art [MYPB14, PPY + 15] where ushing is used as the main tool to preserve condentiality. The wait task represents idle processor time. Apart from the obvious use, scheduling of idle time can impact condentiality of the system.

Leakage Values. The leakage value of a step represents the amount of condential information that would be leaked to an attacker able to read the shared resource just after the execution step. The model does not constrain the way the leakage value is obtained: leakage can be added by the programmer as an annotation, computed by an automatic tool [BLTW13, CMS14, CKN14, VEB + 16], or possibly both.

For instance, the programmer could specify critical zones in which the program must not be interrupted, and the leakage values would be computed automatically by a tool (for both critical and non-critical zones).

An alternative, variable-based approach would be to have the programmer annotate some variables as containing condential information at a certain point (and as cleared of condential information at a later point). Taint analysis can be used to identify which variables are tainted at each point. Information leakage quantication can be used to quantify leakage from the tainted variables. Example Observe that Process 1 in Figure 6.1 can be modeled by the following task:

T α = T (P α , D α , S αa (1, 1, ) S αb (1, 1, ) S αc (1, 1, ) S αd (1, 0, ) S αe (1, 0, )) .
Similarly, Process 2 in Figure . 6.1 can be modeled by the following task:

T β = T (P β , D β , S βa (1, 0, ⊥)) .
Denition 6.3 (Job). Each job τ x,k is created by the activation of the task T x at release time R x,k = (k -1)P x for k ∈ N 0 , and is a tuple τ x,k (R x,k , A x,k , S x,k ) where A x,k = R x,k + D x is the job's absolute deadline, and S x,k is the sequence of steps inherited from task T x .

Jobs are named with the corresponding task's Greek letter and the number k, so job τ β4 is the fourth job generated by task T β and step S β4c is the third step of job τ β4 .

For simplicity, a task (resp. job) will be referred to as or ⊥ when all steps within that task (resp. job) are either or ⊥, respectively. Flush and Wait. The model uses a task to represent complete ushing of the shared resource. The ush task is dened by T F (-, -, S F (E F , 0, )) where E F is the execution time to completely ush the shared resource. Observe that after ushing the shared resource the leakage is reduced to zero. This is achieved by the single step S F (E F , 0, ) that takes all the execution time of the ush task and has a zero leakage value. Since the ush task is always available to be scheduled, it has no dened period or deadline (denoted here as -), being able to schedule (or not) at whim. The security level of ush is since it is acceptable for ush to have access to condential information, and for use in calculating the resulting leakage (see below). For simplicity and when no ambiguity may occur, F is used for the ush task or step.

To represent idle processor time, dene the wait task as T W (-, -, S W (1, * , * )) . Similar to ush, wait is always available to be scheduled and has no period or deadline (again denoted as -). Wait also has a single step that has the minimal runtime of one time unit.

However, the leakage value of wait is here denoted by * since waiting does not change the shared resource, instead the * denotes that the leakage value of a wait step is the same as the previous step. Similarly, the security level is also represented by * because it is the same as the previous step. Again for simplicity and where no ambiguity may occur, W may be used in place of the wait task or step. (a) each step in S appears in the trace S in the order that it appears in S;

(b) the rst step of S does not start execution before R;

(c) the last step of S does not terminate execution after A; 2. each step that is not wait W or ush F appears exactly once in the trace S.

Given a set of tasks Γ, a solution S is a solution for Γ, written S Γ , i ∀T x ∈ Γ, ∀k ∈ N 0 then for each job τ x,k (R x,k , A x,k , S x,k ) it holds that every step in S x,k is in S.

A solution S is periodic if it periodically repeats the same sequence of steps up to job indexing. For simplicity, a periodic solution may be represented by the periodically repeated sequence alone.

Given a trace S the resulting leakage L ( S) of trace S represents the total amount of information leaked during the execution of the jobs scheduled according to S. Denition 6.6 (Resulting leakage). Given a trace S composed of n steps with n ∈ N ∪ {∞}, the resulting leakage L ( S) of the trace S is dened inductively as follows:

if n ≤ 1, then L ( S) = 0;
if n > 1 and the second step S 2 of trace S is , then the resulting leakage is the leakage of the trace without the rst step if n > 1 and the second step S 2 of trace S is ⊥, then the resulting leakage is the leakage of the trace without the rst step S 1 = S(E 1 , L 1 , X 1 ) plus the leakage value L 1 of the rst step S 1 : L ( S) = L ( S \ S 1 ) + L 1 .

Since every solution S is a trace S, a solution resulting leakage L (S) is dened in the same manner.

Example Recall the example from Figure 6.1. The solution in Figure 6.3a has resulting leakage one, since Process 2 is executed when the key is in the shared resource and so the step S βa is able to access the key.

However, the solution in Figure 6.3b has resulting leakage is zero, since Process 2 is executed after the key has been wiped from the shared resource.

If a solution is periodic, the periodic leakage can be calculated as follows. Given one instance of the periodically repeated sequence of steps S = (S 1 , S 2 , . . . , S i ), the periodic leakage is the resulting leakage of the sequence S ++S 1 .

(a) Solution leaking information.

(b) Solution leaking no information.

Illustrating Examples

This section presents three examples illustrating the utility of the model. Each presents a dierent aspect of using the model to nd solutions with good resulting leakage.

Periodic Leakage This example illustrates leakage due to the periodic nature of tasks and how to account for this when scheduling. Consider two tasks: a task T α (3, 3, S αa (1, 0, ), S αb (1, 4, )) and a ⊥ task T β (3, 3, S βa (1, 0, ⊥)). The goal is to nd a solution with minimal (here zero) resulting leakage.

Two periodic solutions to these tasks are depicted in Figure 6.2a & 6.2b. Note that the step S α1a has leakage value zero, so even if S α1a is followed by the ⊥ step S β1a this does not increase the resulting leakage. Thus both periodic solutions have a resulting leakage of zero within their periodically repeated sequence (here corresponding to their hyperperiod). However, when the periodically repeated sequence is repeated, the periodic solution in Figure 6.2a has non-zero periodic leakage, since at time four the step with leakage value four S α1b is followed by the ⊥ step S β2a on periodic scheduling.

Hence, only the periodic solution in Figure. to be scheduled after the last ⊥ step in the periodically repeated sequence (again corresponding here to the hyperperiod) and still meet its deadline. Observe that since S α2a has zero leakage value, the periodic solution has zero periodic leakage. This periodic solution with zero periodic leakage would not be possible if W was not available to be scheduled at any time (in particular as an alternative to scheduling the step S α1b ), since without W then S α1b would be scheduled before S β2a and thus increase periodic leakage.

Periodic Flush Since nding a solution for a set of tasks is generally best solved in a periodic manner, it is possible to exploit this periodic nature when constructing the solution. For example, the total amount of time units not used by jobs can be calculated, and then these time units can be used to consider adding F. Typically, such free time units would be fragmented inside the solution. However, with this information, the scheduler can use suciently long empty spaces (or create them) to schedule F. Hence, even if it may not be possible to ush the memory after each step followed by a ⊥ step, some additional F can be scheduled to reduce the solution's resulting leakage while maintaining schedulability.

For example, consider two tasks: a task T α (8, 8, S αa (1, 5, ), S αb (1, 1, ), S αc (1, 6, ), S αd (1, 4, )) and a ⊥ task T β (3, 3, S βa (1, 0, ⊥)). Here let the execution time of F be two, i.e. E F = 2. Consider the scheduling of the two tasks over their hyperperiod of twentyfour time units (when developing periodic solutions, the hyperperiod is a convenient choice since periodicity is guaranteed). A periodic solution can be seen in Figure 6.4.

No solution with resulting leakage zero exists. Further, it is not possible to schedule the jobs by inserting an F after every step followed by a ⊥ step since this would not be schedulable (this is the state of the art as in [START_REF] Mohan | Realtime systems security through scheduler constraints[END_REF]). However, the periodic solution in Figure 6.4 achieves a low periodic leakage of three per hyperperiod while maintaining schedulability by adding two F steps to minimize the periodic leakage.

Problems

Information leakage (or just leakage) quanties the amount of privileged information leaked (lost to an attacker) by a system, and is widely used to obtain a measure of the (in) security of the system [KLT + 16b, BLMW15, ACPS12, BKR09]. In our work, leakage is used to measure the amount of privileged information that a high-security job leaves in the shared memory at dierent moments of its execution. We will consider the unit of measure of leakage to be bits, following the standard for information-theoretical leakage measures [START_REF] Biondi | Information leakage as a scheduling resource[END_REF]. However, the same leakage model could be used to appropriately measure the loss of any measurable security property, where zero represents no loss.

Similarly, we do not constraint the way the leakage value is obtained: it could be added by the programmer as an annotation in the source code, or automatically computed by one of the many tools available [BLTW13, CKN14, VEB + 16].

Methods

The overarching goal of the approach proposed in this chapter is to produce a solution with a low resulting leakage for a given set of tasks. To achieve this, standard oine scheduling algorithms are extended with a preprocessing and a postprocessing phase. The preprocessing phase transforms a set of tasks Γ into a set of preprocessed tasks Γ . Then scheduling is applied to Γ obtaining a solution S Γ for Γ . Finally, the postprocessing phase transforms the solution S Γ into a postprocessed solution S Γ . Both the pre-and postprocessing phases can aect the desired solution S Γ , here with the goal of reducing the resulting leakage. The rest of this section presents various heuristic algorithms used for the experiments (see Section 6.6). The scheduling algorithms considered are EDF and LSF. Note that EDF and LSF do no consider the security-level or leakage of the steps (for discussion of this see Section 6.7). The rest of this section focuses upon the pre-and postprocessors. The division in phases creates a modular and compositional approach, allowing for a better comparison of dierent pre-and postprocessors.

Preprocessing

Preprocessors are algorithms that take a set of tasks Γ and produce a set of tasks Γ to be scheduled.In our work, we consider preprocessors that attempt to merge adjacent steps with the same security level within each task in Γ. The merged step has the sum of the execution times of the merged steps, the leakage value of the last merged step, and the same security level as the merged steps. For instance, the steps S αa (1, 0, ) and S αb (1, 4, ) could be merged producing the step S αa (2, 4, ). The rest of this section presents three preprocessing algorithms that exploit merging.

Total Merge. The Total Merge algorithm merges all the steps in a task into a single step (as detailed in Algorithm 3). The merging is achieved by starting with a step that has execution time and leakage value zero. The execution time for each other step in the task is then added, and the leakage value from the last step being merged is preserved. The security level is set to that of the last step. Finally, the processed task uses this single merged step as its only step.

One-Step Merge. The One-Step Merge algorithm attempts to merge pairs of adjacent steps. Adjacent pairs are merged if the leakage of the former step is higher than the latter. This is achieved by iterating through the steps S i of the task. If L i > L i+1 , then the steps S i and S i+1 are merged. Otherwise, S i is maintained unchanged. This algorithm generates a new sequence of steps S , that are then used in the processed task Details can be seen in Algorithm 4.

n-Step Merge. A straightforward extension to the One-Step Merge algorithm is to allow the merging of any number of steps. This appears in the results as n-Step Merge.

Postprocessing

Postprocessing algorithms take one solution and produce another solution. This can be done by any possible manipulation of the steps within the original solution S Γ to produce the new solution S Γ that does not break the property of being a solution for Γ.

The rest of this section presents four such postprocessors.

Experiments

This section discusses the results obtained by running experiments with the preprocessing, scheduling, and postprocessing algorithms in this chapter.

The experiments were conducted by using approximately 30,000 randomly generated sets of tasks2 , and then testing each possible combination of one preprocessing, one scheduling, and one postprocessing algorithm. Each set of tasks consists of 2 to 6 tasks with at least one task and one ⊥ task, with each task having 1 to 8 steps, and each step execution time from 1 to 5.

Preprocessor Postprocessor Merge

None Add Flush Swap Move 1-Swap None will not be considered further in this chapter.

Figure 6.5 also shows that, for all preprocessing algorithms, EDF performs better for schedulability than LSF. (This is expected since EDF is guaranteed to nd a solution if the tasks are schedulable, while LSF is not.) The two scheduling algorithms produce almost the same results for every other measure tested, so the rest of this chapter shall present only experimental results using the EDF scheduling algorithm.

Comparing the experimental results from postprocessing algorithms, the average resulting leakages for each combination of pre-and postprocessor is shown in Figure 6.6, while the average running times to generate a solution are shown in Table 6.1.

As expected, solutions without any postprocessing produce the highest resulting leakage. The best resulting leakage is obtained by the Add Flush algorithm. (This would correspond to the approach in [MYPB14, PPY

+ 15] when combined with the Total Merge, however as noted above this is often not schedulable.) Note that merging preprocessors reduce total time, since they reduce the number of steps that the scheduler has to schedule.

1-Swap slightly reduces the resulting leakage, however Table 6.1 shows that it is signicantly more expensive than the scheduling operation, so 1-Swap could be applied after Add Flush only if the cost is acceptable. Swap and Move do not reduce the resulting leakage signicantly more than 1-Swap and are signicantly more expensive to compute. This indicates that there is a balance to be found depending on the scenario. Taking signicant time to pre-compute an optimal scheduling strategy for a sensor or other real-time system prior to shipping could be worth the time cost. However, for online scheduling with limited (or no) ability to look ahead and consider such options, the cost of anything more complex than Add Flush or 1-Swap may be too much.

Discussion

On the Division of Scheduling into Three Phases. The division into three phases is to separate out distinct parts of an overall scheduling from tasks to a solution. This approach allows for separation conceptually of dierent phases, and also for composition of simple algorithms in the pre-and postprocessing phases. For example, a postprocessor could move steps in a solution around to maximize contiguous Ws and then be composed with the Add Flush postprocessor to improve the resulting leakage further. This also allows dierent strategies to be employed in dierent phases, including strategies with dierent goals. For example, processors for resulting leakage minimization and energy consumption could be combined during pre-or postprocessing (or both).

Online Scheduling. In our work, we consider oine scheduling, i.e. when the tasks to be scheduled are known beforehand. In most real cases the tasks appear at runtime, requiring online heuristics to decide the scheduling. The division in steps and the leakage model presented in this chapter extend immediately to the online scenario. While the preprocessors and postprocessors do not, they provide insight that can be used to build online heuristics that reduce leakage. We consider this as a future work.

Execution Time. This chapter consideres the execution time to be essentially xed for each step. Although formally the execution time is worst case, the scheduling here does not exploit when steps may terminate prior to their (worst case) execution time. This could naturally be incorporated into online scheduling (above), but even in a purely oine scheduling system this could be exploited. For example, consider the cache attack scenario, where ushing not only aects the leakage, but by ushing the cache the execution time will go up due to cache misses.

Conclusion

In this manuscript we focused our work on nding new advanced techniques for exploiting the scheduling theory in order to analyze the correctness of CPS under various types of properties.

First, we have presented a software engineering approach that generates model-based analysis tools for the schedulability analysis of CPS. This approach is based on one side on a set of formal models for describing complex scheduling problems, and on the other on meta-models of high-level specication languages to easily specify these scheduling problems. Our approach generates automatically domain-specic analysis tools based on the Cinco framework. These tools allow to specify scheduling problems using graphical components, and they can launch formal analyses by calling model-checking tools such as Uppaal and Uppaal SMC.

On Hierarchical Scheduling Our rst domain-specic tool is designed to analyze hierarchical scheduling systems, using a stochastic model to represent stochastic behavior of the system, this model gives us the possibility to represent more complex systems and analyze their schedulability.

As an example for our rst framework we propose to model an avionic system, on which we execute a number of experiments in order to verify its schedulability, and also to compute the minimum budget for which the whole system is schedulable. We present in this manuscript the results of these experiments.

On Energy Consumption We have also presented new statistical model-checking algorithms that perform optimization or runtime monitoring. These algorithms are based on statistical tests like ANOVA and CUSUM. They are implemented and embedded into our analysis tools. Our second domain-specic tool is designed to analyze scheduling of multi-processor systems with the energy constraint.

For this second framework, we propose an example to illustrate how to use the algorithms proposed for the optimization of the energy consumption and the detection of signicant probability variation. The results of these experiments and their analyses are presented to consolidate our work.

Second, we proposed a new model that consider information leakage as quantitative resource that the scheduler can exploit In a system with shared resources, the security of condential information is a major concern.

On Information Leakage This manuscript allows reasoning about leakage of condential information by extending the workow model to support ne-grained preemption and condentiality. This allows condentiality to be addressed by quantifying the amount of information leaked by the system, including dierent leakage models.

Scheduling in this new model is then considered using pre-and post-processors. These can be computationally combined for scheduling that exploits dierent techniques and approaches, including focusing on dierent aspects of the overall problem. Several preand post-processing heuristic algorithms are presented that can operate on the model.

These are focused on improving resulting leakage, but the principles can be adapted to other problems as well.

In order to evaluate these heuristic algorithms, experiments were conducted by using approximately 30,000 randomly generated sets of tasks, then testing each possible combination of one pre-processing, one scheduling, and one post-processing algorithm. The results of these experiments demonstrate that the model and the heuristics improve over the state of the art and show that even simple heuristics can be eective.

Future work the next step in our work would be to improve our models by extending the model banks in order to analyze more complexe systems. Adding to that, we can also focus on improving treatment time by using parallelism theory advantages, these improvements allow as to treat more information in a small time which would improve the condence of our results.

Another axis that we can follow could be to generalize our models to deal with multi-resource approaches, where scheduling algorithms considers a number of dierent properties at the same time. For example consider condentiality, energy consumption, schedulability, etc.

In fact, multi-resource approaches could be a very good solution to analyze complex systems that have energy constraints, and must interact with other systems to accomplish its mission at the same time. These interactions could expose the condential information of the system under consideration.

Concerning the model that consider condentiality problem, one direction that can be followed would be to generalize this model in order to treat on-line scheduling algorithms.

On-line scheduling algorithms are designed to deal with real-time systems that interact with external environment through dierent sensors. The on-line scheduling algorithm must schedule the entering task and take into consideration the condentiality problem.

Another direction would be to consider theoretical complexity, that can help to improve the eciency of the heuristic algorithms. The heuristic algorithms could be proposed to aim dierent objectives, as example one objective could be to nd a solution that gives optimal condentiality by reducing the resulting leakage to zero. Another objective could be to nd a solution with a xed value of the resulting leakage.

Finally, in our work we proposed a composed strategy that combines pre and postprocessors in order to solve the condentiality problem, a good direction that could be followed is to improve this strategy or to propose other strategies that could give better solutions for this problem.

  Les algorithmes classiques d'ordonnancement des systèmes temps réel se basent sur la priorité des taches et leurs échéances respectives. La priorité de la tâche peut être une valeur xe donnée initialement, ce type d'algorithmes est dit Statique, ou peut être une valeur variable calculer lors de l'exécution de l'ordonnancement, ce type d'algorithmes est dit Dynamique. Pour décrire des systèmes plus complexes les techniques basées sur des modèles utilisent des modèles formels tels que les Systèmes de Transition et les Automates Temporisés pour spécier le comportement logique du système et les contraintes temporelles. Des extensions aux automates temporisés permettent également de spécier des mécanismes d'ordonnancement ou des problèmes d'énergie. Une première contribution de la thèse est de proposer un nouveau modèle stochastique pour décrire des tâches dont le temps d'exécution n'est pas xe, mais décrit par une distribution de probabilités. Ce modèle peut être utilisé pour représenter des tâches apériodiques dont leur déclenchement est dû à des événements extérieurs au système, et leur temps d'exécution n'est pas xe et dépend de l'ensemble des tâches qui constituent le système. Pour analyser ces modèles formels complexes on utilise des techniques de vérication automatisée tel que le model-checking. Cette technique permet de vérier la satisfaction de propriétés décrites en utilisant une logique formelle. Elle consiste à explorer toutes les exécutions possibles du modèle et vérier la satisfaction de la propriété étudiée à chaque exécution. Une alternative est la technique de model-checking statistique (SMC) qui traite un échantillon de l'ensemble de scénarios des exécutions possibles pour quantier la probabilité de satisfaction d'une propriété donnée. Cette méthode est utilisée pour gérer le problème d'explosion d'état, c'est-à-dire le nombre d'états nécessaires pour modéliser le système avec précision, qui peut facilement dépasser l'espace mémoire disponible sur l'ordinateur. Enn cette thèse propose d'utiliser un langage de haut niveau pour avoir une description graphique simpliée des modèles formels. Cette représentation graphique est transformée automatiquement en un ensemble de modèles formels, puis les diérentes propriétés peuvent être vériées sur ces modèles en utilisant l'outil de vérication Uppaal. Les résultats de la vérication formelle sont analysés et les informations les plus pertinentes sont achées graphiquement sur le modèle graphique. Cette thèse étudie trois catégories de problèmes d'ordonnancement dans les systèmes temps réel. Le premier modèle analyse des systèmes d'ordonnancements hiérarchiques (HSS). Les HSS sont des systèmes d'ordonnancement complexes avec plusieurs algorithmes d'ordonnancement. Nous construisons tout d'abord une banque de modèles formels générique à l'aide d'automates temporisés. Ces modèles sont utilisés pour représenter le comportement des diérents composants du système étudié. Nous utilisons en particulier le modèle de tâches temps réel stochastiques implémenté à l'aide d'automates temporisés probabilistes (PTA). Cette banque de modèles est utilisée pour construire des HSS complexes. Pour modéliser les HSS on utilise un langage de haut niveau spécique implémenté avec l'outil Cinco. Cinco est un générateur d'outils de modélisation. Il permet de spécier les fonctionnalités d'une interface graphique dans un langage de méta-modèle compact, et il génère automatiquement à partir de ce méta-modèle un outil d'analyse spécique au domaine avec une interface graphique. A l'intérieur de cet outil d'analyse, nous pouvons dénir les spécications d'un HSS et les propriétés qu'il doit satisfaire. Nous pouvons ensuite lancer l'analyse des propriétés. Cela génère automatiquement les modèles d'automates temporisés en utilisant les composants de notre banque de modèles. Les outils Uppaal et Uppaal SMC sont ensuite utilisés pour eectuer l'analyse. Cette approche permet de masquer complètement les modèles formels utilisés par le concepteur du système qui peut se concentrer sur la structure et les paramètres du HSS.

Figure 1

 1 Figure 1.2 Preemptive Scheduling algorithm

Denition 2 . 1 (

 21 Transition System). A transition system is a tuple (Loc, Act, E, I, AP, L) where Loc is a set of locations; Act is a set of action; E ∈ (S × AP × S) is a transition relation; I, I ⊆ S is a set of initial states;

Figure 2 . 1

 21 Figure 2.1 Light Switch Transition System TA

  tems. Invariants are indicated inside locations and are omitted when equal true. Edges are labeled with the guards, the action, and the set of clocks to be reset. Empty sets of clocks are often omitted. The same applies to clock constraints that are constantly true. The reset of set D of clocks is sometimes indicated by reset(D). If the actions are irrelevant, they are omitted.

Figure 2 . 2

 22 Figure 2.2 Examples of timed automata with a single clock and one example of the evolution of their clock over time.

Figure 2 .

 2 Figure 2.2b describes the evolution of the clock x through time. The system do not

Figure 2 .

 2 3 four examples of the dierent types of models. All these models implement a simple real-time task with various functionalities, depending on the type of model being used.

Figure 2 . 3

 23 Figure 2.3 Implementations of a simple real-time task with timed, stopwatch, priced and hybrid automata

Figure 2 .

 2 4 allows to select two values for the period of the task: 10 with probability 2/3 or 15 with probability 1/3. In what follows, we will call this automaton a dispatcher.

Figure 2 . 4

 24 Figure 2.4 Stochastic dispatcher implemented with a stochastic TA

Figure 2 .

 2 Figure 2.5 SWA model of a stochastic task

Figure 3 . 1

 31 Figure 3.1 Examples of the satisfaction of simple temporal modalities over an execution trace

Figure 3 .

 3 Figure 3.1 represents a graphical representation of given temporal modalities for a simple case where the arguments of the modalities are atomic propositions {a, b}. In the left side of the gure, some LTL formulae are given, while in the right side their corresponding graphical representation as an example of the satisfaction relation over an execution trace.

Figure 3 . 2

 32 Figure 3.2 Examples of satisfaction of some CTL formula

Figure 3 . 3

 33 Figure 3.3 Graphical representation of the model checking approach

(

  MGL). It denes what kind of modeling components the model consists of and what attributes they have. Every modeling component is either a node type, a container type (i.e. a special node that can hold other nodes) or an edge type. It is also possible to dene which kind of nodes can be connected to which kind of edges and express cardinality constraints on those connections.Example For instance, Listing 3.1 presents of a portion of an MGL le with the definition of a container node to represent a simple task. The denition precises some attributes (period, wcet, deadline . . . ). It needs exactly one input transition and one or more output transitions. Furthermore, it can contain other nodes of type Query.

Figure 3 . 4

 34 Figure 3.4 Example of task display generated by the style conguration.

Figure 3 . 5

 35 Figure 3.5 Main principles of domain-specic tools generation with Cinco.

Figure 3 . 6

 36 Figure 3.6 Tool chain for generating and using domain-specic analysis frameworks

Figure 4 . 1

 41 Figure 4.1 Periodic Resource Model supplier with stochastic budget

Figure 4 . 2

 42 Figure 4.2 Example of Hierarchical Scheduling System

Figure 4 . 3 Figure 4 . 4

 4344 Figure 4.3 Flexible Compositional Analysis Framework

Figure 4 . 4

 44 Figure 4.4 TA template of a stochastic task (T i )

Figure 4 . 5 1 .

 451 Figure 4.5 An action to congure stochastic real-time attributes

Figure 4 . 6

 46 Figure 4.6 An action to congure stochastic real-time attributes

Figure 4 .

 4 Figure 4.6 shows an example of a job dispatcher that uses the conguration actions.

Figure 4 . 7

 47 Figure 4.7 Conceptual model of a scheduling unit of a HSS Figure 4.7 depicts the conceptual model of a scheduling unit of a HSS: The scheduling unit is composed of a set of tasks (T i ), a scheduler (A), a queue (pq) and a stochastic dispatcher D. The unit is given a PRM (Γ P RM (Π, Θ)) that is used to analyze the component in a compositional manner. We will call this resource model the supplier. Our framework supports two types of tasks: periodic task and stochastic task. A periodic task instantiates at the same period. Meanwhile, a stochastic task instantiates with a minimum inter-arrival time by an event. The real-time attributes of stochastic tasks are determined by the stochastic dispatcher D using a set Ω of probability distributions, as shown in Figure 4.7.

Figure 4 .

 4 Figure 4.7 in order to analyze the HSS in a compositional manner. The resource model Γ P RM in Fig.4.7 can stop and resume the execution of a running task. It determines when to stop and resume according to the timing requirement (Π, Θ). In our work, the TA model of resource model Γ P RM is created such that it supplies the Θ amount of resources at every period Π in a non-deterministic way, i.e. a task that is scheduled to use CPU is allowed to execute only for Θ time units at any time within its period. Such a non-deterministic behavior simulates every resource supplying patterns of a parent task, including the extreme cases when the longest starvation of the resource assignment occurs, as mentioned in Section 4.1.

Figure 4 .

 4 Figure 4.8 Abstract PRM model in TA

Figure 4 .

 4 Figure 4.9 A simulation of PRM behavior model

Figure 4 .

 4 Figure 4.10 Probability density distribution for the budgets for the scheduling unit C1.

Figure 4 .

 4 Figure 4.11 HSS with 3 scheduling units

Figure 4 .

 4 11 presents an

  The program that solved these problems rst generates the Uppaal model from the model designed in the graphical interface of the framework. It also generates a text le with the Uppaal query needed for the analysis. It then launches Uppaal or Uppaal SMC and analyses the results. The following results are displayed in the interface:

  The program that solves this problem generates the Uppaal model of the HSS with a probabilistic supplier, as the one presented in Figure 4.1. It analyses the schedulability query with Uppaal SMC. This generates a probability distribution, as the one presented in Figure 4.10. The program analyses this distribution to determine the minimum budget. It displays the result in a pop-up window.

  work studies an energy-exible ow shop scheduling problem, that is a multi-objective optimization problem whose goal is to minimize both overall completion time and global energy consumption. It employs stochastic local search techniques. We address a similar problem in our framework for multi-processor scheduling systems. Instead of execution modes and machines switch-o, the conguration options that we study are assignments of tasks to processors and we use statistical model-checking combined with the ANOVA technique to estimate energy cost and response time.

Figure 5 . 1 F

 51 Figure 5.1 F-distribution example with the p-value computed for F=2.23.

Figure. 5 . 2 ,

 52 Figure. 5.2, with values energy and resp for a set of congurations from A to F. Congurations A to D are Pareto-ecient. Conguration E is not Pareto-ecient because energy(C) < energy(E) and resp(C) < resp(E). Similarly, conguration F is no Paretoecient because resp(B) < resp(F ) and energy(B) = energy(F ).

Figure 5 . 2 Pareto-eciency curve 5 . 4 . 3

 52543 Figure 5.2 Pareto-eciency curve

Figure 5 . 3

 53 Figure 5.3 Platform layer with 2 processors, 3 hard real-time tasks and 1 soft real-time task

Figure. 5

 5 Figure. 5.5.

Figure 5 . 4 Figure 5 . 5

 5455 Figure 5.4 Application layer with 3 components and 5 actions

For

  the multi-objectives problem the program opens a pop-up window and draws into the Pareto diagram. This window allows to select one of the Pareto-ecient mapping that is then drawn on the interface. Change detection The program that performs change detection implements the CUSUM algorithm. It rst generates the Uppaal model and it will run the CUSUM algorithm on this model several times. For each execution, it generates with Uppaal SMC a simulation trace that corresponds to the total length of the experiment. It then splits this execution into a set of samples and it analyses each sample to evaluate the query and update the CUSUM ratio. If the value of ratio exceeds the sensitivity threshold it outputs a detection with the detection time in a pop-up window.

Figure 5 . 6

 56 Figure 5.6 Application layer of our case-study model

Figure 5 . 2 5. 6 . 4

 5264 Figure 5.7 Pareto Eciency diagram for optimizing energy consumption and maximum response time of task T 2

Figure 6 . 1

 61 Figure 6.1 Example Processes with schedule-dependent condential information leakage.

S 1 :

 1 L ( S) = L ( S \ S 1 ) ; hyperperiod = 3 (a) Solution leaking information. hyperperiod = 3 (b) Solution leaking no information. hyperperiod = 6 (c) Solution with waiting.

Figure 6 . 2

 62 Figure 6.2 Periodic Solutions for Leakage between hyperperiods.

Figure 6 . 3

 63 Figure 6.3 Schedulings for the processes in Figure. 6.1.

24 Figure 6 . 4

 2464 Figure 6.4 Hyperperiodic ush.

Algorithm 3 :

 3 Total Merge Preprocessor Data: task T(P, D, S) Result: processed task TE T = 0; L T = 0; X T = ⊥ for i = 1 to | S| do let S(E i , L i , X i ) = S i E T = E T + E i L T = L i X T = X i end Return T = T(P, D, S T (E T , L T , X T ))

1

 1 Average execution time (in ms) for each combination of pre-and postprocessor (except Total Merge) using the EDF scheduling algorithm.Sets of tasks with a hyperperiod over 5000 have been discarded to reduce testing time. The code3 to perform the tests and implement the preprocessing, scheduling, and postprocessing is written in Java 1.8, and all experiments conducted on a Linux 3.13 64-bit kernel on an Intel Core i7-3720QM 2.60GHz CPU with 8GB of RAM.A demo4 is available that shows examples, and allows users to conduct their own GUI-based experiments.The rest of this section discusses experimental outcomes.The rst point of interest is the schedulability of the set of tasks used in each experiment. Merging task steps in a preprocessor can make a set of tasks unschedulable, and the EDF and LSF scheduling algorithms are not equally able to nd solutions. The failure percentage for each combination of preprocessing and scheduling algorithm is shown in Figure6.5.

Figure 6 .Figure 6 . 5

 665 Figure 6.5 clearly shows that a greater merging of steps leads to more schedulability failures. In particular, indicating that Total Merge is not an eective algorithm to use in practice despite being considered as the current state of the art [MYPB14, PPY + 15].This is a strong motivation for the approach presented in this work to consider negrained preprocessing and preemption of tasks. Due to its high failure rate, Total Merge

Figure 6 . 6

 66 Figure 6.6 Information leakage of the solutions for each combination of pre-and postprocessor (except Total Merge) using the EDF scheduling algorithm.

  [ZKG + 08], the authors propose a framework for the schedulability analysis of real- time systems, where they dene a generalized model for sporadic tasks to more precisely characterizes the task arrival times. Each task is characterized by two constraints: higher instantaneous arrival rate, which bounds the maximum number of task arrivals during some small time interval; lower average arrival rate, which is used to specify the maxi-

mum number of arrivals over some longer time interval. The work of

[START_REF] Maxim | Response Time Analysis for Fixed-Priority Tasks with Multiple Probabilistic Parameters[END_REF]

considers systems with probabilistic execution times and probabilistic inter-arrival times. However it does not handle dynamic scheduling policies. Moreover, the method is a numerical analysis technique whose complexity is exponential in proportion to the number of samples and tasks. In

[START_REF] Thekkilakattil | Probabilistic preemption control using frequency scaling for sporadic real-time tasks[END_REF]

, the authors propose a method to control the preemptive behavior of real-time sporadic task systems by the use of CPU frequency scaling. They introduced a new sporadic task model in which the task arrival may deviate, according to a discrete time probability distribution, from the minimum inter-arrival time. Based on the probability of arrivals, the authors propose an on-line algorithm computing CPU frequencies that guarantee non-preemptiveness of task behavior while preserving system schedulability.

  Tasks Tasks are implemented with a SWA shown in Figure.4.4. From the Init location, a rst job is initialized with real-time attributes obtained from the function setTaskAttribute(...). This job is queued for execution at location DlyPOoset. There it requests the scheduler to assign a CPU, which is granted by a synchronisation on the channel req_sched[tstat[tid].pid], and reaches location Executing. Its execution can be stopped and resumed according to the availability of the CPU resource. This is implemented by a stopwatch clock t_et[tid]. The clock progresses only when the CPU is available, that is when the function isSchedSuped(...) returns 1. Finally, the job exits from location Executing when it has completed its execution time. This releases the CPU resource

	(a) EDF	(b) FP
	Figure 2.6 SWA models of schedulers
	Figure 2.7 PTA of the stochastic dispatcher
	using function deque_tid(...). The SWA waits the end of the minimal inter-arrival time
	(WaitEndofMINIntv) and then instantiates a new job.
	Scheduler The scheduler SWA implements the scheduling policy. We use two types
	of scheduling policy: earliest deadline rst (EDF), implemented with the SWA in Fig-
	ure. 2.6a, and xed priority (FP), implemented with the SWA in Figure. 2.6b. These
	schedulers synchronize with the task model on the channel req_sched.

  Supplier(policy,period,budget), in yellow, are intermediate suppliers (e.g., Supplier1 in Figure4.11) that receive the resource from an upper level and supply real-time tasks or lower level suppliers. Their parameters are a scheduling policy, a period and a budget within this period. To estimate the necessary budget of a scheduling unit we use a probabilistic supplier, in red, (e.g., PSupplier2 in Figure4.11) whose budget is chosen randomly between values given in an interval. It is denoted ProbSupplier(policy,period,budget), where budget is an interval of the form [LowerBound,UpperBound].Tasks Tasks are the leaf of the HSS tree. They represent the time spent for executing some computations. A task is denoted Task(period,deadline,bcet,wcet,priority) and represented in the model with a green rounded box. As presented in Section 2.5.1, we propose a new model of stochastic task whose attributes may be probability distributions. This type of task is denoted STask(period,deadline,execution,priority) and represented by a green rectangle. Here period, deadline and execution are discrete probability distributions. In-

stead of having a worst case and a best case execution time, we input a probability distribution of execution times.

Table 5

 5 .1. We give for each result the time taken by the analysis. If the result is a measure we give its estimated value and the condence interval that corresponds to the SMC analysis.

	Analysis	Result	Time (s)
	Schedulability	True	4.47
	Energy consumption (platform)	69.408 ± 0.46	1
	Energy consumption (application)	37.69 ± 0.72	4.2
	Maximum response time of T 1	3.86 ± 0.025	3.8
	Maximum response time of T 2	9.36 ± 0.055	3.78
	Maximum response time of T 3	4.89 ± 0.061	3.78
	Table 5.1 Correctness and performances analyzed with Uppaal SMC
	5.6.3 Optimization with ANOVA

Table 5 .

 5 2 Optimization of the mapping between tasks and processors according to energy consumption and maximum response time of tasks T 1 , T 2 or T 3 applied to the model.

	Exec. 1 E t(T 1 ) mapping-1 98.1 2.57 Mapping mapping-2 115 2.58 mapping-3 77.2 2.57 mapping-4 95.3 2.57 mapping-5 70.1 3.81 mapping-6 88.5 3.80 mapping-7 50.9 3.87 mapping-8 69 3.86	Exec. 2 E t(T 2 ) 98.1 6.21 115 6.24 77.3 5.74 95.1 5.76 70.2 3.58 88.5 3.74 50.8 9.34 68.7 9.33	Exec. 3 E t(T 3 ) 97.8 7.15 115 11.7 77.5 12.2 94.9 7.18 70.1 9.99 88.8 8.29 50.7 19.3 69.2 4.91

  Step). Formally, each step is a tuple S(E, L, X) where E denotes the (worst case) execution time that the step takes to be completed, L denotes its (potential) leakage value, and X denotes its security level (either high or low ⊥). (potential) leakage value L of a step S is a measure of the amount of condential information left in a shared resource at the completion of S. Again, the exact meaning of the leakage value is unimportant here. Here indicates that the step contains condential information and therefore is high-security. Similarly, ⊥ indicates that the step should not have access to condential information and therefore is low-security. Since and ⊥ are used to indicate whether the step has access to condential information, ⊥ steps typically have leakage zero. This is not a strict requirement, see Section ??. The choice of having two security levels here is to clearly illustrate the model, however the extension to any number of security levels is straightforward. Denition 6.2 (Task). Each task T x ∈ Γ is a tuple T x (P x , D x , S x ) where P x is the period of the task, D x is its relative deadline, and S x is a sequence of steps S xa , S xb , . . . making up the ordered actions of the task.Tasks are named with Greek letters, e.g. T β . Steps are named with the corresponding tasks Greek letter and a Latin letter in alphabetical order, e.g. step S βc represents the third step of task T β .

	6.3.2 Formal Model
	6.3.2.1 Steps, Tasks and Jobs
	Denition 6.1 (The Example For instance, consider Process 1 in Figure. 6.1. Each assembly instruction
	can be represented by a single step with an execution time of one time unit and a security
	level of	. The rst three instructions have a leakage value of one, representing the fact
	that one word of condential information (the key) is in the shared resource (in register
	r13). However, the remaining instructions have a leakage value of zero since the fourth
	instruction wipes r13.

The system operates with a set of tasks Γ = {T α , T β , . . .}.

  6.3.2.2 Traces, Solutions, and Resulting Leakage Denition 6.4 (Trace).A trace S = (S 1 (E 1 , L 1 , X 1 ), S 2 (E 2 , L 2 , X 2 ), . . . ) is a (possibly innite) sequence of n ∈ N ∪ {∞}steps that may come from any number of jobs.In a trace, Step S 1 starts execution at time t 1 = 0, and each step S i for i > 1 starts execution at time t i = i-1 j=1 E j and terminates execution at time t i + E i . The notation S 1 ++ S 2 is used to indicate concatenation of traces S 1 and S 2 , and S \ S 1 the removal of the step S 1 from the trace S. The focus of this chapter is upon solutions. Denition 6.5 (Solution). A trace S is a solution S if:1. for each job τ(R, A, S):

http://cinco.scce.info

30,000 sets of tasks were generated, 22 were discarded as unschedulable.

Available via git from: https://scm.gforge.inria.fr/anonscm/git/secleakpublic/secleakpublic.git

Demo available via website at: http://secleakpublic.gforge.inria.fr/

Remerciements

@style ( task ,"$ { tid }" ,"${ period }" ,"${ wcet } " ,"${ deadline }" ," ${ priority } ") container Supplier { attr EInt as tid attr EInt as period attr EInt as wcet attr EInt as priority attr EInt as deadline incomingEdges ( Transition [1 ,1 ]) outgoingEdges ( Transition [1 ,*]) containableElements ( Query ) } Listing 3.1 Part of the MGL le that species a task.

The second important le is a specication in the Meta Style Language (MSL), which is used for dening shapes (rectangle, ellipse, polygon,image, text, etc.) and appearances (colors, line style, line width, etc.) for nodes and edges. To change the look of the model depending on runtime information (e.g. the value of a node's attribute) one can either use the attribute directly within a text shape or implement an appearance provider that is invoked by the framework and may contain Java code that decides on the appearance by arbitrary external or internal factors.

Example Listing 3.2 contains the style denition for the previous task node. It is displayed with a red rounded rectangle and some texts in the top precessing the identier of the task, as shown in Figure 3 Those specications are already enough for Cinco to generate the complete graphical modeling tool. But Cinco also provides mechanisms to integrate the code that interprets Chapter 4 Hierarchical Scheduling Systems

In this chapter, we extend the model-based approach of Section 2.5 in order to model hierarchical scheduling systems HSS, that are complex scheduling systems with multiple heterogeneous scheduling levels. The next step consists of expressing a number of problems that must be veried on this model. After that, we detail the methods used to solve each problem. Then, we present a new high-level framework for specifying and verifying the models and the problems. Finally, a number of experiences using the high-level framework are presented with a discussion on their results. Key Contributions. The key contributions in this chapter are as follows:

Formal models for HSS using stochastic tasks of Chapter 3 .

A high level framework for specifying and verifying HSS models.

A set of experiments executed on a case study which is an avionic system.

Hierarchical Scheduling Systems

One of the trends in developing CPS is to execute many heterogeneous real-time components into a single high-performance platform. This does not only reduce the costs, but also improves the performances and maximizes the utilization of hardware resources.

However, these heterogeneous components must be partitioned, such that errors caused by one component are alienated from the other components. For instance, heterogeneous operating platforms in avionics and automotive systems manage various and dierent integrity-level applications. They are integrated using a high-performance hardware units of a HSS, and a set of real-time properties that must be analyzed.

The conguration of the scheduling units of a HSS is determined by the user, who denes the structure of the HSS and species the real-time attributes of individual tasks.

Once the conguration of the HSS has been made, our tool enables the designer to check the conguration of the HSS against real-time properties. In our setting, three important real-time properties are checked: the deadlock freedom of a HSS, and the schedulability and the worst-case response time of individual tasks.

Stochastic Task

In this section, we use the model of stochastic tasks presented in Section 2.5 whose realtime attributes depend on probability distributions. An execution of a task is characterized by 3 real-time attributes: an execution time, a period, and a deadline. The dierence between these stochastic tasks and the previous work [BKD + , BDK + 15a, MCG13] is that the three real-time attributes are dynamically congured according to the condition in which the system is running. This dynamic conguration is modeled by a stochastic dispatcher with an extension of timed automata with conguration actions that depends on the probability distributions.

A task represents the time spent for executing some computation. Its execution time may vary due to the length of executions of the computation logic and the capability of the execution environments, such as CPU, memory, I/O and caches, etc. Real values can be obtained by sampling the execution times from the real world system. The sampled execution times can then be captured by a probability distribution.

Meanwhile, the deadline and the period are determined according to the timing requirements of the functionality implemented by a set of tasks. For instance, some video decoder and encoder would update the deadline and period of tasks according to the frequency of input streams. In a similar way, they can also be represented by probability distributions.

In our stochastic task model we consider discrete probability distributions, dened with a random variable X given by:

where {x 1 , .., x n } are samples, P (x i ) = p i is the probability of each sample x i and n i=1 p i = 1. The probability of any variable x is given by P (x) if x ∈ {x 1 , .., x n }, otherwise P (x) = 0. When all the bottom units have been analyzed we can replace them with normal suppliers using the minimum budget that has been computed. We then repeat the procedure to compute the minimum budget for the upper scheduling units.

Results

We present in Figure 4.13 the results obtained from the analysis of the 3 bottom scheduling units (Navigation, Targeting, Weapon control). The graph plots the load factor of the scheduling unit using the minimum budget computed with SMC for several values of the periods. From these results we select the points with the lowest load factor and the highest period. The values that we choose are listed in Table 4.1. Key Contributions. The key contributions in this chapter are as follows:

New formal models for specifying complex scheduling system with models for multiprocessor scheduling systems and energy measure.

A high-level framework for specifying and verifying scheduling problems. It is automatically generated using a meta-modeling approach.

Two new techniques for solving scheduling problems. The rst one optimizes multiprocessor scheduling systems. The second one performs runtime monitoring to detect expected events.

A case-study that demonstrates the high-level framework and the verication techniques.

execution of the stochastic process is any sequence of observations {x t ∈ S | t ∈ T } of the random variables X t ∈ X . It can be represented as a sequence π = (s 0 , t 0 ), (s 1 , t 1 ), . . . , (s n , t n ), such that s i ∈ S and t i ∈ T , with time stamps monotonically increasing, e.g. t i < t i+1 . Let 0 ≤ i ≤ n, we denote π i = (s i , t i ), . . . , (s n , t n ) the sux of π starting at position i.

Let ϕ be a property that can be evaluated to true or false on an execution. We Consider for instance a stochastic scheduling system as presented previously. We can evaluate at regular time intervals the probability that the energy consumption during the time interval exceeds a given value. This probability may change at runtime if the load of the scheduling system changes, because for instance some new tasks have been added. With change detection we would like to raise an alarm when the change occurs.

Methods

In this section we detail the techniques we used to solve the problems presented in Section. 5.3.

Checking Correctness and Evaluating Performances with MC and SMC

To solve the rst three problems,i.e (Absence of deadlock, Schedulability, and Maximum

Response Time), we use the same techniques presented in Section. 4.4.1.

Energy consumption We rst measure the average energy consumed over a period of time. We use the following query: E[<= runTime;nbSim](max: PlatformEnergy.energy) PlatformEnergy is the PTAthat measures the energy using a cost variable energy. Uppaal SMC runs nbSim simulations of runTime t.u. and it computes the average value of the energy at the end of these simulations.

We can also check if the energy is always lower than a maximum value. We use the

consumption during a sample exceeds a given level. We consider a sample time of 60 time units, that corresponds to the hyper-period of the executing platform. We will observe at each sample of an execution the probability to exceed the maximum energy consumption. This probability should raise when action A 8 starts executing. We will monitor the variation of this probability during an execution of 300 samples, i.e. 18'000 time units.

The CUSUM algorithm detect a change of probability and measure the detection time.

We repeat the CUSUM 100 times and we compute the detection time as the average detection time over all the execution of the CUSUM.

To congure the CUSUM algorithm we rst need to determine the initial probability.

In this example we choose to estimate this probability by executing the optimal model, that is the model without action A 8 that provokes the change. The second parameter that we need to congure is the deviation from the initial probability when the change occurred. This parameter is estimated by computed the energy consumption on a model in which that action is already running at the beginning of the execution.

After xing these two parameters, we proceed to the calibration of the CUSUM algorithm. This step consists in computing the sensitivity threshold λ. It is done by executing CUSUM on the optimal model, without the action responsible for the change, and using the initial probability and the deviation computed before. The threshold λ will be the minimal value such that no detection is observed for all simulations.

Results We run CUSUM on the set of Pareto-ecient mappings of Figure . 5.2. The analysis of one model takes approximately 20 minutes. The results for each mapping are presented in the following tables. In these tables, the rst column (Energy) is the energy level used for the detection, the second column (Init. prob.) is the initial probability, the third column (Deviat.) is the probability deviation, the fourth column (λ) is the sensitivity threshold λ, the fth and sixth columns (T.Detect) are the detection times, in the cases when action A 8 starts after 50 or 100 executions of A 7 .

Table 5.3 presents the results obtained for mapping-6, that executes T 1 on processor P 1 and T 2 , T 3 on processor P 2 . With this mapping we can measure experimentally with Uppaal that action A 8 starts after approximately 1470 t.u. when its start parameter is 50, and 2950 t.u. when its start parameter is 100.

Table 5.4 presents the results obtained for mapping-5, such that T 1 and T 3 are executed on processor P 1 , and T 2 is executed on processor P 2 . In this mapping action A 8 begins after approximately 1480 t.u. for a start of 50, and 2970 t.u. for a start of 100.

The third mapping is mapping-8 such that T 1 and T 2 executes on P 1 and T Discussion In these experiments, we are mainly interested in the detection delay, that is the delay between the true occurrence of the event and its detection by our CUSUM algorithm. Since our models are stochastic and our experiments are based on statistics there is inevitably some variance in the results. First we have congured our algorithm in order to limit to the minimum the occurrences of false alarms. As we can see in the results there is no detection before the true occurrence of the event. There is however some detection delay. Since our algorithm is based on the measure of energy consumption, the event that we monitor (the start of action A 8 ) needs some time to produce eects on the energy consumption. Indeed the change produced by this event is quite subtle (a change from 80% CPU power to 100% CPU power, when the action is running).

Nevertheless the algorithm always manages to raise a detection.

Looking more closely at the results from the dierent mappings, we can observe that the best results are obtained from mapping-8, a model in which action A 8 (that runs on task T 3 ) is executed alone on processor P 2 . This result can be explained by the fact that A 8 running alone on P 2 is not perturbed by the preemption from other tasks, and therefore tends to produce more deterministic eects on the energy consumption. In

Add Flush. The Add Flush algorithm replaces sequences of W with F where possible (detailed in Algorithm 5). Add Flush operates by nding sequences of W whose length is greater than or equal the execution time of F. If such a sequence is found, a F is added to the produced solution instead of the initial sequence of W with execution time equal to the F. Any remaining W in the solution are maintained.

Swap. The Swap algorithm attempts to reduce the resulting leakage by swapping steps within the solution (as in Algorithm 6). Swap works by considering each step S i . Then each possible swap [S i ↔ S j ] between the step S i and a following step S j is considered.

If the trace with this swap applied has less resulting leakage and is still a solution, then this solution [S i ↔ S j ]S is kept as the best possible solution so far. Finally, once all possible swaps have been considered, the best swap to the solution is applied and i is incremented. the steps S i and S j , the move [S i -→ S j ]S moves the step S i to be after S j . For example: [S 1 -→ S 3 ]S a , S b , S c = S b , S c , S a where the rst step S a is moved to be after the third step S c . The rest of the algorithm is the same as Swap, nding the best possible move and ensuring the trace after the move is a solution. The algorithm is identical to the Swap algorithm substituting [S i ↔ S j ]S with [S i -→ S j ]S in Line 4.

1-Swap. Observe that if only swapping or moving with the following step is considered, that is [S i ↔ S i+1 ] or [S i -→ S i+1 ], then the swap and move postprocessors coincide. This postprocessor is denoted as 1-Swap in the results.