Calculating WCET for schedulability analysis of RTIC applications is today performed with a hybrid approach with both static analysis of code and hardware measurements. A fully static analysis tool would allow for a easier integration into a CI/CD pipeline without the actual hardware. This thesis attempts to compute WCET statically, using symbolic execution engine KLEE to generate all the possible paths of execution for a task and then analyses these paths to approximate the worst-case for each path which would yield a approximate WCET for the analysed program. To analyze a path in a program the low-level intermediary assembly language used by the LLVM optimization infrastructure (called LLVM IR) is compared to the finished assembly language to draw conclusions on how an LLVM IR instruction is processed into assembly. To be able to perform this mapping from LLVM IR to assembly, the symbolic execution engine KLEE has been extended to also log each LLVM IR instruction run in a path. These logs combined with a translation table is how the approximations are calculated. The resulting approximations correlate with the actual cycles when the analysed program is run on actual hardware, which indicates that tool could actually be used to approximate WCET. There are however no guarantees and the tool has not been tested for larger scale programs.

La recherche d'une borne supérieure au temps d'exécution d'un programme est une partie essentielle du processus de vérification de systèmes temps-réel critiques. Les programmes de tels systèmes ont généralement des temps d'exécution variables et il est difficile, voire impossible, de prédire l'ensemble de ces temps possibles. Au lieu de cela, il est préférable de rechercher une approximation du temps d'exécution pire-cas ou Worst-Case Execution Time (WCET). Une propriété cruciale de cette approximation est qu'elle doit être sûre, c'est-à-dire qu'elle doit être garantie de majorer le WCET. Parce que nous cherchons à prouver que le système en question se termine en un temps raisonnable, une surapproximation est le seul type d'approximation acceptable. La garantie de cette propriété de sûreté ne saurait raisonnablement se faire sans analyse statique, un résultat se basant sur une série de tests ne pouvant être sûr sans un traitement exhaustif des cas d'exécution. De plus, en l'absence de certification du processus de compilation (et de transfert des propriétés vers le binaire), l'extraction de propriétés doit se faire directement sur le code binaire pour garantir leur fiabilité. Toutefois, cette approximation a un coût : un pessimisme - écart entre le WCET estimé et le WCET réel - important entraîne des surcoûts superflus de matériel pour que le système respecte les contraintes temporelles qui lui sont imposées. Il s'agit donc ensuite, tout en maintenant la garantie de sécurité de l'estimation du WCET, d'améliorer sa précision en réduisant cet écart de telle sorte qu'il soit suffisamment faible pour ne pas entraîner des coûts supplémentaires démesurés. Un des principaux facteurs de surestimation est la prise en compte de chemins d'exécution sémantiquement impossibles, dits infaisables, dans le calcul du WCET. Ceci est dû à l'analyse par énumération implicite des chemins ou Implicit Path Enumeration Technique (IPET) qui raisonne sur un surensemble des chemins d'exécution. Lorsque le chemin d'exécution pire-cas ou Worst-Case Execution Path (WCEP), correspondant au WCET estimé, porte sur un chemin infaisable, la précision de cette estimation est négativement affectée. Afin de parer à cette perte de précision, cette thèse propose une technique de détection de chemins infaisables, permettant l'amélioration de la précision des analyses statiques (dont celles pour le WCET) en les informant de l'infaisabilité de certains chemins du programme. Cette information est passée sous la forme de propriétés de flot de données formatées dans un langage d'annotation portable, FFX, permettant la communication des résultats de notre analyse de chemins infaisables vers d'autres analyses. Les méthodes présentées dans cette thèse sont inclues dans le framework OTAWA, développé au sein de l'équipe TRACES à l'IRIT. Elles usent elles-mêmes d'approximations pour représenter les états possibles de la machine en différents points du programme. / The search for an upper bound of the execution time of a program is an essential part of the verification of real-time critical systems. The execution times of the programs of such systems generally vary a lot, and it is difficult, or impossible, to predict the range of the possible times. Instead, it is better to look for an approximation of the Worst-Case Execution Time (WCET). A crucial requirement of this estimate is that it must be safe, that is, it must be guaranteed above the real WCET. Because we are looking to prove that the system in question terminates reasonably quickly, an overapproximation is the only acceptable form of approximation. The guarantee of such a safety property could not sensibly be done without static analysis, as a result based on a battery of tests could not be safe without an exhaustive handling of test cases. Furthermore, in the absence of a certified compiler (and tech- nique for the safe transfer of properties to the binaries), the extraction of properties must be done directly on binary code to warrant their soundness. However, this approximation comes with a cost : an important pessimism, the gap between the estimated WCET and the real WCET, would lead to superfluous extra costs in hardware in order for the system to respect the imposed timing requirements. It is therefore important to improve the precision of the WCET by reducing this gap, while maintaining the safety property, as such that it is low enough to not lead to immoderate costs. A major cause of overestimation is the inclusion of semantically impossible paths, said infeasible paths, in the WCET computation. This is due to the use of the Implicit Path Enumeration Technique (IPET), which works on an superset of the possible execution paths. When the Worst-Case Execution Path (WCEP), corresponding to the estimated WCET, is infeasible, the precision of that estimation is negatively affected. In order to deal with this loss of precision, this thesis proposes an infeasible paths detection technique, enabling the improvement of the precision of static analyses (namely for WCET estimation) by notifying them of the infeasibility of some paths of the program. This information is then passed as data flow properties, formatted in the FFX portable annotation language, and allowing the communication of the results of our infeasible path analysis to other analyses.

Dans le domaine des systèmes critiques, l'analyse des temps d'exécution des programmes est nécessaire pour planifier et ordonnancer au mieux différentes tâches et par extension pour dimensionner les systèmes. La durée d'exécution d'un programme dépend de divers facteurs comme ses entrées ou le matériel utilisé. Or cette variation temporelle pose problème dans les systèmes temps-réel dans lesquels il est nécessaire de dimensionner précisément les temps processeur alloués à chaque tâche, et pour cela, connaître leur temps d'exécution au pire cas. Au sein de l'équipe TRACES à l'IRIT, nous cherchons à calculer une borne supérieure à ce temps d'exécution au pire cas qui soit la plus précise possible. Pour cela, nous travaillons sur le graphe de flot de contrôle d'un programme qui représente un sur-ensemble des ses exécutions possibles, que nous accompagnons d'annotations sur des comportements spécifiques du programme susceptibles de réduire la sur-approximation de notre estimation. Dans les outils destinés au calcul du temps d'exécution au pire cas des programmes, les annotations sont habituellement exprimées et intégrées grâce à des langages d'annotation spécifiques. Nous proposons d'utiliser des automates appelés automates d'annotation de flot en lieu et place de ces langages, afin de fonder non seulement l'expression, mais également l'intégration d'annotations dans l'analyse sur des bases formelles. Nous présentons ces automates enrichis de contraintes, de variables et d'une hiérarchie et nous montrons comment ils supportent les divers types d'annotations utilisés dans le domaine de l'analyse du temps d'exécution au pire cas. Par ailleurs, l'intégration des annotations dans une analyse se fait habituellement par l'association de contraintes numériques au graphe de flot de contrôle. Les automates que nous présentons supportent cette méthode mais leur expressivité offre également de nouvelles possibilités d'intégration basées sur le dépliage du graphe de flot de contrôle. Nous présentons des résultats expérimentaux issus de la comparaison de ces deux méthodes qui montrent comment le dépliage de graphe peut améliorer la précision de l'analyse. A terme, ce gain de précision dans l'estimation du temps d'exécution au pire cas permettra de mieux exploiter le matériel sans faire courir de risques à l'utilisateur ou au système. / In the domain of critical systems, the analysis of execution times of programs is needed to schedule various task at best and by extension to dimension the whole system. The execution time of a program depends on multiple factors such as entries of the program or the targeted hardware. Yet this time variation is an issue in real-time systems where the duration is required to allow correct processor time to each task, and in this purpose, we need to know their worst-case execution time. In the TRACES team at IRIT, we try to compute a safe upper bound of this worst-case execution time that would be as precise as possible. In order to do so, we work on the control flow graph of a program that represents an over-set of its possible executions and we combine this structure with annotations on specific behaviours of the program that might reduce the over-approximation of our estimation. Tools designed to compute worst-case execution times of programmes usually support the expression and the integration of annotations thanks to specific annotation languages. Our proposal is to replace these languages with a type of automata named flow fact automata so that not only the expression but also the integration of annotations in the analysis inherit from the formal basis of automata. Based on these automata enriched with constraints, variables and a hierarchy, we show how they support the various annotation types used in the worst-case execution time domain. Additionally, the integration of annotations in an analysis usually lead to associate numerical constraint to the control flow graph. The automata presented here support this method but their expressiveness offers new integration possibilities based on the partial unfolding of control flow graph. We present experimental results from the comparison of these two methods that show how the graph unfolding can improve the analysis precision. In the end, this precision gain in the worst-case execution time will ensure a better usage of the hardware as well as the absence of risks for the user or the system itself.

La croissance des flux d'information à travers le monde est responsable d'une importante utilisation de systèmes embarqués temps-réel, et ce notoirement dans le domaine des satellites. La présence de ces systèmes est devenue indispensable pour la géolocalisation, la météorologie, ou les communications. La forte augmentation du volume de ces matériels, impactée par l'afflux de demande, est à l'origine de l'accroissement de la complexité de ces derniers. Grâce à l'évolution du matériel terrestre, le domaine aérospatial se tourne vers de nouvelles technologies telles que les caches, les multi-coeurs, et les hyperviseurs. L'intégration de ces nouvelles technologies est en adéquation avec de nouveaux défis techniques. La nécessité d'améliorer les performances de ces systèmes induit le besoin de réduction du coût de fabrication et la diminution du temps de production. Les solutions technologiques qui en découlent apportent pour majeure partie des avantages en matière de diminution du nombre global de satellites à besoin constant. La densité d'information traitée est parallèlement accrue par l'augmentation du nombre d'exploitants pour chaque satellite. En effet, plusieurs clients peuvent se voir octroyer tout ou partie d'un même satellite. Intégrer les produits de plusieurs clients sur une même plateforme embarquée la rend vulnérable. Augmenter la complexité du système rend dès lors possible un certain nombre d'actes malveillants. Cette problématique autrefois à l'état d'hypothèse devient aujourd'hui un sujet majeur dans le domaine de l'aérospatial. Figure dans ce document, en premier travail d'exploration, une présentation des actes malveillants sur système embarqué, et en particulier ceux réalisés sur système satellitaire. Une fois le risque exposé, je développe la problématique temps-réel. Je m'intéresse dans cette thèse plus précisément à la sécurité des hyperviseurs spatiaux. Je développe en particulier deux axes de recherche. Le premier porte sur l'évolution des techniques de production et la mise en place d'un système de contrôle des caractéristiques temporelles d'un satellite. Le deuxième axe améliore les connaissances techniques sur un satellite en cours de fonctionnement et permet une prise de décision en cas d'acte malveillant. Je propose plus particulièrement une solution physique permettant de déceler une anomalie sur la gestion des mémoires internes au satellite. En effet, la mémoire est un composant essentiel du fonctionnement du système, et ses propriétés communes entre tous les clients la rend particulièrement vulnérable. De plus, connaître le nombre d'accès en mémoire permet un meilleur ordonnancement et une meilleure prédiction d'un système temps réel. Notre composant permet la détection et l'interprétation d'une potentielle attaque ou d'un problème de sûreté de fonctionnement. Cette thèse met en évidence la complémentarité des deux travaux proposés. En effet, la mesure du nombre d'accès en mémoire peut se mesurer via un algorithme génétique dont la forme est équivalente au programme cherchant le pire temps d'exécution. Il est finalement possible d'étendre nos travaux de la première partie vers la seconde. / Satellites are real-time embedded systems and will be used more and more in the world. Become essential for the geo-location, meteorology or communications across the planet, these systems are increasingly in demand. Due to the influx of requests, the designers of these products are designing a more and more complex hardware and software part. Thanks to the evolution of terrestrial equipment, the aero-space field is turning to new technologies such as caches, multi-core, and hypervisor. The integration of these new technologies bring new technical challenges. In effect, it is necessary to improve the performance of these systems by reducing the cost of manufacturing and the production time. One of the major advantages of these technologies is the possibility of reducing the overall number of satellites in space while increasing the number of operators. Multiple clients softwares may be together today in a same satellite. The ability to integrate multiple customers on the same satellite, with the increasing complexity of the system, makes a number of malicious acts possible. These acts were once considered as hypothetical. Become a priority today, the study of the vulnerability of such systems become major. In this paper, we present first work a quick exploration of the field of malicious acts on onboard system and more specifically those carried out on satellite system. Once the risk presentation we will develop some particular points, such as the problematic real-time. In this thesis we are particularly interested in the security of space hypervisors. We will develop precisely 2 lines of research. The first axis is focused on the development of production technics and implementing a control system of a satellite temporal characteristics. The objective is to adapt an existing system to the constraints of the new highly complex systems. We confront the difficulty of measuring the temporal characteristics running on a satellite system. For this we use an optimization method called dynamic analysis and genetic algorithm. Based on trends, it can automatically search for the worst execution time of a given function. The second axis improves the technical knowledge on a satellite in operation and enables decision making in case of malicious act. We propose specifically a physical solution to detect anomalies in the management of internal memory to the satellite. Indeed, memory is an essential component of system operation, and these common properties between all clients makes them particularly vulnerable to malicious acts. Also, know the number of memory access enables better scheduling and better predictability of a real time system. Our component allows the detection and interpretation of a potential attack or dependability problem. The work put in evidence the complementarity of the two proposed work. Indeed, the measure of the number of memory access that can be measured via a genetic algorithm whose shape is similar to the program seeking the worst execution time. So we can expand our work of the first part with the second.

Real-time systems surround every facet of our lives. They can be found in anything from everyday objects like mobile phones and washing machines to objects critical to life and infrastructure including heart rate monitors and nuclear power plants. As time progresses these systems are becoming ever more complex. To cope with the increase in complexity, developers and researchers are turning to model driven development as a solution. One modeling language aimed specifically at real-time systems is UML-RT. This thesis proposes an algorithm that for a significant subset of UML-RT is able to provide a worst-case execution time analysis for capsules at a model level. Having access to the worst-case execution times allows developers to at an early stage reason about a given system. This allows for better resource allocation as well as the ability to perform scheduling analysis. Development of the algorithm was performed iteratively using the constructive research approach. We began by first gaining an understanding of the theory. We then successively developed a theoretical algorithm selecting one or a few UML-RT entities at a time. With each iteration the algorithm was redefined to incorporate the new entities. At the end of the development, we created an implementation of the algorithm as an Eclipse Modeling Framework plug-in using Java. We then created a set of hard coded capsule models which were used to validate the algorithm.

With more functionality added to safety-critical avionics systems, new platforms are required to offer the computational capacity needed. Multi-core platforms offer a potential that is now being explored, but they pose significant challenges with respect to predictability due to shared resources (such as memory) being accessed from several cores in parallel. Multi-core processors also suffer from higher sensitivity to permanent and transient faults due to shrinking transistor sizes. This thesis addresses several of these challenges. First, we review major contributions that assess the impact of fault tolerance on worst-case execution time of processes running on a multi-core platform. In particular, works that evaluate the timing effects using fault injection methods. We conclude that there are few works that address the intricate timing effects that appear when inter-core interferences due to simultaneous accesses of shared resources are combined with the fault tolerance techniques. We assess the applicability of the methods to COTS multi-core processors used in avionics. We identify dark spots on the research map of the joint problem of hardware reliability and timing predictability for multi-core avionics systems. Next, we argue that the memory requests issued by the real-time operating systems (RTOS) must be considered in resource-monitoring systems to ensure proper execution on all cores. We also adapt and extend an existing method for worst-case response time analysis to fulfill the specific requirements of avionics systems. We relax the requirement of private memory banks to also allow cores to share memory banks.

Rapid development processes and higher customer requirements lead to increasing integration of software solutions in the automotive industry’s products. Today, several electronic control units communicate by bus systems like CAN and provide computation of complex algorithms. This increasingly requires a controlled timing behavior. The following diploma thesis investigates how the timing analysis tool SymTA/S can be used in the software development process of the ZF Friedrichshafen AG.Within the scope of several scenarios, the benefits of using it, the difficulties in using it and the questions that can not be answered by the timing analysis tool are examined. (new: additional files)

abstract: Cyber-physical systems and hard real-time systems have strict timing constraints that specify deadlines until which tasks must finish their execution. Missing a deadline can cause unexpected outcome or endanger human lives in safety-critical applications, such as automotive or aeronautical systems. It is, therefore, of utmost importance to obtain and optimize a safe upper bound of each task’s execution time or the worst-case execution time (WCET), to guarantee the absence of any missed deadline. Unfortunately, conventional microarchitectural components, such as caches and branch predictors, are only optimized for average-case performance and often make WCET analysis complicated and pessimistic. Caches especially have a large impact on the worst-case performance due to expensive off- chip memory accesses involved in cache miss handling. In this regard, software-controlled scratchpad memories (SPMs) have become a promising alternative to caches. An SPM is a raw SRAM, controlled only by executing data movement instructions explicitly at runtime, and such explicit control facilitates static analyses to obtain safe and tight upper bounds of WCETs. SPM management techniques, used in compilers targeting an SPM-based processor, determine how to use a given SPM space by deciding where to insert data movement instructions and what operations to perform at those program locations. This dissertation presents several management techniques for program code and stack data, which aim to optimize the WCETs of a given program. The proposed code management techniques include optimal allocation algorithms and a polynomial-time heuristic for allocating functions to the SPM space, with or without the use of abstraction of SPM regions, and a heuristic for splitting functions into smaller partitions. The proposed stack data management technique, on the other hand, finds an optimal set of program locations to evict and restore stack frames to avoid stack overflows, when the call stack resides in a size-limited SPM. In the evaluation, the WCETs of various benchmarks including real-world automotive applications are statically calculated for SPMs and caches in several different memory configurations. / Dissertation/Thesis / Doctoral Dissertation Computer Science 2017

In a real-time system, it is crucial to ensure that all tasks of the system holdtheir deadlines. A missed deadline in a real-time system means that the systemhas not been able to function correctly. If the system is safety critical, this canlead to disaster. To ensure that all tasks keep their deadlines, the Worst-CaseExecution Time (WCET) of these tasks has to be known. This can be done bymeasuring the execution times of a task, however, this is inflexible, time consumingand in general not safe (i.e., the worst-casemight not be found). Unlessthe task is measured with all possible input combinations and configurations,which is in most cases out of the question, there is no way to guarantee that thelongest measured time actually corresponds to the real worst case.Static analysis analyses a safe model of the hardware together with thesource or object code of a program to derive an estimate of theWCET. This estimateis guaranteed to be equal to or greater than the real WCET. This is doneby making calculations which in all steps make sure that the time is exactlyor conservatively estimated. In many cases, however, the execution time of atask or a program is highly dependent on the given input. Thus, the estimatedworst case may correspond to some input or configuration which is rarely (ornever) used in practice. For such systems, where execution time is highly inputdependent, a more accurate timing analysis which take input into considerationis desired.In this thesis we present a framework based on abstract interpretation andcounting of possible semantic states of a program. This is a general methodof WCET analysis, which is language independent and platform independent.The two main applications of this framework are a loop bound analysis and aparametric analysis. The loop bound analysis can be used to quickly find upperbounds for loops in a program while the parametric framework provides aninput-dependent estimation of theWCET. The input-dependent estimation cangive much more accurate estimates if the input is known at run-time. / PROGRESS

Realtidssystem ställer hårda krav på dess ingående mjukvaras temporala beteende. Programmen måste bete sig deterministiskt och ge svar inom satta tidsgränser. Med hårda krav följer större behov av verktyg att testa koden med. WCET (Worst Case Execution Time)-analys har som mål att finna en övre gräns för ett programs exekveringstid. SWEET (SWEdish Execution Time) är ett verktyg för WCET-analys utvecklat av en forskargrupp vid Mälardalens Högskola. PowerPC är en klassisk processorarkitektur som utvecklades av Apple, Motorola och IBM och släpptes 1991. Den har bland annat använts av Apple i äldre versioner av deras Macintosh-datorer och i TV-spelskonsoler såsom Nintendo GameCube och är stor inom inbyggda system. Tidigare har endast analys av källkod, C, varit möjlig i SWEET. Målet för detta examensarbete var att möjliggöra analys av körbara program för vilka källkoden ej är tillgänglig, Detta gjordes genom att konstruera en översättare från PowerPC-binärer till det programformat som SWEET använder för sina statiska analyser, ALF, med hjälp av tredjepartsverktyget aiT från AbsInt GmbH. Resultatet blev en med undantag för flyttalsinstruktioner komplett översättare av PowerPC-program till ALF-kod. De flesta genererade programfiler som har testats i SWEET har gett lyckat resultat. / Real-time systems put tough timing requirements on the software running on them. The programs must behave deterministically and respond within set time limits. With these demands comes a higher demand on verification tools. The goal of a WCET (Worst Case Execution Time) analysis is to derive the upper bound of a program's execution time. SWEET (SWEdish Execution Time) is a tool for WCET analysis developed by a research group at Mälardalen University. PowerPC is a classic processor architecture that was developed by Apple, Motorola and IBM and was released in 1991. It has been used in older versions of Apple's Macintosh computers and in video game consoles such as the GameCube from Nintendo, and is a popular choice for embedded solutions. Previously you could only do analyses on code generated from C in SWEET. The goal of this MSC thesis was to construct a converter from PowerPC binaries to the program format that SWEET uses for its analyses, ALF, with the help of the third-party tool aiT from AbsInt GmbH. The result is a - with the exception of floating-point instructions - complete converter from PowerPC programs to ALF. Most of the generated program files have been tested within SWEET with successful results.