Debugging is an important phase in the embedded software development cycle because of its high proportion in the overall cost in the product development. Debugging is difficult for real-time applications as such programs are time-sensitive and must meet deadlines in often a resource constrained environment. A common approach for real-time systems is to monitor the execution instead of stepping through the program, because stepping will usually violate all deadline constraints. We consider a time-triggered approach for program monitoring at runtime, resulting in bounded and predictable overhead. In time-triggered execution monitoring, a monitor runs as a separate process in parallel with an application program and samples the program's state periodically to evaluate a set of properties. Applying this technique in computing systems, results in bounded and predictable overhead. However, the time-triggered approach can have high overhead depending on the granularity of the monitoring effort. To reduce this overhead, we instrument the program with markers that will require to sample less frequently and thus reduce the overhead. This leads to interesting problems of (a) where to place the markers in the code and (b) how to manipulate the markers. While related work investigates the first part, in this work, we investigate the second part. We investigate different instrumentation schemes and propose two new schemes based on bitvectors that significantly reduce the overhead for time-triggered execution monitoring. Time-triggered execution monitoring suffers from several drawbacks such as; the time-triggered monitor requires certain synchronization features at the operating system level and may suffer from various concurrency and synchronization dependencies in a real-time setting. Furthermore, the time-triggered execution monitoring scheme requires the embedded environment to provide multi-tasking features. To address the aforementioned problems, we propose a new method called time-triggered self-monitoring, where the program under inspection is instrumented, so that it self-samples its state in a periodic fashion without requiring assistance from an external monitor or an internal timer. The experimental results show that a time-triggered self-monitored program performs significantly better in terms of execution time, binary code size, and context switches when compared to the same program monitored by an external time-triggered monitor.

Debugging is an important phase in the embedded software development cycle because of its high proportion in the overall cost in the product development. Debugging is difficult for real-time applications as such programs are time-sensitive and must meet deadlines in often a resource constrained environment. A common approach for real-time systems is to monitor the execution instead of stepping through the program, because stepping will usually violate all deadline constraints. We consider a time-triggered approach for program monitoring at runtime, resulting in bounded and predictable overhead. In time-triggered execution monitoring, a monitor runs as a separate process in parallel with an application program and samples the program's state periodically to evaluate a set of properties. Applying this technique in computing systems, results in bounded and predictable overhead. However, the time-triggered approach can have high overhead depending on the granularity of the monitoring effort. To reduce this overhead, we instrument the program with markers that will require to sample less frequently and thus reduce the overhead. This leads to interesting problems of (a) where to place the markers in the code and (b) how to manipulate the markers. While related work investigates the first part, in this work, we investigate the second part. We investigate different instrumentation schemes and propose two new schemes based on bitvectors that significantly reduce the overhead for time-triggered execution monitoring. Time-triggered execution monitoring suffers from several drawbacks such as; the time-triggered monitor requires certain synchronization features at the operating system level and may suffer from various concurrency and synchronization dependencies in a real-time setting. Furthermore, the time-triggered execution monitoring scheme requires the embedded environment to provide multi-tasking features. To address the aforementioned problems, we propose a new method called time-triggered self-monitoring, where the program under inspection is instrumented, so that it self-samples its state in a periodic fashion without requiring assistance from an external monitor or an internal timer. The experimental results show that a time-triggered self-monitored program performs significantly better in terms of execution time, binary code size, and context switches when compared to the same program monitored by an external time-triggered monitor.

The term verification can mean different things to different people based on their background and the context of research. Comparably the term runtime might bring about similar disarray with lesser confusion. Whilst a software application executes on a system, there are libraries and codes that facilitates the execution of that binary, these processes and libraries make up the runtime environment, and verification in this context refers to the concrete techniques that verify a run and checks if it satisfies or defies the specified requirements. This study is specifically concerned with runtime verification systems, and how to make use of them in a limited-resource environment such as embedded systems or Programmable Logic Controller (PLC). It is of utmost importance to validate the conformance of a system, specially those in automotive and transportation industry. Vehicles such as trains are responsible to transport millions of people everyday which makes safety and reliability of the system the most prime component of bunch. Many manufacturers employs state of the art technologies and processes to endure the safety of the final product. Since most of the parts in vehicles (including trains) are computer controlled, the system (OS, application, control system, etc.) should undergo proper and comprehensive tests to single out even the smallest anomalies and misbehaviour. While traditional software testing can detect most of the anomalies, runtime verification can be used as a complementary method to passively monitor the running system and point out those behaviours and malfunctioning that are otherwise close to impossible to be caught. This thesis investigates runtime verification in train manufacturing, and propose a structured, contemporary process and system to monitor the train control system for conformance. Furthermore several methods of formal specification to be used for declaration of specification were explored and a suitable choice for this case study was suggested, in addition a proof of concept tool to demonstrate the entire process is developed as well.

The goal of this thesis is to implement a tool that based on user defined properties can verify sequences of events in the traces of the program, or the log file. Properties are defined in extended regular expressions. The tool is able to verify parametric properties. User can define relations between parameters of events. Input of this tool is the definition of properties and constraints of parameters. Output of the tool is the report of violated properties with its sequences of events that caused the error.

The popularity and demand for safe autonomous vehicles are on the rise. Advances in semiconductor technology have led to the integration of a wide range of sensors with high-performance computers, all onboard the autonomous vehicles. The complexity of the software controlling the vehicles has also seen steady growth in recent years. Verifying the control software using traditional verification techniques is difficult and thus increases their safety concerns. Runtime verification is an efficient technique to ensure the autonomous vehicle's actions are limited to a set of acceptable behaviors that are deemed safe. The acceptable behaviors are formally described in linear temporal logic (LTL) specifications. The sensor data is actively monitored to verify its adherence to the LTL specifications using monitors. Corrective action is taken if a violation of a specification is found. An unmanned aerial vehicle (UAV) development platform is proposed for the validation of monitors on configurable hardware. A high-fidelity simulator is used to emulate the UAV and the virtual environment, thereby eliminating the need for a real UAV. The platform interfaces the emulated UAV with monitors implemented on configurable hardware and autopilot software running on a flight controller. The proposed platform allows the implementation of monitors in an isolated and scalable manner. Scenarios violating the LTL specifications can be generated in the simulator to validate the functioning of the monitors. / Master of Science / Safety is one of the most crucial factors considered when designing an autonomous vehicle. Modern vehicles that use a machine learning-based control algorithm can have unpredictable behavior in real-world scenarios that were not anticipated while training the algorithm. Verifying the underlying software code with all possible scenarios is a difficult task. Runtime verification is an efficient solution where a relatively simple set of monitors validate the decisions made by the sophisticated control software against a set of predefined rules. If the monitors detect an erroneous behavior, they initiate a predetermined corrective action. Unmanned aerial vehicles (UAVs), like drones, are a class of autonomous vehicles that use complex software to control their flight. This thesis proposes a platform that allows the development and validation of monitors for UAVs using configurable hardware. The UAV is emulated on a high-fidelity simulator, thereby eliminating the time-consuming process of flying and validating monitors on a real UAV. The platform supports the implementation of multiple monitors that can execute in parallel. Scenarios to violate rules and cause the monitors to trigger corrective actions can easily be generated on the simulator.

Runtime Verification (RV) is usually considered as a lightweight automatic verification technique for the dynamic analysis of systems, where a monitor observes executions produced by a system and analyzes its executions against a formal specification. If the monitor were synthesized, in addition to the monitoring specification, also from extra assumptions on the system behavior (typically described by a model as transition systems), then it may output more precise verdicts or even be predictive, meanwhile it may no longer be lightweight, since monitoring under assumptions has the same computation complexity with model checking. When suitable assumptions come into play, the monitor may also support partial observability, where non-observable variables in the specification can be inferred from observables, either present or historical ones. Furthermore, the monitors are resettable, i.e. being able to evaluate the specification at non-initial time of the executions while keeping memories of the input history. This helps in breaking the monotonicity of monitors, which, after reaching conclusive verdicts, can still change its future outputs by resetting its reference time. The combination of the above three characteristics (assumptions, partial observability and resets) in the monitor synthesis is called the Assumption-Based Runtime Verification, or ABRV. In this thesis, we give the formalism of the ABRV approach and a group of monitoring algorithms based on specifications expressed in Linear Temporal Logic with both future and past operators, involving Boolean and possibly other types of variables. When all involved variables have finite domain, the monitors can be synthesized as finite-state machines implemented by Binary Decision Diagrams. With infinite-domain variables, the infinite-state monitors are based on satisfiability modulo theories, first-order quantifier elimination and various model checking techniques. In particular, Bounded Model Checking is modified to do its work incrementally for efficiently obtaining inconclusive verdicts, before IC3-based model checkers get involved. All the monitoring algorithms in this thesis are implemented in a tool called NuRV. NuRV support online and offline monitoring, and can also generate standalone monitor code in various programming languages. In particular, monitors can be synthesized as SMV models, whose behavior correctness and some other properties can be further verified by model checking.

Proving the correctness of autonomous systems is challenged by the use of non-deterministic artificial intelligence algorithms and ever-increasing lines of code. While correctness is conventionally determined through analysis and testing, it is impossible to train and test the system for all possible scenarios or formally analyze millions of lines of code. This thesis describes an alternative method that monitors system behavior during runtime and executes a recovery action if any formally specified property is violated. Multiple parallel safety monitors synthesized from linear temporal logic (LTL) formulas capturing the correctness and liveness properties are implemented in isolated configurable hardware to avoid negative impacts on the system performance. Model checking applied to the final implementation establishes the correctness of the last line of defense against malicious attacks and software bugs. The first part of this thesis illustrates the monitor synthesis flow with rules defining a three-dimensional cage for a commercial-off-the-shelf drone and demonstrates the effectiveness of the monitoring system in enforcing strict behaviors. The second part of this work defines safety monitors to provide assurances for a virtual autonomous flight beyond visual line of sight. Distinct sets of monitors are called into action during different flight phases to monitor flight plan conformance, stability, and airborne collision avoidance. A wireless interface supported by the proposed architecture enables the configuration of monitors, thereby eliminating the need to reprogram the FPGA for every flight. Overall, the goal is to increase trust in autonomous systems as demonstrated with two common drone operations. / Master of Science / Software code in autonomous systems, like cars, drones, and robots, keeps growing not just in length, but also in complexity. The use of machine learning and artificial intelligence algorithms to make decisions could result in unexpected behaviors when encountering completely new situations. Traditional methods of verifying software encounter difficulties while establishing the absolute correctness of autonomous systems. An alternative to proving correctness is to enforce correct behaviors during execution. The system's inputs and outputs are monitored to ensure adherence to formally stated rules. These monitors, automatically generated from rules specified as mathematical formulas, are isolated from the rest of the system and do not affect the system performance. The first part of this work demonstrates the feasibility of the approach by adding monitors to impose a virtual cage on a commercially available drone. The second phase of this work extends the idea to a simulated autonomous flight with a predefined set of points that the drone must pass through. These points along with the necessary parameters for the monitors can be uploaded over Bluetooth. The position, speed, and distance to nearby obstacles are independently monitored and a recovery action is executed if any rule is violated. Since the monitors do not assume anything about the source of the violations, they are effective against malicious attacks, software bugs, and sensor failures. Overall, the goal is to increase confidence in autonomous systems operations.

Cette thèse étudie l’enforcement de propriétés temporisées à l’exécution en présence d’évènements incontrôlables. Les travaux se placent dans le cadre plus général de la vérification à l’exécution qui vise à surveiller l’exécution d’un système afin de s’assurer qu’elle respecte certaines propriétés. Ces propriétés peuvent être spécifiées à l’aide de formules logiques, ou au moyen d’autres modèles formels, parfois équivalents, comme des automates. Nous nous intéressons à l’enforcement à l’exécution de propriétés spécifiées par des automates temporisés. Tout comme la vérification à l’exécution, l’enforcement à l’exécution surveille l’exécution d’un système, la différence étant qu’un mécanisme d’enforcement réalise certaines modifications sur l’exécution afin de la contraindre à satisfaire la propriété souhaitée. Nous étudions plus particulièrement l’enforcement à l’exécution lorsque certains évènements de l’exécution sont incontrôlables, c’est-à-dire qu’ils ne peuvent pas être modifiés par un mécanisme d’enforcement. Nous définissons des algorithmes de synthèse de mécanismes d’enforcement décrits de manières fonctionnelle puis opérationnelle, à partir de propriétés temporisées régulières (pouvant être représentées par des automates temporisés). Ainsi, deux mécanismes d’enforcement équivalents sont définis, le premier présentant une approche correcte sans considération d’implémentation, alors que le second utilise une approche basée sur la théorie des jeux permettant de précalculer certains comportements, ce qui permet de meilleures performances. Une implémentation utilisant ce précalcul est également présentée et évaluée. Les résultats sont encourageant quant à la faisabilité de l’enforcement à l’exécution en temps réel, avec des temps supplémentaires suffisamment courts sur de petites propriétés pour permettre une utilisation de tels systèmes. / This thesis studies the runtime enforcement of timed properties when some events are uncontrollable. This work falls in the domain of runtime verification, which includes all the techniques and tools based on or related to the monitoring of system executions with respect to requirement properties. These properties can be specified using different models such as logic formulae or automata. We consider timed regular properties, that can be represented by timed automata. As for runtime verification, a runtime enforcement mechanism watches the executions of a system, but instead of just outputting a verdict, it modifies the execution so that it satisfies the property. We are interested in runtime enforcement with uncontrollable events. An uncontrollable event is an event that an enforcement mechanism can not modify. We describe the synthesis of enforcement mechanisms, in both a functional and an operational way, that enforce some desired timed regular property. We define two equivalent enforcement mechanisms, the first one being simple, without considering complexity aspects, whereas the second one has a better time complexity thanks to the use of game theory; the latter being better suited for implementation. We also detail a tool that implements the second enforcement mechanism, as well as some performance considerations. The overhead introduced by the use of our tool seems low enough to be used in some real-time application scenarios.

Protecting web services from cyber attacks is a complex problem requiring many layers of defense and mitigation strategies. Out of the diverse range of attacks, denial of service (DoS) attacks on the business logic – or the domain – are poorly studied and no widely accepted general-purpose software product to prevent these attacks exists today. At the same time, in light of the growing importance of e-commerce, defense mechanisms should be designed in a way to be self-reconfiguring, as manual reconfiguration does not scale well. In this work, a rule-based intrusion detection system (IDS) is proposed which logs the behaviour of each user and decides upon a service level based on past behaviour. The implementation is achieved by applying runtime verification (RV), a lightweight formal method which can be utilized to observe traces of user behaviour in real time. The applicability of this approach is measured by means of conducting experiments on a web service, a mock-up hotel chain which grants three different service levels for users based on their individual trust rating. Synthetic traces of bookings and cancellations are issued to account for the detection rate of the IDS and the efficacy of its mitigation strategy. The results indicate that RV is a viable approach for creating a rule-based IDS. The IDS may be tuned to attain a high detection rate of more than 95% while preserving a low false positive rates of less than 3%. Furthermore, attacks are mitigated by changing the business rules for users who have been identified as being malicious, resulting in an increased occupancy of the hotel. Lastly, RV is shown to be significantly more scalable and expressive than regular formal methods, such as model checking. Even though the results seem promising, testing the system on real traces and possibly with varying thresholds remains future work. / Att skydda webbtjänster från cyberattacker är ett komplicerat problem som kräver många lager av försvarsoch lindringsstrategier. Av det olika utbudet av attacker, denial of service attacker (DoS) på affärslogiken – eller domänen – undersöks sällan och ingen allmän accepterad mjukvara för att förhindra dessa attacker finns idag. Samtidigt, mot bakgrund av den växande betydelsen av e-handel, bör förvarsmekanismer utformas för att vara självkonfigurerande, eftersom manuell omkonfigurering inte är skalbart. I detta arbete föreslås ett regelbaserat intrusion detection system (IDS) som loggar varje användares beteende och beslutar om en servicenivå baserad på tidigare beteenden. Implementeringen uppnås genom att använda runtime verification (RV), en lättviktig formell metod som kan användas för att observera spår av användarbeteende i realtid. Tillämpningen av denna metod mäts med hjälp av experiment på en webbtjänst, en mock-up hotellkedja som ger tre olika servicenivåer för användare baserat på deras individuella förtroendevärdering. Syntetiska spår av bokningar och avbokningar används för att redovisa IDS:s detektionsgrad och effektiviteten i dess lindringsstrategi. Resultaten indikerar att RV är ett genomförbart tillvägagångssätt för att skapa ett regelbaserat IDS. Systemet kan vara inställt för att uppnå en hög detektionsgrad på mer än 95% och bevarar samtidigt en låg falsk positiv nivå på mindre än 3%. Dessutom mildras attackerna genom att ändra affärsreglerna för användare som har identifierats som skadliga, vilket resulterar i en ökad beläggning hos hotellet. Slutligen visas RV vara betydligt mer skalbar och uttrycksfull än vanliga formella metoder, till exempel model checking. Även om resultaten verkar lovande, återstår testning av systemet på riktiga spår och eventuellt med olika trösklar som framtida arbete.

La vérification à l’exécution est une méthode formelle légère qui consiste à vérifier qu’une exécution d’un système est correcte par rapport à une spécification. La spécification exprime de manière rigoureuse le comportement attendu du système, en utilisant généralement des formalismes basés sur la logique ou les machines à états finies. Alors que la verification a l’éxecution traite les systèmes monolithiques de manière exhaustive, plusieurs difficultés se présentent lors de l’application des techniques existantes à des systèmes décentralisés, c-à-d. des systèmes avec plusieurs composants sans point d’observation central. Dans cette thèse, nous nous concentrons particulièrement sur trois problèmes : la gestion de l’information partielle, la séparation du déploiement des moniteurs du processus de vérification lui-même et le raisonnement sur la décentralisation de manière modulaire et hiérarchique. Nous nous concentrons sur la notion de spécification décentralisée dans laquelle plusieurs spécifications sont fournies pour des parties distinctes du système. Utiliser une spécification décentralisée a divers avantages tels que permettre une synthèse de moniteurs à partir des spécifications complexes et la possibilité de modulariser les spécifications. Nous présentons également un algorithme de vérification général pour les spécifications décentralisées et une structure de données pour représenter l’exécution d’un automate avec observations partielles. Nous développons l’outil THEMIS, qui fournit une plateforme pour concevoir des algorithmes de vérification décentralisée, des mesures pour les algorithmes, une simulation et des expérimentations reproductibles pour mieux comprendre les algorithmes.Nous illustrons notre approche avec diverses applications. Premièrement, nous utilisons des spécifications décentralisées pour munir une analyse de pire cas, adapter, comparer et simuler trois algorithmes de vérification décentralisée existants dans deux scénarios: l’interface graphique Chiron, et des traces et spécifications générées aléatoirement. Deuxièmement, nous utilisons des spécifications décentralisées pour vérifier diverses propriétés dans un appartement intelligent: correction du comportement des capteurs de l’appartement, détection d’activité spécifiques de l’utilisateur (Activities of Daily Living, ADL) et composition de spécifications des deux catégories précédentes.En outre, nous élaborons sur l’utilisation de spécifications décentralisées pour la vérification décentralisée pendant l’exécution de programmes parallélisés. Nous commençons par discuter les limitations des approches et des outils existants lorsque les difficultés introduites par le parallélisme sont rencontrées. Nous détaillons la description de zones de parallélisme d’une unique exécution d’un programme et décrivons une approche générale qui permet de réutiliser des techniques de verification à l’éxécution existantes. Dans notre configuration, les moniteurs sont déployés dans des fils d’exécution spécifiques et échangent de l’information uniquement lorsque des points de synchronisation définis par le programme lui-même sont atteints. En utilisant les points de synchronisation existants, notre approche réduit les interférences et surcoûts résultant de la synchronisation, au prix d’un retard pour déterminer le verdict. / Runtime Verification (RV) is a lightweight formal method which consists in verifying that a run of a system is correct with respect to a specification. The specification formalizes the behavior of the system typically using logics or finite-state machines. While RV comprehensively deals with monolithic systems, multiple challenges are presented when scaling existing approaches to decentralized systems, that is, systems with multiple components with no central observation point. We focus particularly on three challenges: managing partial information, separating monitor deployment from the monitoring process itself, and reasoning about decentralization in a modular and hierarchical way. We present the notion of a decentralized specification wherein multiple specifications are provided for separate parts of the system. Decentralized specifications provide various advantages such as modularity, and allowing for realistic monitor synthesis of the specifications. We also present a general monitoring algorithm for decentralized specifications, and a general datastructure to encode automata execution with partial observations. We develop the THEMIS tool, which provides a platform for designing decentralized monitoring algorithms, metrics for algorithms, and simulation to better understand the algorithms, and design reproducible experiments.We illustrate the approach with two applications. First, we use decentralized specifications to perform a worst-case analysis, adapt, compare, and simulate three existing decentralized monitoring algorithms on both a real example of a user interface, and randomly generated traces and specifications. Second, we use decentralized specifications to check various specifications in a smart apartment: behavioral correctness of the apartment sensors, detection of specific user activities (known as activities of daily living), and composition of properties of the previous types.Furthermore, we elaborate on utilizing decentralized specifications for the decentralized online monitoring of multithreadedprograms. We first expand on the limitations of existing tools and approaches when meeting the challenges introduced by concurrency and ensure that concurrency needs to be taken into account by considering partial orders in traces. We detail the description of such concurrency areas in a single program execution, and provide a general approach which allows re-using existing RV techniques. In our setting, monitors are deployed within specific threads, and only exchange information upon reaching synchronization regions defined by the program itself. By using the existing synchronization, we reduce additional overhead and interference to synchronize at the cost of adding a delay to determine the verdict.