Université de Rennes 1 Enforcement à l'éxécution de propriétés temporisées Runtime enforcement of timed properties Vérification des logicielsThéorie des automatesLogique temporelleIngénierie des systèmesTemps réelComputer programs -- VerificationMachine theorySystems engineeringReal-time data processingTense (Logic) Logiciels -- VérificationThèses et écrits académiques Automates mathématiques, Théorie desThèses et écrits académiques Logique temporelleInformatiqueThèses et écrits académiques Ingénierie des systèmesThèses et écrits académiques Temps réel (informatique)Thèses et écrits académiques L'enforcement à l'exécution est une technique efficace de vérification et de validation dont le but est de corriger les exécutions incorrectes d'un système, par rapport à un ensemble de propriétés désirées. En utilisant un moniteur d'enforcement, une exécution (possiblement incorrecte), vue comme une séquence d'événements, est passée en entrée du moniteur, puis corrigée en sortie par rapport à la propriété. Durant les dix dernières années, l'enforcement à l'exécution a été étudiée pour des propriétés non temporisées. Dans cette thèse, nous considérons l'enforcement à l'exécution pour des systèmes où le temps entre les actions du système influence les propriétés à valider. Les exécutions sont donc modélisées par des séquences d'événements composées d'actions avec leurs dates d'occurence (des mots temporisés). Nous considérons l'enforcement à l'exécution pour des spécifications régulières modélisées par des automates temporisés. Les moniteurs d'enforcement peuvent, soit retarder les actions, soit les supprimer lorsque retarder les actions ne permet pas de satisfaire la spécification, permettant ainsi à l'exécution de continuer. Pour faciliter leur conception et la preuve de leur correction, les mécanismes d'enforcement sont modélisés à différents niveaux d'abstraction : les fonctions d'enforcement qui spécifient le comportement attendu des mécanismes en termes d'entrées-sorties, les contraintes qui doivent être satisfaites par ces fonctions, les moniteurs d'enforcement qui décrivent les mécanismes de manière opérationnelle, et les algorithmes d'enforcement qui fournissent une implémentation des moniteurs d'enforcement. La faisabilité de l'enforcement à l'exécution pour des propriétés temporisées est validée en prototypant la synthèse des moniteurs d'enforcement à partir d'automates temporisés. Nous montrons également l'utilité de l'enforcement à l'exécution de spécifications temporisées pour plusieurs domaines d'application. Runtime enforcement is a verification/validation technique aiming at correcting possibly incorrect executions of a system of interest. It is a powerful technique to ensure that a running system satisfies some desired properties. Using an enforcement monitor, an (untrustworthy) input execution (in the form of a sequence of events) is modified into an output sequence that complies with a property. Over the last decade, runtime enforcement has been mainly studied in the context of untimed properties. In this thesis, we consider enforcement monitoring for systems where the physical time elapsing between actions matters. Executions are thus modeled as sequences of events composed of actions with dates (called timed words). We consider runtime enforcement for timed specifications modeled as timed automata, in the general case of regular timed properties. The proposed enforcement mechanism has the power of both delaying events to match timing constraints, and suppressing events when no delaying is appropriate, thus allowing the enforcement mechanisms and systems to continue executing. To ease their design and correctness-proof, enforcement mechanisms are described at several levels: enforcement functions that specify the input-output behavior in terms of transformations of timed words, constraints that should be satisfied by such functions, enforcement monitors that describe the operational behavior of enforcement functions, and enforcement algorithms that describe the implementation of enforcement monitors. The feasibility of enforcement monitoring for timed properties is validated by prototyping the synthesis of enforcement monitors from timed automata. We also show the usefulness of enforcement monitoring of timed specifications for several application-domains. Electronic Thesis or DissertationText en application/pdf1 : 3461 Kohttps://ecm.univ-rennes1.fr/nuxeo/site/esupversions/723f4609-9d4c-4f67-853b-df3aa9007653 Pinisetty Srinivas 1985-10-25 IN 187816751 srinu85.pinisetty@gmail.com 2015REN1S004 http://www.theses.fr/2015REN1S004 2015-01-23 Informatique Université de Rennes 1thesis.degree.grantor_1 02778715X Doctorat non ouiJéronThierryintervenant_1095612777MarchandHervéintervenant_2095626360 Mathématiques, informatique, signal, électronique et télécommunicationsecoleDoctorale_1 139007164 IRISApartenaireRecherche_1 026386909 Université européenne de BretagnepartenaireRecherche_2 139075119 ddc:004 JéronThierryMarchandHervéUniversité de Rennes 1Sciences et technologie, médecine, pharmacie, odontologie, droit, économie, gestion, philosophieMathématiques, informatique, signal, électronique et télécommunicationsÉcole doctorale Mathématiques, informatique, signal, électronique et télécommunications (Rennes)IRISAUniversité européenne de Bretagne ASCII PDF 3544393