Cette thèse s'intéresse à la modélisation et à l'analyse dessystèmes temps-réel distribués.Un système distribué est constitué de plusieurs composantsqui évoluent de manière partiellement indépendante. Lorsque des actionsexécutables par différentscomposants sont indépendantes, elles sont dites concurrentes.Dans ce cas, elles peuvent être exécutées dans n'importe quel ordre, sanss'influencer, et l'état atteint après ces actions ne dépend pas de leur ordred'exécution.Dans les systèmes temps-réel distribués, les contraintes de temps créent desdépendances complexes entre les composants et les événements qui ont lieu surces composants. Malgré l'omniprésence et l'aspect critique de ces systèmes,beaucoup de leurs propriétés restent encore à étudier.En particulier, la nature distribuée de ces systèmes est souvent laissée de côté.Notre travail s'appuie sur deux formalismesde modélisation: les réseaux de Petri temporels et les réseaux d'automatestemporisés, et est divisé en deux parties.Dans la première partie, nous mettons en évidence les différences entre lessystèmes temporisés centralisés et les systèmes temporisés distribués. Nouscomparons les formalismes principaux et leurs extensions, avec une approcheoriginale qui considère la concurrence.En particulier, nous montrons comment transformer un réseau de Petri temporelen un réseau d'automates temporisés qui a le même comportement distribué.Nous nous intéressons ensuite aux horloges partagées dans lesréseaux d'automates temporisés. Les horloges partagées sont problématiqueslorsque l'on envisage d'implanter ces modèles sur des architecturesdistribuées. Nous montrons comment se passer des horloges partagées, touten préservant le comportement distribué, lorsque cela est possible.Dans la seconde partie, nous nous attachons à formaliser les dépendancesentre les événements dans les représentations en ordre partieldes exécutions des réseaux de Petri (temporels ou non).Les réseaux d'occurrence sont une de ces représentations, et leur structuredonne directement les relations de causalité, conflit et concurrence entreles événements. Cependant, nous montrons que, même dans le cas non temporisé,certaines relations logiques entre les événements nepeuvent pas être directement décrites par ces relations structurelles.Après avoir formalisé les relations logiques en question, nous résolvons leproblème de synthèse suivant: étant donnée une formule logique qui décrit unensemble d'exécutions, construire un réseau d'occurrence associé,quand celui-ci existe.Nous étudions ensuite les relations logiques dans un cadre temporisé simplifié,et montrons que le temps crée des dépendances complexes entre les événements.Ces dépendances peuvent être utilisées pour définir des dépliages canoniques deréseaux de Petri temporels, dans ce cadre simplifié. / This thesis is concerned with the modeling and the analysis of distributedreal-time systems. In distributed systems, components evolve partlyindependently: concurrent actions may be performed in any order, withoutinfluencing each other and the state reached after these actions does notdepends on the order of execution. The time constraints in distributed real-timesystems create complex dependencies between the components and the events thatoccur. So far, distributed real-time systems have not been deeply studied, andin particular the distributed aspect of these systems is often left aside. Thisthesis explores distributed real-time systems. Our work on distributed real-timesystems is based on two formalisms: time Petri nets and networks of timedautomata, and is divided into two parts.In the first part, we highlight the differences between centralized anddistributed timed systems. We compare the main formalisms and their extensions,with a novel approach that focuses on the preservation of concurrency. Inparticular, we show how to translate a time Petri net into a network of timedautomata with the same distributed behavior. We then study a concurrency relatedproblem: shared clocks in networks of timed automata can be problematic when oneconsiders the implementation of a model on a multi-core architecture. We showhow to avoid shared clocks while preserving the distributed behavior, when thisis possible.In the second part, we focus on formalizing the dependencies between events inpartial order representations of the executions of Petri nets and time Petrinets. Occurrence nets is one of these partial order representations, and theirstructure directly provides the causality, conflict and concurrency relationsbetween events. However, we show that, even in the untimed case, some logicaldependencies between event occurrences are not directly described by thesestructural relations. After having formalized these logical dependencies, wesolve the following synthesis problem: from a formula that describes a set ofruns, we build an associated occurrence net. Then we study the logicalrelations in a simplified timed setting and show that time creates complexdependencies between event occurrences. These dependencies can be used to definea canonical unfolding, for this particular timed setting.

Alternating timed automata are a powerful extension of classical Alur-Dill timed automata that are closed under all Boolean operations. They have played a key role, among others, in providing verification algorithms for prominent specification formalisms such as Metric Temporal Logic. Unfortunately, when interpreted over an infinite dense time domain (such as the reals), alternating timed automata have an undecidable language emptiness problem. In this thesis we consider restrictions on this model that restore the decidability of the language emptiness problem. We consider the restricted class of safety alternating timed automata, which can encode a corresponding Safety fragment of Metric Temporal Logic. This thesis connects these two formalisms with insertion channel machines, a model of faulty communication, and demonstrates that the three formalisms are interreducible. We thus prove a non-elementary lower bound for the language emptiness problem for 1-clock safety alternating timed automata and further obtain a new proof of decidability for this problem. Complementing the restriction to safety properties, we consider interpreting the automata over bounded dense time domains. We prove that the time-bounded language emptiness problem is decidable but non-elementary for unrestricted alternating timed automata. The language emptiness problem for alternating timed automata is a special case of a much more general and abstract logical problem: Church's synthesis problem. Given a logical specification S(I,O), Church's problem is to determine whether there exists an operator F that implements the specification in the sense that S(I,F(I)) holds for all inputs I. It is a classical result that the synthesis problem is decidable in the case that the specification and implementation are given in monadic second-order logic over the naturals. We prove that this decidability extends to MSO over the reals with order and furthermore to MSO over every fixed bounded interval of the reals with order and the +1 relation.

Nous avons étudié dans cette thèse une approche discrète de la synthèse de contrôleurs pour les systèmes hybrides permettant la manipulation de dynamiques non-linéaires : les états sont regroupés dans une partition finie au prix d'une sur-approximation non déterministe de la relation de transition. Nous avons développé des algorithmes permettant de réduire l'explosion du nombre d'états due à la discrétisation en exploitant des propriétés des systèmes ODE. Ces algorithmes sont basés sur une approche hiérarchique du problème de la synthèse en le résolvant pour des sous problèmes et en utilisant ces résultats pour réduire l'espace d'états global. Nous avons aussi combiné des objectifs de vivacité et de sécurité pour s'approcher d'une stabilisation. Des résultats implémentés sur un prototype viennent montrer l'intérêt de cette approche.Pour la vérification, nous avons étudié le problème du model checking d'automates temporisés basé sur la résolution SAT. Nous avons exploré des solutions alternatives pour le codage des réductions SAT basées sur des exécutions parallèles de transitions indépendantes. Alors qu'une telle optimisation a déjà été étudiée pour les systèmes discrets, une approche intuitive pour les automates temporisés serait de considérer que des transitions en parallèle ont lieu au même instant (synchrones). Toutefois il est possible de relâcher cette condition et nous avons montré trois sémantiques différentes pour les séquences temporisées avec des transitions parallèles. Nous montrons la correction des sémantiques et décrivons des résultats expérimentaux réalisés avec notre prototype. / We consider a discretization based approach to controller synthesis of hybrid systems that allows to handle non-linear dynamics. In such an approach, states are grouped together in a finite index partition at the price of a non-deterministic over approximation of the transition relation. The main contribution of this work is a technique to reduce the state explosion generated by the discretization: exploiting structural properties of ODE systems, we propose a hierarchical approach to the synthesis problem by solving it first for sub problems and using the results for state space reduction in the full problem. A secondary contribution concerns combined safety and liveness control objectives that approximate stabilization. Results implemented on a prototype show the benefit of this approach. For the verification, we study the model checking problem of timed automata based on SAT solving. Our work investigates alternative possibilities for coding the SAT reductions that are based on parallel executions of independent transitions. While such an optimization has been studied for discrete systems, its transposition to timed automata poses the question of what it means for timed transitions to be executed “in parallel”. The most obvious interpretation is that the transitions in parallel take place at the same time (synchronously). However, it is possible to relax this condition. On the whole, we define and analyse three different semantics of timed sequences with parallel transitions. We prove the correctness of the proposed semantics and report experimental results with a prototype implementation.

Cette thèse porte sur la vérification des automates temporisés, un modèle bien établi pour les systèmes temps-réels. La thèse est constituée de trois parties. La première est dédiée à la déterminisation des automates temporisés, problème qui n'a pas de solution en général. Nous proposons une méthode approchée (sur-approximation, sous-approximation, mélange des deux) fondée sur la construction d'un jeu de sûreté. Cette méthode améliore les approches existantes en combinant leurs avantages respectifs. Nous appliquons ensuite cette méthode de déterminisation à la génération automatique de tests de conformité. Dans la seconde partie, nous prenons en compte des aspects quantitatifs des systèmes temps-réel grâce à une notion de fréquence des états acceptants dans une exécution d'un automate temporisé. Plus précisément, la fréquence d'une exécution est la proportion de temps passée dans les états acceptants. Nous intéressons alors à l'ensemble des fréquences des exécutions d'un automate temporisé pour étudier, par exemple, le vide de langages seuils. Nous montrons ainsi que les bornes de l'ensemble des fréquences sont calculables pour deux classes d'automates temporisés. D'une part, les bornes peuvent être calculées en espace logarithmique par une procédure non-déterministe dans les automates temporisés à une horloge. D'autre part, elles peuvent être calculées en espace polynomial dans les automates temporisés à plusieurs horloges ne contenant pas de cycles forçant la convergence d'horloges. Finalement, nous étudions le problème de l'accessibilité des états acceptants dans des réseaux d'automates temporisés qui communiquent via des files FIFO. Nous considérons tout d'abord des automates temporisés à temps discret, et caractérisons les topologies de réseaux pour lesquelles l'accessibilité est décidable. Cette caractérisation est ensuite étendue aux automates temporisés à temps continu. / This thesis is about verification of timed automata, a well-established model for real time systems. The document is structured in three parts. The first part is dedicated to the determinization of timed automata, a problem which has no solution in general. We propose an approximate (over-approximation/under-approximation/mix) method based on the construction of a safety game. This method improves both existing approaches by combining their respective advantages. Then, we apply this determinization approach to the generation of conformance tests. In the second part, we take into account quantitative aspects of real time systems thanks to a notion of frequency of accepting states along executions of timed automata. More precisely, the frequency of a run is the proportion of time elapsed in accepting states. Then, we study the set of frequencies of runs of a timed automaton in order to decide, for example, the emptiness of threshold languages. We thus prove that the bounds of the set of frequencies are computable for two classes of timed automata. On the one hand, we prove that bounds are computable in logarithmic space by a non-deterministic procedure in one-clock timed automata. On the other hand, they can be computed in polynomial space in timed automata with several clocks, but having no cycle that forces the convergence between clocks. Finally, we study the reachability problem in networks of timed automata communicating through FIFO channels. We first consider dicrete timed automata, and characterize topologies of networks for which reachability is decidable. Then, this characterization is extended to dense-time automata.

Les générateurs de nombres véritablement aléatoires (TRNG) sont des composants cruciaux dans certaines applications cryptographiques sensibles (génération de clés de chiffrement, génération de signatures DSA, etc). Comme il s’agit de composants très bas-niveau, une faille dans le TRNG peut remettre en question la sécurité de tout le système cryptographique qui l’exploite. Alors que beaucoup de principes de TRNG existent dans la littérature, peu de travaux analysent rigoureusement ces architectures en termes de sécurité. L’objectif de cette thèse était d’étudier les avantages des techniques de conception asynchrone pour la conception de générateurs de nombres véritablement aléatoires (TRNG) sûrs et robustes. Nous nous sommes en particulier intéressés à des oscillateurs numériques appelés anneaux auto-séquencés. Ceux-ci exploitent un protocole de requêtes et acquittements pour séquencer les données qui y circulent. En exploitant les propriétés uniques de ces anneaux, nous proposons un nouveau principe de TRNG, avec une étude théorique détaillée sur son fonctionnement, et une évaluation du cœur du générateur dans des cibles ASIC et FPGA. Nous montrons que ce nouveau principe permet non seulement de générer des suites aléatoires de très bonne qualité et avec un très haut débit (>100 Mbit/s), mais il permet aussi une modélisation réaliste de l’entropie des bits de sortie (celle-ci peut être réglée grâce aux paramètres de l’extracteur). Ce travail propose également une méthodologie complète pour concevoir ce générateur, pour le dimensionner en fonction du niveau de bruit dans le circuit, et pour le sécuriser face aux attaques et défaillances / True Random Number Generators (TRNG) are ubiquitous in many critical cryptographic applications (key generation, DSA signatures, etc). While many TRNG designs exist in literature, only a few of them deal with security aspects, which is surprising considering that they are low-level primitives in a cryptographic system (a weak TRNG can jeopardize a whole cryptographic system). The objective of this thesis was to study the advantages of asynchronous design techniques in order to build true random number generators that are secure and robust. We especially focused on digital oscillators called self-timed rings (STR), which use a handshake request and acknowledgement protocol to organize the propagation of data. Using some of the unique properties of STRs, we propose a new TRNG principle, with a detailed theoretical study of its behavior, and an evaluation of the TRNG core in ASICs and FPGAs. We demonstrate that this new principle allows to generate high quality random bit sequences with a very high throughput (> 100 Mbit/s). Moreover, it enables a realistic estimation for the entropy per output bit (this entropy level can be tuned using the entropy extractor parameters). We also present a complete methodology to design the TRNG, to properly set up the architecture with regards to the level of noise in the circuit, and to secure it against attacks and failures

Ce mémoire, réalisé dans le cadre d’une thèse sous convention CIFRE avec la société Schneider-Electric et l’Université de Lorraine à travers le laboratoire du CRAN, porte sur l’évaluation des performances temporelles des architectures de contrôle-commande distribuées sur un réseau de communication. Le besoin industriel s’exprime sous la forme d’un outil d’aide au dimensionnement des architectures en phase d’avant-vente caractérisée par une connaissance partielle de ces dernières. Le problème scientifique sous-jacent est relatif à la génération automatique des modèles servant de support à l’évaluation. En effet, l’évaluation des performances doit être réalisée pour un ensemble important d’architectures, dans un temps court, difficilement compatible avec une construction manuelle des modèles. Notre contribution porte sur la définition formelle, à l’aide de réseaux de Petri colorés et temporisés, d’un modèle « constructeur » d’architectures embarquant des mécanismes de configuration, d’instanciation et de paramétrage. Plusieurs algorithmes sont proposés pour, d’une part, construire automatiquement le modèle d’une architecture donnée, à partir d’une description formelle de sa topologie et d’une librairie de modèles d’équipements de contrôle-commande, et, d’autre part, pour générer les observateurs requis à partir d’une description formelle des performances à évaluer. Ces différents algorithmes ont été implantés dans un outil interfacé, d’une part avec l’outil Schneider de description des architectures, et, d’autre part avec le simulateur de l’outil CPN Tools qui fournit une estimation des performances via des simulations de Monte-Carlo. L’intérêt de cette approche a été illustrée sur la base de quelques architectures types fournies par la société Schneider-Electric / This PhD dissertation, supported by CIFRE convention between the company Schneider-Electric and the University of Lorraine through the CRAN laboratory, deals with the assessment of temporal performances for a networked distributed control system. The industrial need was the development of a quotation and sizing tool of industrial control architecture during pre-sales stage. This stage is characterized by limited information about the process and the customers’ needs. The underlying scientific problematic was the ability to generate automatically models serving as support for the evaluation. In fact, performance assessment is realized for a wide range of architecture during a small amount of time, which is not compliant with a manual definition of the models. Our contribution is mainly based on a formal definition of a “builder” model with Colored and Timed Petri Nets which embeds mechanisms for configuration, instantiation and parameters setting of the architecture models. Several algorithms have been proposed for firstly build automatically the architecture Petri Nets model from a formal description of the topology and from a component model library and, secondly, for generating performance observers. Theses algorithms have been implemented on a tool gathering a user interface developed by Schneider –Electric and the Petri Nets simulator called CPN Tools which provides the performance assessment through Monte-Carlo simulation. The added value of this approach has been illustrated through case studies provided by Schneider-Electric

Notre propos est la conception assistée par ordinateur des scénarios comprenant des contenus multimédia qui interagissent avec les actions extérieures, notamment celles de l’interprète (e.g., spectacles vivants, installations muséales interactives et jeux vidéo). Le contenu multimédia est structuré dans un ordre spatial et temporel selon les exigences de l’auteur. Par conséquent, la complexité potentiellement élevée de ces scénarios nécessite des langages de spécification adéquats pour leur complète description et vérification.Partitions Interactives est un formalisme qui a été proposé comme un modèle pour la composition et l’exécution des scénarios multimédias interactifs. En outre, un séquenceur inter-médias, appelé ISCORE,a été élaboré à partir de la sémantique Petri net proposée par ce formalisme. Au cours des dernières années, I-SCORE a été utilisé avec succès pour la composition et l’exécution des spectacles et des expositions interactives. Néanmoins, ces applications et les applications émergentes telles queles jeux vidéo et les installations muséales interactives, de plus en plus exigent deux caractéristiques que la version stable actuelle de I-SCORE ainsi que son modèle sous-jacent ne supportent pas : (1)des structures de contrôle flexibles comme des conditionnelles et des boucles ; et (2) des mécanismes pour la vérification automatique de scénarios.Dans cette thèse, nous présentons deux modèles formels pour la composition et la vérification automatique de scénarios interactifs multimédia avec des choix interactifs, i.e., des scénarios où l’interprète ou le système peut prendre des décisions au sujet de leur état d’exécution avec un certain degré de liberté définie par le compositeur.Dans notre première approche, nous définissons un nouveau langage de programmation appelé REACTIVEIS dont les programmes sont définis comme des arbres représentant l’aspect hiérarchique des scénarios interactifs et dont les noeuds contiennent les conditions nécessaires pour démarrer et arrêter les objets temporels (TOS). En outre, nous définissons une sémantique opérationnelle basé sur des arbres marqués, contenant dans leurs noeuds, les informations sur le début et la fin de chaque TO. Nous définissons également une interprétation déclarative de REACTIVEIS comme formules de la logique linéaire intuitionniste avec sous exponentiels (SELL). Nous montrons que cette interprétation est adéquate : les dérivations dans la logique correspondent à des traces du programme et vice-versa.Dans notre deuxième approche, nous présentons un système basé sur des Automates Temporisés.Dans le système proposé, nous modélisons des scénarios interactifs comme un réseau d’automates temporisés et les étendons avec des points interactifs gardés par des conditions, permettant ainsi la spécification de comportements avec branchements. Par ailleurs, nous profitons des outils matures et efficaces pour simuler et vérifier automatiquement des scénarios modélisés comme des automates temporisés. Dans notre système, les scénarios peuvent être synthétisés dans un matériel reconfigurable afin de fournir une faible latence et l’exécution en temps réel.Dans cette thèse, nous explorons également une nouvelle façon de définir et mettre en oeuvre des scénarios interactifs, visant à un modèle plus dynamique en utilisant le langage réactif REACTIVEML.Enfin, nous présentons une extension des scénarios interactifs utilisant des réseaux de Petri colorés(CPN) qui vise à traiter des données complexes, en particulier, les données statiques et dynamiques de flux audio. / Interactive multimedia deals with the computer-based design of scenarios consisting of multimediacontent that interacts with external actions and those of the performer (e.g., multimedialive-performance arts, interactive museum installations, and video games). The multimedia content is structured in a spatial and temporal order according to the author’s requirements. Therefore, thepotentially high complexity of these scenarios requires adequate specification languages for theircomplete description and verification.Interactive scores is a formalism which has been proposed as a model for composing and performing interactive multimedia scenarios. In addition, an inter-media sequencer, called I-SCORE, hasbeen developed following the Petri Net semantics proposed by this formalism. During the last years,I-SCORE has been used successfully for the composition and performance of live performances and interactive exhibitions. Nevertheless, these applications and emergent applications such as videogames and interactive museum installations, increasingly demand two features that the current stable version of I-SCORE as well as its underlying model do not support: (1) flexible control structures such as conditionals and loops; and (2) mechanisms for the automatic verification of scenarios.In this dissertation we present two formal models for composition and automatic verification of multimedia interactive scenarios with interactive choices, i.e., scenarios where the performer or thesystem can take decisions about their execution state with a certain degree of freedom defined bythe composer.In our first approach, we define a novel programming language called REACTIVEIS. This language extends the full capacity of temporal organization of interactive scenarios by allowing the composerto use a defined logical system for the specification of the starting and stopping conditions of temporal objects (TOs). REACTIVEIS programs are formally defined as tree-like structures representing the hierarchical aspect of interactive scenarios and whose nodes contain the conditions needed to startand stop the TOs. Moreover, we define an operational semantics based on labeled trees, containing in their nodes, the information about the start and stop times of each TO.We show that this operational semantics offers an intuitive yet precise description of the behavior of interactive scenarios.We also endowed REACTIVEIS with a declarative interpretation as formulas in Intuitionistic LinearLogic with Subexponentials (SELL). We shall show that such interpretation is adequate: derivations in the logic correspond to traces of the program and vice-versa. Hence, we can use all the meta-theory of Intuitionistic Linear Logic (ILL) to reason about interactive scenarios and develop tools for theverification and analysis of interactive scenarios.In our second approach, we present a Timed Automata (TA) based framework. In the proposed framework, we model interactive scenarios as a network of timed automata and extend them with interactive points (IPs) guarded by conditions, thus allowing for the specification of branching behaviors.Moreover, we take advantage of the mature and efficient tools for TA to simulate and automatically verify scenarios. In our framework, scenarios can be synthesized into a reconfigurable hardware in order to provide a low-latency and real-time execution by taking advantage of the physical parallelism,low-latency, and high-reliability of these devices. Furthermore, we implemented a tool to systematically construct bottom-up TA models from the composition environment of I-SCORE. Doing that, we provide a friendly and specialized environment for composing and automatic verification of interactive scenarios. Finally, we present an extension of interactive scenarios using Colored Petri Nets (CPNs) thataims to handle complex data, in particular, dynamic and static data audio streams. [...]

Dans cette thèse nous nous sommes intéressés aux problèmes concernant la conception et la gestion des plans de soins à domicile. Un plan de soins à domicile définit l'ensemble des activités médicales et/ou sociales qui sont menées jour après jour au domicile d'un patient. Ce plan de soins est généralement construit à travers un processus complexe impliquant une évaluation complète des besoins du patient ainsi que son environnement social et physique. La spécification de plans de soins à domicile est difficile pour plusieurs raisons: les plans de soins à domicile sont par nature des processus non structurés qui impliquent des activités répétitives mais irrégulières, dont la spécification requiert des expressions temporelles complexes. Ces caractéristiques font que les plans de soins à domicile sont difficiles à modéliser en utilisant les technologies traditionnelles de modélisation de processus. Tout d'abord, nous présentons l'approche basée sur les DSL (Langage spécifique au domaine) qui permet d'exprimer les plans de soins à domicile en utilisant des abstractions de haut niveau et orientées utilisateur. Le DSL nous permet à travers cette thèse de proposer un langage de temporalités permettant de spécifier les temporalités des activités du plan de soins à domicile. Ensuite, nous décrivons comment les plans de soins à domicile, formalisés grâce aux automates temporisés, peuvent être générés à partir de ces abstractions. Nous proposons une approche en trois étapes qui consiste à: (i) le mapping entre les spécifications temporelles élémentaires et les automates temporisés appelés "pattern automata", (ii) la combinaison des "patterns automata" afin de construire les automates d'activités en utilisant l'algorithme de composition que nous avons déni, et aussi (iii) la construction de l'automate de plan de soins à domicile global. L'automate de plan de soins à domicile résultant englobe tous les schedules autorisés des activités pour un patient donné. Enfin, nous montrons comment la vérification et le suivi de l'automate du plan de soins à domicile résultant peuvent être faits en utilisant des techniques et des outils existants, en particulier en utilisant l'outil de verification UPPAAL. / In this thesis we are interested in the problems underlying the design and the management of home care plans. A home care plan defines the set of medical and/or social activities that are carried out day after day at a patient's home. Such a care plan is usually constructed through a complex process involving a comprehensive assessment of patient's needs as well as his/her social and physical environment. Specication of home care plans is challenging for several reasons: home care plans are inherently nonstructured processes which involve repetitive, but irregular, activities, whose specification requires complex temporal expressions. These features make home care plans difficult to model using traditional process modeling technologies. First, we present a DSL (Domain Specific Language) based approach tailored to express home care plans using high level and user-oriented abstractions. DSL enables us through this thesis to propose a temporalities language to specify temporalities of home care plan activities. Then, we describe how home care plans, formalized as timed automata, can be generated from these abstractions. We propose a three-step approach which consists in (i) mapping between elementary temporal specifications and timed automata called Pattern automata, (ii) combining patterns automata to build the activity automata using our composition algorithm and then (iii) constructing the global care plan automaton. The resulting care plan automaton encompasses all the possible allowed schedules of activities for a given patient. Finally, we show how verification and monitoring of the resulting care plan can be handled using existing techniques and tools, especially using UPPAAL Model Checker.

Background: The development of an objective and comprehensive drug-based index of physical function for older adults has the potential to more accurately predict fall risk. Design: the index was developed using 862 adults (ages 57–85) from the National Social Life, Health, and Aging Project (NSHAP) Wave 1 study. The index was evaluated in 70 adults (ages 51–88) from a rehabilitation study of dizziness and balance. Methods: The prevalence among 601 drugs for 1,694 side effects was used with fall history to determine the magnitude of each side effect's contribution towards physical function. This information was used to calculate a Medication-based Index of Physical function (MedIP) score for each individual based on his or her medication profile. The MedIP was compared to the timed up and go (TUG) test as well as drug counts using receiver operating characteristic (ROC) analysis. The associations between various indices of physical function and MedIP were calculated. Results: Within the NSHAP data set, the MedIP was better than drug counts or TUG at predicting falls based on ROC analysis. Using scores above and below the cutpoint, the MedIP was a significant predictor of falls (OR = 2.61 [95% CI 1.83, 3.64]; P < 0.001). Using an external data set, it was shown that the MedIP was significantly correlated with fall number (P = 0.044), composite physical function (P = 0.026) and preferred gait speed (P = 0.043).

De nos jours, la mise au point de logiciels ou de systèmes fiables est de plus en plus difficile. Les nouvelles technologies impliquent de plus en plus d'interactions entre composants complexes, dont l'analyse et la compréhension deviennent de plus en plus délicates. Pour pallier ce problème, les domaines de la vérification et de la validation ont connu un bond significatif avec la mise au point de nouvelles méthodes, réparties en deux grandes familles : la vérification formelle et la simulation. Longtemps considérées comme à l'opposée l'une de l'autre, les recherches récentes essaient de rapprocher ces deux grandes familles de méthodologies. Dans ce cadre, les travaux de cette thèse proposent une nouvelle approche pour intégrer la simulation dites à évènements discrets aux méthodes formelles. L'objectif est d'améliorer les méthodes formelles existantes, en les combinant à la simulation, afin de leur permettre de détecter des erreurs qu'elles ne pouvaient déceler avant, notamment sur des systèmes temporisés. Cette approche nous a conduit à la mise au point d'un nouveau langage formel, le DEv-PROMELA. Ce nouveau langage, créé à partir du PROMELA et du formalisme DEVS, est à mi-chemin entre un langage de spécifications formelles vérifiables et un formalisme de simulation. En combinant alors un model-checking traditionnel et une simulation à évènements discrets sur le modèle exprimé dans ce nouveau langage, il est alors possible de détecter et de comprendre des dysfonctionnements qu'un model-checking seul ou qu'une simulation seule n'auraient pas permis de trouver. Ce résultat est notamment illustré à travers les différents exemples étudiés dans ces travaux. / Nowadays, making reliable software and systems is become harder. New technologies imply more and more interactions between complex components, whose the analysis and the understanding are become arduous.To overcome this problem, the domains of verification and validation have known a significant progress, with the emergence of new automatic methods that ensure reliability of systems. Among all these techniques, we can find two great families of tools : the formal methods and the simulation. For a long time, these two families have been considered as opposite to each other. However, recent work tries to reduce the border between them. In this context, this thesis proposes a new approach in order to integrate discrete-event simulation in formal methods. The main objective is to improve existing model-checking tools by combining them with simulation, in order to allow them detecting errors that they were not previously able to find, and especially on timed systems. This approach led us to develop a new formal language, called DEv-PROMELA. This new language, which relies on the PROMELA and on the DEVS formalism, is like both a verifiable specifications language and a simulation formalism. By combining a traditional model-checking and a discrete-event simulation on models expressed in DEv-PROMELA, it is therefore possible to detect and to understand dysfunctions which could not be found by using only a formal checking or only a simulation. This result is illustrated through the different examples which are treated in this work.