In this thesis, we explored the possibility of introducing a few vulnerabilities to a separation kernel to increase its performance. We made modifications to S3K, an open-source separation kernel that is in the final stages of being designed. To test the viability of our modifications we benchmarked both the unmodified and the modified versions and compared the results. We changed the scheduler and the inter-process communication used for time sharing: we introduced side-channel vulnerabilities to allow the modified functionalities to complete their work faster. The changes to the scheduler increased performance notably when having a high scheduling overhead, but not so much with low overhead. The changes to the inter-process communication proved to have limited usefulness, as the default version was already rather quick, and the new version had the drawback of increasing the time needed for scheduling. We also tested our scheduler modifications in the inter-process communication benchmarks. This greatly improved performance in all scenarios, and it made our modifications to the inter-process communication slightly more viable. To see how our results held up in a scenario closer to a real use case we also implemented a simple cryptographic application and designed tests based on it. When we ran the tests with different combinations of including or excluding our modifications we got similar results to our previous benchmarks. Overall, our modifications to the scheduler seem like a promising change to the separation kernel, given that one is willing to introduce the side-channels that come with the changes. The modifications to the inter-process communication on the other hand are more questionable and are likely only useful in specific scenarios. / I detta arbete utforskade vi möjligheten att introducera några sårbarheter till en separationskärna för att öka dess prestanda. Vi modifierade S3K, en separationskärna med öppen källkod som är i slutstadiet av att designas. För att testa hur praktiskt användbara våra modifikationer var så körde vi benchmarks på både den ursprungliga versionen och den modifierade versionen och jämförde resultaten. Vi ändrade schemaläggaren och interprocesskommunikationen som används för att dela tid: sidokanalssårbarheter introducerades för att tillåta de ändrade funktionerna att göra färdigt sina arbeten snabbare. Ändringarna till schemaläggaren visade sig öka prestandan noterbart när man hade en hög schemaläggnings-overhead, men skillnaden var inte så stor med låg overhead. Ändringarna till interprocesskommunikationen visade sig ha begränsad användbarhet, då standardversionen redan var ganska snabb och den nya versionen hade nackdelen att den ökade schemaläggningstiden. Vi testade också våra schemaläggningsmodifikationer i våra benchmarks för interprocesskommunikationen. Detta ökade prestandan mycket i alla scenarion, och gjorde våra modifikationer till interprocesskommunikationen något mer praktiskt användbara. För att se hur våra resultat stod sig i ett mer verkligt scenario så implementerade vi också en simpel kryptografisk applikation, och utformade test runt den. När vi testade olika kombinationer av att inkludera eller exkludera våra modifikationer fick vi liknande resultat som vi fick i tidigare benchmarks. Överlag så verkar våra modifikationer till schemaläggaren lovande, givet att man är villig att introducera de sidokanalssårbarheter som kommer med ändringarna. Modifikationerna till interprocesskommunikationen är dock mer tveksamma, och är sannolikt bara användbara i specifika scenarion.

Designing Resilient Distributed embedded Systems is a challenging task. One of the design issues is to guarantee correct behavior of the system during the runtime. It demands verification that information propagated through the system is reliable. The goal of this thesis is a research and implementation of an analysis that should identify obsolescence of variables due to delays caused by scheduling and communication in real-time systems. Analysis will be designed for Ensemble-Based Component System (EBCS) semantics because it enables precise specification and analysis of important properties. The main problem is to find a suitable input model of the analysis and find its possible limits. Effort should be put in balancing between the level of abstraction given to a RDS developer and power of the analysis itself. The main benefit of the analysis will be detection of situations in which data processed in RDS are outdated and can cause incorrect behavior of particular components.

Dans cette thèse, nous analysons les réseaux des systèmes temps-réel distribués et plus particulièrement ceux des domaines de l’avionique et de l’automobile. Nous nous sommes focalisés sur deux protocoles : « Avionic Full DupleX Switched Ethernet » (AFDX), « Audio Vidéo Bridging Ethernet » (AVB). Dans ces domaines critiques, le déterminisme du réseau doit être garanti. Il consiste, notamment, en la détermination d’une borne garantie du délai de bout en bout de traversée du réseau pour chaque trame ; et un dimensionnement des files d’attente des trames suffisamment grand pour garantir qu’aucune d’entre elle ne débordera et ainsi, éviter toute perte de trame.Il existe plusieurs méthodes pour l’évaluation des délais et nous avons, principalement, travaillé sur la méthode « Forward end-to-end delay Analysis » (FA). FA avait déjà été définie avec la politique d’ordonnancement « First-In-First-Out » dans le contexte de l’AFDX. Nous sommes repartis de cette approche, nous l’avons reformulé et généralisé à n’importe quel réseau Ethernet commuté. Nous l’avons aussi étendu aux priorités statiques et au protocole AVB et sa politique de service « Credit Based Shaper ». Pour chaque contribution, des démonstrations formelles ont été présentées et une expérimentation incluant une comparaison de FA avec les principales approches d’évaluation sur un exemple industriel. Finalement, nous avons développé et démontré formellement une approche pour le dimensionnement des files d’attente en termes de nombre de trames. Cette approche a été expérimentée également sur une configuration industrielle. / In this thesis, we analyze networks in the context of distributed real-time systems, especially in the fields of avionics, with “Avionics Full DupleX Switched Ethernet” (AFDX), and automobile, with “Audio Video Bridging Ethernet” (AVB). For such applications, network determinism needs to be guaranteed. It involves, in particular, assessing a guaranteed bound on the end-to-end traversal time across the network fr each frame; and dimensioning the buffers in order to avoid any loss of frame because of a buffer overflow.There are several methods for worst-case delay analysis, and we have mainly worked on the “Forward end-to-end Delay Analysis” (FA) method. FA had already been developed for “First-In-First-Out” scheduling policy in the AFDX context, so we generalized it to any Switched Ethernet network. We have also extended it to handle static priorities and the AVB protocol, shaping policy named “Credit Based Shaper” (CBS). Each contribution has been formaly proved and experiments have been led on industrial configurations. For our experimentations, we have compared our results with the results of competing approaches. Finally, we have developed and formally demonstrated an approach for buffer dimensioning in terms of number of frames. This approach has also been tested on an industrial configuration and has produced tight bounds.

Afin de garantir qu'un programme respectera toutes ses contraintes temporelles, nous devons être capable de calculer une estimation fiable de son temps d'exécution au pire cas (WCET: worst case execution time). Cependant, identifier une borne précise du pire temps d'exécution devient une tâche très complexe du fait de la sophistication croissante des processeurs. Ainsi, l'objectif de nos travaux de recherche a été de définir une méthode formelle qui puisse s'adapter aux évolutions du matériel. Cette méthode consiste à développer un modèle du processeur cible, puis à l'exécuter symboliquement afin d'associer à chaque trace d'exécution un temps d'exécution au pire cas. Une méthode de fusionnement est également prévue afin d'éviter une possible explosion combinatoire. Cette méthode a pour principale contrainte de ne pas introduire trop d'imprécision sur les temps calculés. / To ensure that a program will respect all its timing constraints we must be able to compute a safe estimation of its worst case execution time (WCET). However with the increasing sophistication of the processors, computing a precise estimation of the WCET becomes very difficult. In this report, we propose a novel formal method to compute a precise estimation of the WCET that can be easily parameterized by the hardware architecture. Assuming that we developed an executable timed model of the hardware, we use symbolic execution to precisely infer the execution time for a given instruction flow. We also merge the states relying on the loss of precision we are ready to accept, in order to avoid a possible states explosion.

A Cyber-physical System (CPS) can be described as a network of interlinked, concurrent computational components that interact with the physical world. Such a system is usually of reactive nature and must satisfy strict timing requirements to guarantee a correct behaviour. The components can be of mixed-criticality which implies different progress models and communication models, depending whether the focus of a component lies on predictability or resource efficiency. In this dissertation I present a novel approach that bridges the gap between stream processing models and Labelled Transition Systems (LTSs). The former offer powerful tools to describe concurrent systems of, usually simple, components while the latter allow to describe complex, reactive, components and their mutual interaction. In order to achieve the bridge between the two domains I introduce the novel LTS Synchronous Interface Automaton (SIA) that allows to model the interaction protocol of a process via its interface and to incrementally compose simple processes into more complex ones while preserving the system properties. Exploiting these properties I introduce an analysis to identify permanent blocking situations in a network of composed processes. SIAs are wrapped by the novel component-based coordination model Process Network with Synchronous Communication (PNSC) that allows to describe a network of concurrent processes where multiple communication models and the co-existence and interaction of heterogeneous processes is supported due to well defined interfaces. The work presented in this dissertation follows a holistic approach which spans from the theory of the underlying model to an instantiation of the model as a novel coordination language, called Streamix. The language uses network operators to compose networks of concurrent processes in a structured and hierarchical way. The work is validated by a prototype implementation of a compiler and a Run-time System (RTS) that allows to compile a Streamix program and execute it on a platform with support for ISO C, POSIX threads, and a Linux operating system.

This master's thesis is focused on benchmarking of Real-Time Operating Systems uC/OS-II and uC/OS-III . It describes the basic features of these systems and metrics used for benchmarking of Real-Time Operating Systems. Selected test methods are implemented and based on them are then compared the performance of Real-Time Operating Systems uC/OS-II and uC/OS-III .

Firm real time system with Poisson arrival process, iid exponential service times and iid deadlines till the end of service of a job, operated under the First Come First Served (FCFS) scheduling policy is well studied. In this thesis, we present an exact theoretical analysis of a similar (M/M/1 + G queue) system with exact admission control (EAC). We provide an explicit expression for the steady state workload distribution. We use this solution to derive explicit expressions for the loss ratio and the sojourn time distribution. An exact theoretical analysis of the performance of an M/M/1 + G queue with preemptive deadlines till the end of service, operating under the Earliest Deadline First (EDF) scheduling policy, appears to be difficult, and only approximate formulas for the loss ratio are available in the literature. We present in this thesis similar approximate formulas for the loss ratio in the present of an exit control mechanism, which discards a job at the epoch of its getting the server if there is no chance of completing it. We refer to this exit control mechanism as the Early job Discarding Technique (EDT). Monte Carlo simulations of performance indicate that the maximum approximation error is reasonably small for a wide range of arrival rates and mean deadlines. Finally, we compare the loss ratios of the First Come First Served and the Earliest Deadline First scheduling policies with or without admission or exit control mechanism, as well as their counterparts with deterministic deadlines. The results include some formal equalities, inequalities and some counter-examples to establish non-existence of an order. A few relations involving loss ratios are posed as conjectures, and simulation results in support of these are reported. These results lead to a complete picture of dominance and non-dominance relations between pairs of scheduling policies, in terms of loss ratios.

This thesis deals with the real time dynamic system control and it uses similar computation methods as earlier bachelor thesis. In the beginning of the thesis, some basics from the field of control and regulation are explained. Systems in this thesis are mostly described by differential equations. Because of this, thesis contains a section about solving differential equations. In this section, multiple approaches are covered and compared. The Modern Taylor series method is introduced, which is used by implemented applications. For system simulation, existing software was upgraded and multiple additional utilities were also implemented. The approximation of the transport delay is also mentioned.

This term project deals with the problem of scheduling real-time tasks in overload conditions and techniques for lowering power consumption. Each of these parts features mechanisms and reasons for their using. There are also described specific algorithms, that are implemented, in operating system uC/OS-II, and compared in next phase of master's thesis.