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.

Depuis le début des années 90, les automates temporisés et les langages temporisés ont été largement utilisés pour modéliser et vérifier les systèmes temps réels. Ces langages ont été aussi été largement étudiés d'un point de vue théorique. Plus récemment Asarin et Degorre ont introduit les notions de volume et d'entropie des langages temporisés pour quantifier la taille de ces langages et l'information que ses éléments contiennent. Dans cette thèse nous construisons de nouveaux développements à cette théorie (que nous appelons volumétrie des langages temporisés) et l'appliquons a plusieurs problèmes apparaissant dans divers domaine de recherche tel que la théorie de l'information, la vérification, la combinatoire énumérative. Entre autre nous (i) développons une théorie de la dynamique symbolique temporisée~; (ii) caractérisons une dichotomie entre automate temporisé se comportant bien ou mal~; (iii) définissons pour un automate temporisé donné, un processus stochastique d'entropie maximale le moins biaisé possible~; (iv) développons une version temporisé de la théorie des codes sur canal contraint (v) énumérons et générons aléatoirement des permutations dans une certaine classe / Since early 90s, timed automata and timed languages are extensively used for modelling and verification of real-time systems, and thoroughly explored from a theoretical standpoint. Recently Asarin and Degorre introduced the notions of volume and entropy of timed languages to quantify the size of these languages and the information content of their elements. In this thesis we build new developments of this theory (called by us volumetry of timed languages) and apply it to several problems occurring in various domains of theoretical computer science such as verification, enumerative combinatorics or information theory. Among other we (i) develop a theory of timed symbolic dynamics; (ii) characterize a dichotomy between bad behaving and well behaving timed automata; (iii) define a least biased stochastic process for a timed automaton; (iv) develop a timed theory of constrained channel coding; (v)count and generate randomly and uniformly permutations in certain classes

<p>Testing is the dominant verification technique used in the software industry today. The use of automatic test case execution increases, but the creation of test cases remains manual and thus error prone and expensive. To automate generation and selection of test cases, model-based testing techniques have been suggested.</p><p>In this thesis two central problems in model-based testing are addressed: the problem of how to formally specify coverage criteria, and the problem of how to generate a test suite from a formal timed system model, such that the test suite satisfies a given coverage criterion. We use model checking techniques to explore the state-space of a model until a set of traces is found that together satisfy the coverage criterion. A key observation is that a coverage criterion can be viewed as consisting of a set of items, which we call coverage items. Each coverage item can be treated as a separate reachability problem. </p><p>Based on our view of coverage items we define a language, in the form of parameterized observer automata, to formally describe coverage criteria. We show that the language is expressive enough to describe a variety of common coverage criteria described in the literature. Two algorithms for test case generation with observer automata are presented. The first algorithm returns a trace that satisfies all coverage items with a minimum cost. We use this algorithm to generate a test suite with minimal execution time. The second algorithm explores only states that may increase the already found set of coverage items. This algorithm works well together with observer automata.</p><p>The developed techniques have been implemented in the tool CoVer. The tool has been used in a case study together with Ericsson where a WAP gateway has been tested. The case study shows that the techniques have industrial strength.</p>

This work is devoted to the issue of monitoring of distributed real-time systems. In particular, it focuses on formal aspects of model-based supervision and problems which are related to it. In its first part, we present the basic properties of two well-known formal models used to model distributed systems: networks of timed automata and time Petri nets. We show that the behavior of these models can be represented with so-called branching processes. We also introduce the key conceptual elements of the supervisory system. The second part of the work is dedicated to the issue of constrained unfoldings which enable us to track causal relationships between events in a distributed system. This type of structure can be used to reproduce processes of the system on the basis of a completely unordered set of previously observed events. Moreover, we show that time constraints imposed on a system and observations submitted to the supervisory system can significantly affect a course of events in the system. We also raise the issue of parameters in time constraints. The proposed methods are illustrated with case studies. The third part of the work deals with the issue of unobservable cyclical behaviors in distributed systems. This type of behaviors leads to an infinite number of events in constrained unfoldings. We explain how we can obtain a finite structure that stores information about all observed events in the system, even if this involves processes that are infinite due to such unobservable loops. The fourth and final part of the work is dedicated to implementation issues of the previously described methods.

The problem of fault diagnosis has been widely discussed by the academic community using the theory of Discrete Event Systems. However, the application of this theory to real systems is a field where there is a lot to be explored. The problem proposed in this work is to diagnose permanent or intermittent failures in devices (sensors and actuators) belonging to stations of a didactic flexible manufacturing system, called Modular Production System - MPS, produced by Festo company. The objective will be achieved through a modeling and simulation that allow for future implementation in the system. Three methods will be presented on fault diagnosis written in UPPAAL software language which is based on the timed safety automata formalism, as proposed by ALUR and DILL (1994) and HENZINGER et al (1994). The first method is an implementation of TRIPAKIS (2002) diagnoser. The other two methods developed in this research are inspired by TRIPAKIS (2002) and are diagnosable by definitions presented in TRIPAKIS (2002) and I-diagnosability presented in Sampath et al. (1995). The strategies for fault detection include the use of a network of timed safety automata, composed of the automaton that describes the process behavior and the diagnosers automata for each type of failure. The diagnosers detect failures from the observation of delays of certain transitions in the automaton G (process) and isolate them through observations of the sensors states. Fault indicators events serve to announce failures and synchronize the automaton G with the diagnosers. / O problema do diagnóstico de falhas, utilizando a teoria de Sistemas a Eventos Discretos, tem sido largamente abordado pela comunidade acadêmica. Entretanto, a aplicação desta teoria a sistemas reais é um campo onde há muito a ser explorado. O problema proposto, neste trabalho, é o de diagnosticar falhas permanentes ou intermitentes de dispositivos (sensores e atuadores) pertencentes a estações de um sistema flexível de manufatura didático, denominado Sistema Modular de Produção - MPS, fabricado pela empresa Festo. Este objetivo será alcançado por meio de uma modelagem e simulação que permitam uma futura implementação no sistema. Serão apresentados três métodos para diagnóstico de falhas escritos na linguagem do software UPPAAL que se baseia no formalismo autômatos seguros temporizados, conforme proposto por ALUR e DILL (1994) e HENZINGER et al (1994). O primeiro método é uma implementação do diagnosticador proposto em TRIPAKIS (2002). Os outros dois métodos, elaborados nesta pesquisa, são inspirados no diagnosticador TRIPAKIS (2002) e são diagnosticáveis pelos critérios apresentados em TRIPAKIS (2002) e Idiagnosticabilidade conforme SAMPATH et al. (1995). As estratégias para detecção de falhas incluem a utilização de uma rede de autômatos seguros temporizados, composta pelo autômato que descreve o comportamento do processo e por autômatos diagnosticadores para cada tipo de falha. Os diagnosticadores detectam as falhas a partir da observação de atrasos de determinadas transições do autômato G (processo) e as isolam por meio de observações dos estados dos sensores. Eventos indicadores de falhas servem para anunciar falhas e sincronizar o autômato G com os diagnosticadores.

La vérification et la validation des composants logiciels des systèmes temps réel est un des enjeuxmajeurs pour le développement de systèmes automatisés. Les modèles de tels systèmes doiventêtre vérifiés, et la conformité de leur implémentation par rapport à leur modèle doit être validée. Nous nous plaçons dans le cadre des systèmes récursifs temps réels modélisables par des automates à pile temporisés avec deadlines (TPAIO). Les deadlines imposent des conditions de progression du temps. L’objectif de cette thèse est de proposer des méthodes de génération de tests pour les TPAIO.Nos contributions sont les suivantes. Premièrement, une relation de conformité pour les TPAIO est introduite. Deuxièmement, une méthode polynomiale de génération de tests à partir d’un TPAIO déterministe avec deadline lazy est définie. Elle consiste à définir un algorithme de calcul d’un automate temporisé d’accessibilité incomplet en respectant les contraintes de pile. Cette méthode est incomplète. L’incomplétude n'étant pas un problème car l’activité de test est par essence incomplète. Troisièmement, nous définissons une méthode générant des cas de tests à partir d’un TPAIO déterministe avec sorties seulement et deadline delayable seulement. Elle d’applique aux abstractions de programmes récursifs temporisés. Elle consiste à générer des cas de tests en calculant un testeur sur-approximé. Finalement, nous avons proposé une généralisation du processus de génération de tests à partir d’un TPAIO général avec entrées/sorties et avec deadlines quelconques. La capacité de cette dernière méthode à détecter des implémentations non conformes est évaluée par une technique de mutation. / The verification and validation of software components for real-time systems is a major challenge for the development of automated systems. The models of such systems must be verified and the conformance of their implementation w.r.t their model must be validated. Our framework is that of real-time recursive systems modelled by timed pushdown automata with deadlines (TPAIO). The deadlines impose time progress conditions. The objective of this thesis is to propose test generation methods from TPAIO.Our contributions are as follows. Firstly, a conformance relation for TPAIO is introduced. Secondly, a polynomial method of test generation from a deterministic TPAIO with only lazy deadlines is defined. It consists of defining a polynomial algorithm that computes a partial reachability timed automaton by removing the stack constraints. This method is incomplete. The incompleteness is not a problem because software testing is an incomplete activity by nature. Thirdly, we define a method for generating test cases from a deterministic TPAIO with only outputs and delayable deadlines. It applies to the abstractions of timed recursive programs. It consists of generating test cases by computing an over-approximated tester. Finally, we propose a generalization of the test generation process from a non deterministic TPAIO with any deadlines. Its ability to detect non conform implementation is assessed by a mutation technique.

With the prevalence of technology and computer systems in today’s society, it is crucial to ensure that the systems we use are secure. The fields that study these issues, cybersecurity and cybersafety, use the formal verification technique of modelchecking. This paper tackles one aspect of the work needed to develop model-checking methods as we try to improve the efficiency and the reliability of model-checking techniques using the Time Petri Net model. Formal methods based on Time Petri Nets are not exempt from the state-explosion problem, and we study here different approaches to circumvent this problem. In particular, we show that limiting the exploration of such a model to runs with integer dates maintains the integrity of the model-checking result. We also show that it is possible to set a limit on the number of runs that can be explored while maintaining the probability that the observation is correct above a certain threshold. / Med tanke på hur vanligt det är med teknik och datorsystem i dagens samhälle är det viktigt att se till att de system vi använder är säkra. De områden som studerar dessa frågor, cybersäkerhet och cybersafety, använder den formella verifieringstekniken modellkontroll. Denna artikel tar upp en aspekt av det arbete som krävs för att utveckla metoder för modellkontroll, eftersom vi försöker förbättra effektiviteten och tillförlitligheten hos metoder för modellkontroll med hjälp av Time Petri Netmodellen. Formella metoder baserade på Time Petri Nets är inte undantagna från problemet med tillståndsexplosion, och vi studerar här olika tillvägagångssätt för att kringgå detta problem. I synnerhet visar vi att om man begränsar utforskningen av en sådan modell till körningar med heltalsdatum bibehålls integriteten hos resultatet av modellkontrollen. Vi visar också att det är möjligt att sätta en gräns för antalet körningar som kan utforskas samtidigt som sannolikheten för att observationen är korrekt hålls över ett visst tröskelvärde.

No description available.

Les travaux présentés dans ce manuscrit portent sur la conduite de systèmes complexes critiques. Ils s'inscrivent dans le cadre du projet CONNEXION (Investissements d'Avenir, BGLE2) qui réunit les principaux acteurs de la filière nucléaire française autour de la conception des systèmes de contrôle-commande des centrales et de leur exploitation. Dans le domaine de la conduite, les actions développées par le projet concernent la phase d'ingénierie avec pour objectif d'intégrer le point de vue de l'exploitant au plus tôt dans la validation des architectures de contrôle de commande, et la phase d'exploitation avec pour objectif de fournir une aide à la préparation et à l'exécution des procédures de conduite. Dans ce contexte, la contribution présentée dans ce mémoire porte sur la génération et la vérification de séquences d'actions de conduite répondant à un objectif donné et pouvant être opérées en toute sécurité sur le procédé. L'approche proposée repose la vérification d'une propriété d'atteignabilité sur un réseau d'automates temporisés modélisant le comportement des architectures. L'originalité réside dans la définition d’un cadre formel de modélisation sous la forme de patrons favorisant la réutilisabilité des modèles ainsi que dans la proposition d'algorithmes d'abstraction et de recherche d'atteignabilité itératifs exploitant la hiérarchisation intrinsèque des architectures afin de permettre le passage à l'échelle de l'approche proposée. La contribution a été éprouvée sur la plate-forme d'expérimentation CISPI du CRAN puis sur un cas d'étude à échelle industrielle proposé dans le cadre du projet CONNEXION / The works presented in this manuscript deals with critical complex systems operation. They are part of the CONNEXION project (Investissements d'Avenir, BGLE2), which involves the main actors in the French nuclear industry around the design of control systems for power plants and their operation. In the operation field, the actions developed by the project concern the engineering phase with the aim of integrating the operator's point of view as soon as possible in the validation of control architectures, and the operation phase with the aim of providing assistance in the preparation and execution of operation procedures. In this context, the contribution presented in this manuscript deals with the generation and verification of action sequences that meet a given objective and that can be safely operated on the process. The proposed approach relies on verifying a reachability property on a network of timed automata modelling the behavior of architectures. The originality is in the definition of a formal modelling framework using patterns promoting the reusability of models, as well as in the proposition of abstraction and reachability iterative analysis algorithms exploiting the intrinsic hierarchization of architectures in order to scale-up of the proposed approach. The contribution was evaluated on the CISPI experimental platform of the CRAN, and on an industrial scale case study proposed within the framework of the CONNEXION project