Vérification à l'exécution de spécifications décentralisées hiérarchiques

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.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